Branching Bisimulation with Explicit Divergence

Rob van Glabbeek

National ICT Australia, Sydney, Australia

School of Computer Science and Engineering, University of New South Wales, Sydney, Australia

Bas Luttik

Department of Mathematics and Computer Science, Technische Universiteit Eindhoven, The Netherlands CWI, The Netherlands

Nikola Trčka

Department of Mathematics and Computer Science, Technische Universiteit Eindhoven, The Netherlands

Abstract. We consider the relational characterisation of branching bisimulation with explicit divergence. We prove that it is an equivalence relation and that it coincides with the original definition of branching bisimulation with explicit divergence in terms of coloured traces. We also establish a correspondence with several variants of an action-based modal logic with until- and divergence modalities.

1. Introduction

Branching bisimulation with explicit divergence (BB^{Δ}) [6] is the coarsest semantic equivalence on labelled transition systems with silent moves that is a congruence for parallel composition (as found in process algebras like CCS, CSP or ACP) and only equates processes satisfying the same CTL^{∗} formulas without the nexttime operator [5]. It is also the finest equivalence in the linear time – branching time spectrum of [4].

The original definition of BB^{Δ}, in terms of coloured traces, stems from [6]. In [4], BB^{Δ} is defined in terms of a modal and a relational characterisation, which are claimed to coincide with each other and with the original notion from [6]. Of these three definitions of BB^{Δ}, the relational characterisation from [4] is the most concise one, in the sense that it requires the least amount of auxiliary concepts. Moreover, this definition is most in the style of the standard definitions of other kinds of bisimulation, found elsewhere in the literature. For these reasons, it is tempting to take it as standard definition.

Although it is not hard to establish that the modal characterisation from [4] is correct, in the sense that it defines an equivalence that coincides with BB^{Δ} of [6], it is not at all trivial to establish that the same holds for the relational characterisation from [4]. If fact, it is non-trivial that this relation is an equivalence, and that it satisfies the so-called stuttering property. Once these properties have been established, it follows that the notion coincides with BB^{Δ} of [6].

In this paper we establish that the relational characterisation of BB^{Δ} from [4] yields an equivalence relation that has the stuttering property and hence coincides with BB^{Δ}. We also explore other relational characterisations of BB^{Δ}. Finally we establish agreement between the relational characterisation from [4], the modal characterisation from [4], and an alternative modal characterisation obtained by adding the divergence modality of [4] to the Hennessy-Milner logic with until proposed in [2].

2. Relational characterisations of BB^{Δ}

We presuppose a set A of actions with a special element τ ∈ A. Furthermore, we presuppose a labelled transition system (S, →) with labels from A, i.e., S is a set and → ⊆ S × A × S is a transition relation on S. Let s, s′ ∈ S and a ∈ A. We write s ⟶^{a} s′ for (s, a, s′) ∈ → and we abbreviate the statement ‘s ⟶^{a} s′ or (a = τ and s = s′)’ by s ⟶^{(a)} s′. We denote by →^{+} the transitive closure of the binary relation ⟶^{τ}, and by ↠ its reflexive-transitive closure.

Definition 2.1. [4] A symmetric binary relation R on S is a branching bisimulation with explicit divergence if it satisfies the following two conditions for all s, t ∈ S and a ∈ A:

(T) if s R t and s ⟶^{a} s′ for some state s′, then there exist states t′ and t′′ such that t −↠ t′′ ⟶^{(a)} t′, s R t′′ and s′ R t′; and

(D) if s R t and there is an infinite sequence of states (s_{k})_{k∈ω} such that s = s_{0}, s_{k} ⟶^{τ} s_{k+1} and s_{k} R t for all k ∈ ω, then there exists an infinite sequence of states (t_{l})_{l∈ω} such that t = t_{0},

t_{l} ⟶^{τ} t_{l+1} for all l ∈ ω, and s_{k} R t_{l} for all k, l ∈ ω.

We write s \underline{↔}_{b}^{Δ} t if there exists a branching bisimulation with explicit divergence R such that s R t.

The relation \underline{↔}_{b}, defined as above but without clause (D), is the relational characterisation of branching bisimulation equivalence given in [4]. As shown in [6, 4, 1], it yields the same concept of branching bisimulation equivalence as the original definition of [6]. Figure 1 illustrates the condition (D). In [4] it was claimed that the notion \underline{↔}_{b}^{Δ} defined above coincides with branching bisimulation equivalence with explicit divergence as defined earlier in [6]. In this paper we will substantiate this claim. On the way to this end, we will show that \underline{↔}_{b}^{Δ} is an equivalence relation and has the so-called stuttering property. It will be convenient to consider three alternatives for (D) that we will now introduce.

s_{1}  s_{2}  s_{3} t^{1}  t^{2}  t^{3} τ  τ τ τ  τ  τ  τ τ s = s_{0} t = t^{0}

Figure 1. Condition (D).

The first alternative for (D) stems from the observation that (D) has some redundancy. Note that it requires for a divergence from s of which every state is related to t that there exists a divergence from t of which every state is related to every state on the divergence from s. However, both universal quantifications in the conclusion can be relaxed to existential quantifications. It suffices to require that there exists a divergence from t of which some state besides t is related to some state on the divergence from s. The requirement can be expressed as follows:

(D_{0}) if s R t and there is an infinite sequence of states (s_{k})_{k∈ω} such that s = s_{0}, s_{k} ⟶^{τ} s_{k+1} and s_{k} R t for all k ∈ ω, then there exists a state t′ such that t ⟶^{+} t′ and s_{k} R t′ for some k ∈ ω.

Although condition (D_{0}) does not explicitly require the existence of a divergence from t, using (T) it can be inductively constructed. We write s \underline{↔}_{b}^{Δ_{0}} t if there exists a symmetric binary relation R satisfying (T) and (D_{0}) such that s R t. Clearly, \underline{↔}_{b}^{Δ} ⊆ \underline{↔}_{b}^{Δ_{0}}; we shall prove in the next section that also \underline{↔}_{b}^{Δ_{0}} ⊆ \underline{↔}_{b}^{Δ}.

The difficulty in proving that \underline{↔}_{b}^{Δ} and \underline{↔}_{b}^{Δ_{0}} are equivalences is in establishing transitivity. The culprit appears to be the fact that (D) and (D_{0}) only consider divergences from s of which every state is related to t. Our second alternative omits this restriction. It considers every divergence from s and requires that it is simulated by a divergence from t.

(D_{1}) if s R t and there is an infinite sequence of states (s_{k})_{k∈ω} such that s = s_{0} and s_{k} ⟶^{τ} s_{k+1} for all k ∈ ω, then there exist an infinite sequence of states (t_{l})_{l∈ω} and a mapping σ: ω →ω such that

t = t_{0}, t_{l} ⟶^{τ} t_{l+1} and s_{σ(l)} R t_{l} for all l ∈ω.

We write s \underline{↔}_{b}^{Δ_{1}} t if there exists a symmetric binary relation R satisfying (T) and (D_{1}) such that s R t. Condition (D_{1}) has the property that if two relations both satisfy it, then so does their relational composition, and this property will facilitate a direct proof that \underline{↔}_{b}^{Δ_{1}} is transitive.

Note that (D_{0}) is a weaker requirement than (D_{1}); hence \underline{↔}_{b}^{Δ_{1}} ⊆ \underline{↔}_{b}^{Δ_{0}}. Our third alternative is a technically convenient reformulation of (D_{1}) that will serve as a stepping stone in the proof that \underline{↔}_{b}^{Δ_{0}} is included in \underline{↔}_{b}^{Δ_{1}}:

(D′_{1}) if s R t and there is an infinite sequence of states (s_{k})_{k∈ω} such that s = s_{0} and s_{k} ⟶^{τ} s_{k+1} for all k ∈ ω, then there exists a state t′ such that t ⟶^{τ} t′ and s_{k} R t′ for some k ∈ ω.

Proposition 2.1. A binary relation R satisfies (D′_{1}) iff it satisfies (D_{1}).

Proof The implication from right to left is trivial. For the implication from left to right, suppose that R satisfies (D′_{1}) and that s R t, and consider an infinite sequence of states (s_{k})_{k∈ω} such that s = s_{0} and s_{k} ⟶^{τ} s_{k+1} for all k ∈ ω. We construct an infinite sequence of states (t_{l})_{l∈ω} and a mapping σ: ω → ω

such that t = t_{0}, t_{l} ⟶^{τ} t_{l+1} and s_{σ(l)} R t_{l} for all l ∈ω.

The infinite sequence (t_{l})_{l∈ω} and the mapping σ : ω → ω can be defined simultaneously by induction on l:

1. We define t_{0} = t and σ(0) = 0; it then clearly holds that s_{σ(0)} R t_{0}.

2. Suppose that s_{σ(l)} R t_{l}. Then, since (s_{σ(l)+k})_{k∈ω} is an infinite sequence such that s_{σ(l)+k} ⟶^{τ} s_{σ(l)+k+1} for all k ∈ ω, by (D_{1}) there exists t′ such that t_{l} ⟶^{τ} t′ and s_{σ(l)+k′} R t′ for some k′ ∈ ω; we define t_{l+1} = t′ and σ(l + 1) = k′. □

Remark 2.1. It will be established below that \underline{↔}_{b}^{Δ} = \underline{↔}_{b}^{Δ_{0}}. Note that, once we have this, we can replace the second condition of Definition 2.1 by any interpolant of (D) and (D_{0}), i.e., any condition that is implied by (D) and implies (D_{0}), and end up with the same equivalence. For instance, we could replace it by the condition of Gerth, Kuiper, Peled & Penczek [3]:

if s R t and there is an infinite sequence of states (s_{k})_{k∈ω} such that s = s_{0}, s_{k} ⟶^{τ} s_{k+1} and

s_{k} R t for all k ∈ ω, then there exists a state t′ such that t ⟶^{τ} t′ and s_{k} R t′ for some k > 0;

or by the divergence condition that appears in the definition of divergence-sensitive stuttering simulation of Nejati [8]:

if s R t and there is an infinite sequence of states (s_{k})_{k∈ω} such that s = s_{0}, s_{k} ⟶^{τ} s_{k+1} and

s_{k} R t for all k ∈ ω, then there exists a state t′ such that t ⟶^{τ} t′ and s_{k} R t′ for some k ≥ 0.

Similarly, we will prove that \underline{↔}_{b}^{Δ_{1}} = \underline{↔}_{b}^{Δ_{0}}, and so we can replace the second condition of Definition 2.1 by an interpolant of (D_{1}) and (D_{0}). For instance, the condition

if s R t and there is an infinite sequence of states (s_{k})_{k∈ω} such that s = s_{0} and s_{k} ⟶^{τ} s_{k+1} for

all k ∈ ω, then there exists a state t′ such that t ⟶^{+} t′ and s_{k} R t′ for some k ≥ 0

is a convenient interpolant of (D_{1}) and (D_{0}) to use when showing that two states are branching bisimulation equivalent with explicit divergence.

3. Equivalence proof

Our goal is now to prove that \underline{↔}_{b}^{Δ} is an equivalence relation. To this end, we first show that \underline{↔}_{b}^{Δ_{1}} is an equivalence relation. In fact, we have carefully chosen condition (D_{1}) to enable a direct proof of this fact. Using this, we obtain \underline{↔}_{b}^{Δ_{1}} ⊆ \underline{↔}_{b}^{Δ}. Then, we define the notion of stuttering closure and use it to establish \underline{↔}_{b}^{Δ_{0}} ⊆ \underline{↔}_{b}^{Δ_{1}}. Together with the observation \underline{↔}_{b}^{Δ} ⊆ \underline{↔}_{b}^{Δ_{0}} made above, the cycle of inclusions yields that the relations \underline{↔}_{b}^{Δ}, \underline{↔}_{b}^{Δ_{0}} and \underline{↔}_{b}^{Δ_{1}} coincide. Therefore, \underline{↔}_{b}^{Δ} is an equivalence relation. We have not been able to find a less roundabout way to obtain this result. The material needed for the equivalence proof also yields that \underline{↔}_{b}^{Δ} has the stuttering property.

3.1. \underline{↔}_{b}^{Δ_{1}} is an equivalence relation

The proofs below are rather straightforward. Nevertheless, the proof strategy employed for both Lemma 3.1 and 3.3 would fail for \underline{↔}_{b}^{Δ} and \underline{↔}_{b}^{Δ_{0}}. It is for this reason that we present all detail.

Lemma 3.1. Let {R_{i} | i ∈ I} be a family of binary relations.

(i) If R_{i} satisfies (T) for all i ∈ I, then so does the union ⋃_{i∈I} R_{i}.

(ii) If R_{i} satisfies (D_{1}) for all i ∈ I, then so does the union ⋃_{i∈I} R_{i}.

Proof Let R = ⋃_{i∈I} R_{i}.

(i) Suppose that R_{i} satisfies (T) for all i ∈ I. To prove that R also satisfies (T), suppose that s R t and s ⟶^{a} s′ for some state s′. Then s R_{i} t for some i ∈ I. Since R_{i} satisfies (T), it follows that there are states t′ and t′′ such that t −↠ t′′ ⟶^{(a)} t′, s R_{i} t′′ and s′ R_{i} t′, and hence s R t′′ and s′ R t′.

(ii) Suppose that R_{i} satisfies (D_{1}) for all i ∈ I. To prove that R satisfies (D_{1}), suppose that s R t and that there is an infinite sequence of states (s_{k})_{k∈ω} such that s = s_{0} and s_{k} ⟶^{τ} s_{k+1}. From s R t it follows that s R_{i} t for some i ∈ I. By (D_{1}) there exist an infinite sequence of states (t_{l})_{l∈ω} and a mapping σ : ω → ω such that t = t_{0}, t_{l} ⟶^{τ} t_{l+1} and s_{σ(l)} R_{i} t_{l} for all l ∈ ω, and from the latter it follows that s_{σ(l)} R t_{l}. □

Lemma 3.2. Let R be a binary relation that satisfies (T). If s R t and s −↠ s′, then there is a state t′ such that t −↠ t′ and s′ R t′.

Proof Let s_{0}, …, s_{n} be states such that s = s_{0} ⟶^{τ} ⋯ ⟶^{τ} s_{n} = s′. By (T) and a straightforward induction on n there exist states t_{0}, …, t_{n} such that t = t_{0}−↠ ⋯−↠t_{n} = t′ and s_{i} R t_{i} for all i ≤ n. □

Lemma 3.3. Let R_{1} and R_{2} be binary relations.

(i) If R_{1} and R_{2} both satisfy (T), then so does their composition R_{1} ; R_{2}.

(ii) If R_{1} and R_{2} both satisfy (D_{1}), then so does their composition R_{1} ; R_{2}.

Proof Let R = R_{1} ; R_{2}.

(i) To prove that R satisfies (T), suppose s R u and s ⟶^{a} s′. Then there exists a state t such that s R_{1} t and t R_{2} u. Since R_{1} satisfies (T), there exist states t′ and t′′ such that t −↠ t′′ ⟶^{(a)} t′, s R_{1} t′′ and s′ R_{1} t′. By Lemma 3.2 there is a state u′′ such that u −↠ u′′ and t′′ R_{2} u′′. We now distinguish two cases:

(a) Suppose that a = τ and t′′ = t′. Then u −↠ u′′ ⟶^{(a)} u′′, from s R_{1} t′′ and t′′ R_{2} u′′ it

follows that s R u′′, and from s′ R_{1} t′ and t′ R_{2} u′′ it follows that s′ R u′′.

(b) Suppose that t′′ ⟶^{a}t′. Then there exist states u′′′ and u′ such that u′′−↠u′′′ ⟶^{(a)}u′, t′′ R_{2} u′′′

and t′ R_{2} u′. So, u −↠ u′′′ ⟶^{(a)} u′, from s R_{1} t′′ and t′′ R_{2} u′′′ it follows that s R u′′′, and

from s′ R_{1} t′ and t′ R_{2} u′ it follows that s′ R u′.

(ii) To prove that R satisfies (D_{1}), suppose that s R u and that there is an infinite sequence of states (s_{k})_{k∈ω} such that s = s_{0}, s_{k} ⟶^{τ} s_{k+1} for all k ∈ ω. As before, there exists a state t such that s R_{1} t and t R_{2} u. From s R_{1} t it follows that there exist an infinite sequence of states (t_{l})_{l∈ω} and a mapping σ : ω → ω such that t = t_{0}, t_{l} ⟶^{τ} t_{l+1} and s_{σ(l)} R t_{l} for all l ∈ ω. Hence, since t R_{2} u, it follows that there exist an infinite sequence of states (u_{m})_{m∈ω} and a mapping ρ : ω → ω

such that u = u_{0}, u_{m} ⟶^{τ} u_{m+1} and t_{ρ(m)} R_{2} u_{m} for all m ∈ ω. Clearly, s_{σ(ρ(m))} R u_{m} for all

m ∈ ω. □

Theorem 3.1. \underline{↔}_{b}^{Δ_{1}} is an equivalence relation.

Proof The diagonal on S (i.e., the binary relation {(s, s) | s ∈ S}) is a symmetric relation that satisfies (T) and (D_{1}), so \underline{↔}_{b}^{Δ_{1}} is reflexive. Furthermore, that \underline{↔}_{b}^{Δ_{1}} is symmetric is immediate from the required symmetry of the witnessing relation.

To prove that \underline{↔}_{b}^{Δ_{1}} is transitive, suppose s \underline{↔}_{b}^{Δ_{1}} t and t \underline{↔}_{b}^{Δ_{1}} u. Then there exist symmetric binary relations R_{1} and R_{2} satisfying (T) and (D_{1}) such that s R_{1} t and t R_{2} u. The relation R = (R_{1} ; R_{2}) ∪ (R_{2} ; R_{1}) is clearly symmetric and, by Lemmas 3.1 and 3.3, satisfies (T) and (D_{1}). Hence, since s R u, it follows that s \underline{↔}_{b}^{Δ_{1}} u. □

3.2. \underline{↔}_{b}^{Δ_{1}} is included in \underline{↔}_{b}^{Δ}

To prove the inclusion \underline{↔}_{b}^{Δ_{1}} ⊆ \underline{↔}_{b}^{Δ} we establish that \underline{↔}_{b}^{Δ_{1}} is a branching bisimulation with explicit divergence.

Lemma 3.4. The relation \underline{↔}_{b}^{Δ_{1}} satisfies (T) and (D_{1}).

Proof Directly from the definition it follows that \underline{↔}_{b}^{Δ_{1}} is the union of all symmetric relations satisfying (T) and (D_{1}), so, using Lemma 3.1, \underline{↔}_{b}^{Δ_{1}} itself satisfies (T) and (D_{1}). □

In fact, it is now clear that \underline{↔}_{b}^{Δ_{1}} is the largest symmetric binary relation satisfying (T) and (D_{1}).

Lemma 3.5. The relation \underline{↔}_{b}^{Δ_{1}} satisfies (D).

Proof Suppose that s \underline{↔}_{b}^{Δ_{1}} t and that there is an infinite sequence of states (s_{k})_{k∈ω} such that s = s_{0}, s_{k} ⟶^{τ} s_{k+1} and s_{k} \underline{↔}_{b}^{Δ_{1}} t for all k ∈ ω. According to Lemma 3.4, the relation \underline{↔}_{b}^{Δ_{1}} satisfies (D_{1}), so there exist an infinite sequence of states (t_{l})_{l∈ω} and a mapping σ : ω → ω such that t = t_{0}, t_{l} ⟶^{τ} t_{l+1} and s_{σ(l)} \underline{↔}_{b}^{Δ_{1}} t_{l} for all l ∈ ω. By Theorem 3.1, \underline{↔}_{b}^{Δ_{1}} is an equivalence relation, so it follows from s_{k} \underline{↔}_{b}^{Δ_{1}} t, s_{σ(l)} \underline{↔}_{b}^{Δ_{1}} t and s_{σ(l)} \underline{↔}_{b}^{Δ_{1}} t_{l} that s_{k} \underline{↔}_{b}^{Δ_{1}} t_{l} for all k, l ∈ ω. Hence \underline{↔}_{b}^{Δ_{1}} satisfies (D). □

Theorem 3.2. \underline{↔}_{b}^{Δ_{1}} ⊆ \underline{↔}_{b}^{Δ}.

Proof By Theorem 3.1, the relation \underline{↔}_{b}^{Δ_{1}} is symmetric. By Lemma 3.4, it satisfies (T), and by Lemma 3.5 it satisfies (D). So \underline{↔}_{b}^{Δ_{1}} is a branching bisimulation with explicit divergence, and hence s \underline{↔}_{b}^{Δ_{1}} t implies s \underline{↔}_{b}^{Δ} t. □

3.3. Stuttering closure

Definition 3.1. A binary relation R has the stuttering property if, whenever t_{0} ⟶^{τ} ⋯ ⟶^{τ} t_{n}, s R t_{0} and s R t_{n}, then s R t_{i} for all i = 0, …, n.

The following operation converts any binary relation R on S into a larger relation R̂ that has the stuttering property.

Definition 3.2. Let R be a binary relation on S. The stuttering closure R̂ of R is defined by

R̂ = {(s, t) | ∃s^{♭}, s^{♯}, t^{♭}, t^{♯} ∈ S. s^{♭} −↠ s −↠ s^{♯} & t^{♭} −↠ t −↠ t^{♯} & s^{♭} R t^{♯} & s^{♯} R t^{♭}} .

Figure 2 illustrates the notion of stuttering closure. Clearly R ⊆ R̂. We establish a few basic properties of the stuttering closure.

Lemma 3.6. The stuttering closure of a binary relation has the stuttering property.

Proof Let R be a binary relation and let R̂ be its stuttering closure. To show that R̂ has the stuttering property, suppose that t_{0} ⟶^{τ} ⋯ ⟶^{τ} t_{n}, s R̂ t_{0} and s R̂ t_{n}. Then, on the one hand, there exist states s^{♯} and t_{0}^{♭} such that s −↠ s^{♯}, t_{0}^{♭} −↠ t_{0} and s^{♯} R t_{0}^{♭}, and on the other hand there exist states s^{♭} and t_{n}^{♯} such that s^{♭} −↠ s, t_{n} −↠ t_{n}^{♯} and s^{♭} R t_{n}^{♯}. Now, since s^{♭} −↠ s −↠ s^{♯} and t_{0}^{♭} −↠ t_{i} −↠ t_{n}^{♯} for all i = 0, …, n, it follows that s R̂ t_{i}. □

t^{♯} s^{♯} s s^{♭} t^{♭}  t

Figure 2. Stuttering closure.

Remark 3.1. The stuttering closure R̂ of a binary relation R is not necessarily the smallest relation containing R with the stuttering property. For a counterexample, consider a transition system with states s^{♭}, s^{♯}, t^{♭} and t^{♯} and transitions s^{♭} ⟶^{τ} s^{♯} and t^{♭} ⟶^{τ} t^{♯}; the binary relation

R = {(s^{♭}, t^{♯}), (t^{♯}, s^{♭}), (s^{♯}, t^{♭}), (t^{♭}, s^{♯}), (s^{♯}, t^{♯}), (t^{♯}, s^{♯})}

has the stuttering property, but R̂ has additionally the pairs (s^{♭}, t^{♭}) and (t^{♭}, s^{♭}).

Lemma 3.7. The stuttering closure R̂ of a symmetric binary relation R is symmetric.

Proof Suppose s R̂ t; then there exist states s^{♭}, s^{♯}, t^{♭} and t^{♯} such that s^{♭} −↠ s −↠ s^{♯}, t^{♭} −↠ t −↠ t^{♯}, s^{♭} R t^{♯} and s^{♯} R t^{♭}. Since R is symmetric, it follows that t^{♭} R s^{♯} and t^{♯} R s^{♭}. Hence t R̂ s. □

Lemma 3.8. Let R̂ be the stuttering closure of R. If R satisfies (T) and s R̂ t, then there exists t′ such that t −↠ t′ and s R t′.

Proof Suppose s R̂ t; then there exist states s^{♭}, s^{♯}, t^{♭} and t^{♯} such that s^{♭} −↠ s −↠ s^{♯}, t^{♭} −↠ t −↠ t^{♯}, s^{♭} R t^{♯} and s^{♯} R t^{♭}. From s^{♭} R t^{♯} and s^{♭} −↠ s it follows by Lemma 3.2 that there exists t′ such that (t −↠) t^{♯} −↠ t′ and s R t′. □

Lemma 3.9. If R satisfies (T), then so does its stuttering closure R̂.

Proof Suppose that s R̂ t and that s ⟶^{a} s′ for some s′. Then by Lemma 3.8 there exists t^{†} such that t −↠ t^{†} and s R t^{†}. Hence, since s ⟶^{a} s′, it follows by (T) that there exist states t′′ and t′ such that

(t −↠) t^{†} −↠ t′′ ⟶^{(a)} t′, s R t′′ and s′ R t′ .

Now, s R t′′ and s′ R t′ respectively imply s R̂ t′′ and s′ R̂ t′. □

3.4. Closing the cycle of inclusions

Using the notion of stuttering closure we can now prove \underline{↔}_{b}^{Δ_{0}} ⊆ \underline{↔}_{b}^{Δ_{1}}, thereby closing the cycle of inclusions. To prove the inclusion we establish that if R is a witnessing relation for \underline{↔}_{b}^{Δ_{1}}, then R̂ is a witnessing relation for \underline{↔}_{b}^{Δ_{0}}.

Lemma 3.10. If R satisfies (T) and (D_{0}), then R̂ satisfies (D′_{1}).

Proof Suppose that s R̂ t and there exists an infinite sequence of states (s_{k})_{k∈ω} such that s = s_{0} and s_{k} ⟶^{τ} s_{k+1} for all k ∈ ω. We have to show that there exists a state t′ such that t ⟶^{τ} t′ and s_{k} R̂ t′ for some k ∈ ω.

As s R̂ t, by Lemma 3.8 there exist t_{0}, …, t_{n} such that t = t_{0} ⟶^{τ} ⋯ ⟶^{τ} t_{n} and s R t_{n}. By Lemma 3.6, s R̂ t_{i} for all i = 0, …, n, so if n > 0, then we can take t′ = t_{1}. We proceed with the assumption that n = 0; so s R t.

First suppose that s_{k} R t for all k ∈ ω. Then by condition (D_{0}) there exist t_{0}, …, t_{m} such that t = t_{0} ⟶^{τ} ⋯ ⟶^{τ} t_{m} with m > 0 and s_{k} R t_{m} for some k ∈ ω. As s_{k} R̂ t_{0} and s_{k} R̂ t_{m}, it follows by Lemma 3.6 that s_{k} R̂ t_{i} for all i = 0, …, n. Hence, in particular, s_{k} R̂ t_{1}, so we can take t′ = t_{1}.

In the remaining case there is a k_{0} ∈ ω such that s_{k} R t for all k ≤ k_{0} while s_{k_{0}+1} and t are not related by R. Since s_{k_{0}} R t and s_{k_{0}} ⟶^{τ} s_{k_{0}+1}, by condition (T) of Definition 2.1 there exist states

t_{0}, …, t_{m}, t_{m+1} such that t = t_{0} ⟶^{τ} ⋯ ⟶^{τ} t_{m} ⟶^{(τ)} t_{m+1}, s_{k_{0}} R t_{m} and s_{k_{0}+1} R t_{m+1}. Since s_{k_{0}+1}

and t are not related by R, it follows that t_{0} ≠ t_{m+1}, so either m > 0 or t_{m} ⟶^{τ} t_{m+1}. In case m > 0, since s_{k_{0}} R̂ t_{0} and s_{k_{0}} R̂ t_{m}, by Lemma 3.6 it follows that s_{k_{0}} R̂ t_{1}, so we can take t′ = t_{1}. In case m = 0 and t = t_{m} ⟶^{τ} t_{m+1}, we can take t′ = t_{m+1}. □

Theorem 3.3. \underline{↔}_{b}^{Δ_{0}} ⊆ \underline{↔}_{b}^{Δ_{1}}.

Proof Suppose that s \underline{↔}_{b}^{Δ_{0}} t. Then there exists a binary relation R satisfying (T) and (D_{0}), such that s R t. By Lemma 3.7 the stuttering closure R̂ of R is symmetric, by Lemma 3.9 it satisfies (T), and by Lemma 3.10 and Proposition 2.1 it satisfies (D_{1}). Moreover, s R̂ t. Hence, s \underline{↔}_{b}^{Δ_{1}} t. □

Corollary 3.1. \underline{↔}_{b}^{Δ} = \underline{↔}_{b}^{Δ_{0}} = \underline{↔}_{b}^{Δ_{1}}. □

Corollary 3.2. The relation \underline{↔}_{b}^{Δ} is an equivalence relation. □

Recall that the proof strategy employed in Lemma 3.1(ii) to show that any union of binary relations satisfying (D_{1}) also satisfies (D_{1}), fails with (D) or (D_{0}) instead of (D_{1}). In fact, it is easy to show that these results do not even hold. Therefore, we could not directly infer from the definition of \underline{↔}_{b}^{Δ} that it is itself a branching bisimulation with explicit divergence. But now it follows, for \underline{↔}_{b}^{Δ} = \underline{↔}_{b}^{Δ_{1}} satisfies (T) and (D_{1}) by Lemma 3.4, and hence also the weaker condition (D_{0}). It satisfies (D) by Lemma 3.5.

Corollary 3.3. \underline{↔}_{b}^{Δ} is the largest symmetric relation satisfying (T) and (D_{0}). It even satisfies (D), (D_{1}) and (D′_{1}). It therefore is the largest branching bisimulation with explicit divergence. □

The following corollary is another consequence, which we need in the next section.

Corollary 3.4. The relation \underline{↔}_{b}^{Δ} has the stuttering property.

Proof Since \underline{↔}_{b}^{Δ} satisfies (T) and (D_{0}), its stuttering closure ˆ \underline{↔}_{b}^{Δ} satisfies (T) and (D_{1}) by Lemmas 3.9 and 3.10 and Proposition 2.1. Moreover, ˆ \underline{↔}_{b}^{Δ} is symmetric by Lemma 3.7. Therefore ˆ \underline{↔}_{b}^{Δ} is included in \underline{↔}_{b}^{Δ_{1}} (cf. the proof of Lemma 3.4). As \underline{↔}_{b}^{Δ} ⊆ ˆ \underline{↔}_{b}^{Δ} ⊆ \underline{↔}_{b}^{Δ_{1}} we find \underline{↔}_{b}^{Δ} = ˆ \underline{↔}_{b}^{Δ}. Thus, by Lemma 3.6, \underline{↔}_{b}^{Δ} has the stuttering property. □

4. Defining BB^{Δ} in terms of coloured traces

A path from a state s is an alternating sequence s_{0}, a_{1}, s_{1}, a_{2}, s_{2}, …, a_{n}, s_{n} of states and actions, such

that s = s_{0} and s_{k−1} ⟶^{a_{k}} s_{k} for k = 1, …, n.

Definition 4.1. A colouring is an equivalence relation on S. Given a colouring C and a state s ∈ S, the colour C(s) of s is the equivalence class containing s.

For π = s_{0}, a_{1}, s_{1}, …, a_{n}, s_{n} a path from s, let C(π) be the alternating sequence of colours and actions obtained from C(s_{0}), a_{1}, C(s_{1}), …, a_{n}, C(s_{n}) by contracting all subsequences C, τ, C, τ, …, τ, C to C. The sequence C(π) is called a C-coloured trace of s. A colouring C is consistent if two states of the same colour always have the same C-coloured traces.

A state s is C-divergent if there exists an infinite sequence of states (s_{k})_{k∈ω} such that s = s_{0}, s_{k} ⟶^{τ} s_{k+1} and C(s_{k}) = C(s) for all k ∈ ω. A consistent colouring is said to preserve divergence if no C-divergent state has the same colour as a nondivergent state.

We write s ≡_{c} t if there exists a consistent colouring C with C(s) = C(t), and s ≡_{c}^{Δ} t if there exists a consistent, divergence preserving colouring C with C(s) = C(t).

In [6] it is shown that ≡_{c} = \underline{↔}_{b}. Here we show that ≡_{c}^{Δ} = \underline{↔}_{b}^{Δ}.

Lemma 4.1. Let C be a colouring such that two states with the same colour have the same C-coloured traces of length three (i.e. colour - action - colour). Then C is consistent.

Proof Suppose C(s_{0}) = C(t_{0}) and C_{0}, a_{1}, C_{1}, …, a_{n}, C_{n} is a coloured trace of s_{0}. Then, for i = 1, …, n, there are states s_{i} and paths π_{i} from s_{i−1} to s_{i}, such that C(π_{i}) = C_{i−1}, a_{i}, C_{i}. With induction on i, for i = 1, …, n we find states t_{i} with C(s_{i}) = C(t_{i}) and paths ρ_{i} from t_{i−1} to t_{i} such that C(ρ_{i}) = C_{i−1}, a_{i}, C_{i}. Namely, the assumption about C allows us to find ρ_{i} given t_{i−1}, and then t_{i} is defined as the last state of ρ_{i}. Concatenating all the paths ρ_{i} yields a path ρ from t_{0} with C(ρ) = C_{0}, a_{1}, C_{1}, …, a_{n}, C_{n}.

□

Theorem 4.1. ≡_{c}^{Δ} = \underline{↔}_{b}^{Δ}.

Proof “⊆”: Let C be a consistent colouring that preserves divergence. It suffices to show that C is a branching bisimulation with explicit divergence.

Suppose s C t, i.e. C(s) = C(t), and s ⟶^{a} s′ for some state s′. In case a = τ and C(s′) = C(s) we have s′ C t and condition (T) is satisfied. So suppose a ≠ τ or C(s′) ≠ C(s). Then s, and therefore also t, has a coloured trace C(s), a, C(s′). This implies that there are states t_{0}, …, t_{n} for some n ≥ 0 and t′

with t = t_{0} ⟶^{τ} t_{1} ⟶^{τ} ⋯ ⟶^{τ} t_{n} ⟶^{(a)} t′ such that C(t_{i}) = C(s) for i = 0, ..., n and C(t′) = C(s′). Hence

(T) is satisfied.

Now suppose s C t and there is an infinite sequence of states (s_{k})_{k∈ω} such that s = s_{0}, s_{k} ⟶^{τ} s_{k+1} and s_{k} C t for all k ∈ ω. Then C(s_{k}) = C(s) for all k ∈ ω. Hence s, and therefore also t, is C-divergent. Thus there exists an infinite sequence of states (t_{l})_{l∈ω} such that t = t_{0}, t_{l} ⟶^{τ} t_{l+1} and C(t_{l}) = C(t) for all l ∈ ω. It follows that s_{k} C t_{l} for all k, l ∈ ω. Hence also (D) is satisfied.

“⊇”: It suffices to show that \underline{↔}_{b}^{Δ} is a consistent, divergence preserving colouring. By Corollary 3.2 it is an equivalence relation. We also use that it satisfies (T) and (D) (Corollary 3.3) and has the stuttering property (Corollary 3.4). We invoke Lemma 4.1 for proving consistency.

Suppose that s and t have the same colour, i.e., s \underline{↔}_{b}^{Δ} t, and let C, a, D be a \underline{↔}_{b}^{Δ}-coloured trace of s. Then a ≠ τ or C ≠ D, and there are states s′′ and s′ with s −↠ s′′ ⟶^{a} s′, such that s′′, s ∈ C and s′ ∈ D. As \underline{↔}_{b}^{Δ} satisfies (T), by Lemma 3.2 there is a state t^{†} with t −↠ t^{†} and s′′ \underline{↔}_{b}^{Δ} t^{†}. Therefore there exist states t′′ and t′ such that (t−↠) t^{†} −↠ t′′ ⟶^{(a)} t′, s′′ \underline{↔}_{b}^{Δ} t′′ and s′ \underline{↔}_{b}^{Δ} t′. As \underline{↔}_{b}^{Δ} has the stuttering property and t′′ \underline{↔}_{b}^{Δ} s′′ \underline{↔}_{b}^{Δ} s \underline{↔}_{b}^{Δ} t, all states on the τ-path from t to t′′ have the same colour as s. Hence C, a, D is a \underline{↔}_{b}^{Δ}-coloured trace of t.

Now suppose s and t have the same colour and s is \underline{↔}_{b}^{Δ}-divergent. Then there is an infinite sequence of states (s_{k})_{k∈ω} such that s = s_{0}, s_{k} ⟶^{τ} s_{k+1} and s_{k} \underline{↔}_{b}^{Δ} s \underline{↔}_{b}^{Δ} t for all k ∈ ω. As \underline{↔}_{b}^{Δ} satisfies (D), this implies that there exists an infinite sequence of states (t_{l})_{l∈ω} such that t = t_{0}, t_{l} ⟶^{τ} t_{l+1} and s_{k} \underline{↔}_{b}^{Δ} t_{l} for all k, l ∈ ω. It follows that t_{l} \underline{↔}_{b}^{Δ} t for all l ∈ ω, and hence t is \underline{↔}_{b}^{Δ}-divergent. □

5. Modal characterisations of BB^{Δ}

We shall now establish agreement between the relational and modal characterisations of BB^{Δ} proposed in [4]. The class of formulas Φ_{jb}^{Δ} of the modal logic for BB^{Δ} proposed in [4] is generated by the following grammar:

φ ::= ¬φ | ⋀ Φ | φ a φ | Δφ  (a ∈ A, φ ∈ Φ_{jb}^{Δ} and Φ ⊆ Φ_{jb}^{Δ}).  (1)

In case the cardinality |S| of the set of states of our labelled transition system is less than some infinite cardinal κ, we may require that |Φ| < κ in conjunctions, thus obtaining a set of formulas rather than a proper class. We shall use the following standard abbreviations: ⊤ = ⋀ ∅, ⊥ = ¬⊤ and ⋁ Φ = ¬ ⋀{¬φ | φ ∈ Φ}.

We define when a formula φ is valid in a state s (notation: s ⊧ φ) inductively as follows:

(i) s ⊧ ¬φ iff s |̸= φ;

(ii) s ⊧ ⋀ Φ iff s ⊧ φ for all φ ∈ Φ;

(iii) s ⊧ φ a ψ iff there exist states s′ and s′′ such that s −↠ s′′ ⟶^{(a)} s′, s′′ ⊧ φ and s′ ⊧ ψ;

(iv) s ⊧ Δφ iff there exists an infinite sequence (s_{k})_{k∈ω} of states such that s −↠ s_{0}, s_{k} ⟶^{τ} s_{k+1} and s_{k} ⊧ φ for all k ∈ ω.

Validity induces an equivalence on states: we define ∼ ⊆ S × S by

s ∼ t iff ∀φ ∈ Φ_{jb}^{Δ}. s ⊧ φ ⇔ t ⊧ φ .

We shall now establish that ∼ coincides with \underline{↔}_{b}^{Δ}.

Theorem 5.1. For all states s and t: s \underline{↔}_{b}^{Δ} t iff s ∼ t.

Proof To establish the implication from left to right, we prove by structural induction on φ that if s \underline{↔}_{b}^{Δ} t and s ⊧ φ, then t ⊧ φ. We only treat the cases φ = ψ a χ and φ = Δψ; the other two cases are trivial.

1. Suppose φ = ψa χ and s ⊧ φ. Then there exist states s′ and s′′ such that s −↠ s′′ ⟶^{(a)} s′, s′′ ⊧ ψ and s′ ⊧ χ. By Lemma 3.2, there exists a state t^{†} such that t −↠ t^{†} and s′′ \underline{↔}_{b}^{Δ} t^{†}. From this it follows that there exist states t′ and t′′ such that t −↠ t′′ ⟶^{(a)} t′, s′′ \underline{↔}_{b}^{Δ} t′′ and s′ \underline{↔}_{b}^{Δ} t′, for if a = τ and s′ = s′′ we can take t′ = t′′ = t^{†} and otherwise, since s′′ \underline{↔}_{b}^{Δ} t^{†}, the states t′ and t′′ exist by (T). It follows by the induction hypothesis that t′′ ⊧ ψ and t′ ⊧ χ, and hence t ⊧ φ.

2. Suppose φ = Δψ and s ⊧ φ. Then there exists an infinite sequence (s_{k})_{k∈ω} such that s −↠ s_{0}, s_{k} ⟶^{τ} s_{k+1} and s_{k} ⊧ ψ for all k ∈ ω. By Lemma 3.2, there exists a state t_{0} such that t −↠ t_{0} and s_{0} \underline{↔}_{b}^{Δ} t_{0}. From Corollary 3.3 it follows that \underline{↔}_{b}^{Δ} satisfies (D_{1}), so there exist an infinite sequence of states (t_{l})_{l∈ω} and a mapping σ : ω → ω such that t_{l} ⟶^{τ} t_{l+1} and s_{σ(l)} \underline{↔}_{b}^{Δ} t_{l} for all l ∈ ω. By the induction hypothesis t_{l} ⊧ ψ for all l ∈ ω, and hence t ⊧ φ.

For the implication from right to left, it suffices by Corollary 3.1 to prove that ∼ is symmetric and satisfies the conditions (T) and (D_{0}).

That ∼ is symmetric is clear from its definition.

To establish condition (T) of Definition 2.1, suppose that s ∼ t and s ⟶^{a} s′, and define sets T′′ and T′ as follows:

T′′ = {t′′ ∈ S | t −↠ t′′ & s ≁ t′′}; and

T′ = {t′ ∈ S | ∃t′′ ∈ S. t −↠ t′′ ⟶^{(a)} t′ & s′ ≁ t′} .

For each t′′ ∈ T′′ let φ_{t′′} be a formula such that s ⊧ φ_{t′′} and t′′ |̸= φ_{t′′}, and let φ = ⋀{φ_{t′′} | t′′ ∈ T′′}. Similarly, for each t′ ∈ T′ let ψ_{t′} be a formula with s′ ⊧ ψ_{t′} and t′ |̸= ψ_{t′}, and let ψ = ⋀{ψ_{t′} | t′ ∈ T′}. Note that s ⊧ φ a ψ, and hence, since s ∼ t, also t ⊧ φ a ψ. So, there exist states t′ and t′′ such that

t −↠ t′′ ⟶^{(a)} t′, t′′ ⊧ φ and t′ ⊧ ψ. From t′′ ⊧ φ it follows that t′′ ∉ T′′, so s ∼ t′′; from t′ ⊧ ψ it

follows that t′ ∉ T′, so s′ ∼ t′. Thereby, condition (T) is established.

To establish condition (D_{0}), suppose that s ∼ t and that there exists an infinite sequence (s_{k})_{k∈ω} such that s = s_{0}, s_{k} ⟶^{τ} s_{k+1} and s_{k} ∼ t for all k ∈ ω. Define the set T^{∞} by

T^{∞} = {t′ ∈ S | t −↠ t′ & s ≁ t′} .

For each t′ ∈ T^{∞} let φ_{t′} be a formula such that s ⊧ φ_{t′} and t′ |̸= φ_{t′}, and let φ = ⋀{φ_{t′} | t′ ∈ T^{∞}}. Since s_{0} = s ⊧ φ and s_{k} ∼ t ∼ s, it follows that s_{k} ⊧ φ for all k ∈ ω, and therefore s ⊧ Δφ. Hence, t ⊧ Δφ, so there exists an infinite sequence (t_{ℓ})_{ℓ∈ω} such that t −↠ t_{0}, t_{ℓ} ⟶^{τ} t_{ℓ+1} and t_{ℓ} ⊧ φ for all ℓ ∈ ω. It follows that t_{ℓ} ∉ T^{∞}, so s ∼ t_{ℓ}, for all ℓ ∈ ω, and hence s_{k} ∼ s ∼ t_{ℓ} for all k, ℓ ∈ ω. It follows, in particular, that t ⟶^{+} t_{1} and s_{k} ∼ t_{1} for some k ∈ ω. Thereby, also condition (D_{0}) is established. □

Clause (iii) in the definition of validity appears to be rather liberal. More stringent alternatives are obtained by using φ ⟨â⟩ ψ or φ ⟨a⟩ ψ instead of φ a ψ, with the following definitions:

(iii′) s ⊧ φ ⟨â⟩ ψ iff either a = τ and s ⊧ ψ, or there exists a sequence of states s_{0}, …, s_{n}, s_{n+1}

(n ≥ 0) such that s = s_{0} ⟶^{τ} ⋯ ⟶^{τ} s_{n} ⟶^{a} s_{n+1}, s_{i} ⊧ φ for all i = 0, …, n and s_{n+1} ⊧ ψ.

(iii′′) s ⊧ φ⟨a⟩ψ iff there exists states s_{0}, …, s_{n}, s_{n+1} (n ≥ 0) such that s = s_{0}⟶^{τ}⋯⟶^{τ}s_{n}⟶^{(a)}s_{n+1},

s_{i} ⊧ φ for all i = 0, …, n and s_{n+1} ⊧ ψ.

The modality ⟨â⟩ stems from De Nicola & Vaandrager [2]. There it was shown, for labelled transition systems with bounded nondeterminism, that branching bisimulation equivalence, \underline{↔}_{b}, is characterised by the logic with negation, binary conjunction and this until modality. The modality ⟨a⟩ is a common strengthening of ⟨â⟩ and the just-before modality a above; it was first considered in [4]. Henceforth we denote by Φ_{u}^{Δ} the set of formulas generated by the grammar in (1) with φ a φ replaced by φ ⟨a⟩ φ.

Definition 5.1. Two modal formulas φ and ψ that are interpreted on states of labelled transition systems are globally equivalent, written φ ⇚⇛ ψ, if s ⊧ φ ⇔ s ⊧ ψ for all states s in all labelled transition systems. Two modal logics are equally expressive if for any formula in the one there is a globally equivalent formula in the other.

As remarked in [4], the modalities ⟨â⟩ and ⟨a⟩ are equally expressive, since

φ ⟨τ̂⟩ ψ ⇚⇛ ψ ∨ φ ⟨τ⟩ ψ ,
φ ⟨τ⟩ ψ ⇚⇛ φ ∧ φ ⟨τ̂⟩ ψ and
φ ⟨a⟩ ψ ⇚⇛ φ ⟨â⟩ ψ  for all a ≠ τ.

Note that the modality a can be expressed in terms of ⟨a⟩:

φ a ψ ⇚⇛ ⊤ ⟨τ⟩ (φ ⟨a⟩ ψ) .

Laroussinie, Pinchinat & Schnoebelen established in [7] that the modal logic with negation, binary conjunction and ⟨â⟩ and the logic with negation, binary conjunction and a are equally expressive. Below, we adapt their method to show that replacing a by ⟨â⟩ or ⟨a⟩ in the modal logic for BB^{Δ} proposed in [4] also yields an equally expressive logic. The central idea, from [7], is that any formula in Φ_{jb}^{Δ} can be written as a Boolean combination of formulas that propagate either upwards or downwards along a path of τ-transitions. A formula φ that propagates upwards, i.e., with the property that if s −↠ t and s ⊧ φ, then also t ⊧ φ, we shall call an upward formula. A formula φ that propagates downwards, i.e., with the property that if s −↠ t and t ⊧ φ, then also s ⊧ φ, we shall call a downward formula.

Lemma 5.1. Every φ ∈ Φ_{jb}^{Δ} is globally equivalent with a formula of the form ⋁ Φ, where each formula in Φ is a conjunction of an upward and a downward formula.

Proof Note that ψ a χ and Δψ are downward formulas and that the negation of a downward formula is an upward formula. Furthermore, a conjunction of upward formulas is again an upward formula and a conjunction of downward formulas is again a downward formula. It follows, by the standard laws of Boolean algebra, that the formula φ is equivalent to a formula of the desired shape. □

The proof that for every formula φ ∈ Φ_{u}^{Δ} there exists a globally equivalent formula φ′ ∈ Φ_{jb}^{Δ} proceeds by induction on the structure of φ, and the only nontrivial case is when φ = ψ ⟨a⟩ χ. According to the induction hypothesis, for ψ and χ there exist equivalent formula in Φ_{jb}^{Δ}, so, by Lemma 5.1, ψ is equivalent to a disjunction of conjunctions of upward and downward formulas. The proof in [7] then relies on these disjunctions being finite. To generalise it to infinite disjunctions, we shall use the following lemma.

Lemma 5.2. Let Φ be a set of formulas and let φ be a formula. Then

(⋁ Φ) ⟨a⟩ φ ⇚⇛ ⋁ {(⋁ Φ′) ⟨a⟩ φ | Φ′ a finite subset of Φ} .

Proof

(⇛) Suppose s ⊧ (⋁ Φ) ⟨a⟩ φ. Then there exist states s_{0}, …, s_{n}, s_{n+1} such that s = s_{0} ⟶^{τ} ⋯ ⟶^{τ} s_{n} ⟶^{(a)}s_{n+1}, s_{i} ⊧ ⋁ Φ for all i = 0, …, n and s_{n+1} ⊧ φ. Since s_{i} ⊧ ⋁ Φ, we can associate with every s_{i} (i = 0, …, n) a formula φ_{i} ∈ Φ such that s_{i} ⊧ φ_{i}. Let Φ′ = {φ_{i} | i = 0, …, n}; then Φ′ is a finite subset of Φ such that s_{i} ⊧ ⋁ Φ′ for every i = 0, …, n. It follows that s ⊧ (⋁ Φ′)⟨a⟩φ, and hence s ⊧ ⋁{(⋁ Φ′) ⟨a⟩ φ | Φ′ a finite subset of Φ}.

(⇚) If s ⊧ ⋁{(⋁ Φ′) ⟨a⟩ φ | Φ′ a finite subset of Φ}, then s ⊧ (⋁ Φ′) ⟨a⟩ φ for some finite subset Φ′

of Φ. So there exist states s_{0}, …, s_{n}, s_{n+1} such that s = s_{0} ⟶^{τ} ⋯ ⟶^{τ} s_{n} ⟶^{(a)} s_{n+1}, s_{i} ⊧ ⋁ Φ′

for all i = 0, …, n and s_{n+1} ⊧ φ. Since s_{i} ⊧ ⋁ Φ′ implies s_{i} ⊧ ⋁ Φ for all i = 0, …, n, it follows that s ⊧ (⋁ Φ) ⟨a⟩ φ. □

We now adapt the method in [7] and show that replacing a by ⟨â⟩ or ⟨a⟩ in the modal logic for BB^{Δ} proposed in [4] yields an equally expressive logic.

Theorem 5.2. For every formula φ ∈ Φ_{u}^{Δ} there exists a globally equivalent formula φ′ ∈ Φ_{jb}^{Δ}.

Proof The proof is by structural induction on φ; the only nontrivial case is when φ = ψ ⟨a⟩ χ. By the induction hypothesis there exist formulas ψ′, χ′ ∈ Φ_{jb}^{Δ} such that ψ ⇚⇛ ψ′ and χ ⇚⇛ χ′. By Lemma 5.1, ψ′ ⇚⇛ ⋁ Ψ, where each formula in Ψ is a conjunction of an upward and a downward formula. Hence, by the evident congruence property of ⇚⇛ and Lemma 5.2,

φ ⇚⇛ ⋁ {(⋁ Ψ′) ⟨a⟩ χ′ | Ψ′ a finite subset of Ψ} .

Clearly, it now suffices to establish that (⋁ Ψ′) ⟨a⟩ χ′ is globally equivalent to a formula in Φ_{jb}^{Δ}, for all finite subsets Ψ′ of Ψ. Recall that Ψ consists of conjunctions of an upward and a downward formula, so we can assume that Ψ′ = {ψ_{i}^{u} ∧ ψ_{i}^{d} | i = 1, …, n}; we proceed by induction on the cardinality of Ψ′. If |Ψ′| = 0, then

(⋁ Ψ′) ⟨a⟩ χ′ ⇚⇛ ⊥ ,

and ⊥ ∈ Φ_{jb}^{Δ}. Suppose |Ψ′| > 0. By the induction hypothesis there exists, for every i = 1, …, n, a formula φ′_{i} such that

(⋁ Ψ′ − {ψ_{i}^{u} ∧ ψ_{i}^{d}}) ⟨a⟩ χ′ ⇚⇛ φ′_{i} .

Then, it is easy to verify that

(⋁ Ψ′) ⟨a⟩ χ′ ⇚⇛ ⋁_{i=1}^{n} (ψ_{i}^{u} ∧ (ψ_{i}^{d} a χ′ ∨ ψ_{i}^{d} τ φ′_{i})) ,

and the right-hand side formula is in Φ_{jb}^{Δ}. Some intuition for this last step is offered in [7]. □

s_{1}  s_{2}  s_{3} τ  τ τ τ s = s_{0}  a_{2}  a_{3}  a_{4} a_{1} b_{0}  b_{1}  b_{2}  b_{3} t_{1}  t_{2}  t_{3} t_{0} u^{0}  u^{1}  u^{2}  u^{3}

Figure 3. A divergence.

In the same vain, there is also an obvious strengthening of the divergence modality Δ. Let Δ̂ be the unary divergence modality with the following definition:

(iv′) s ⊧ Δ̂φ iff there exists an infinite sequence (s_{k})_{k∈ω} of states such that s = s_{0}, s_{k} ⟶^{τ} s_{k+1} and s_{k} ⊧ φ for all k ∈ ω.

We denote by ΦΔ̂ ; jb the set of formulas generated by the grammar in (1) with Δφ replaced by Δ̂φ. Note that the modality Δ can be expressed in terms of Δ̂:

Δφ ⇚⇛ ⊤ τ Δ̂φ .

A crucial step in our adaptation of the method of Laroussinie, Pinchinat & Schnoebelen above consisted of showing that infinite disjunctions in the left argument of ⟨a⟩ can be avoided. If infinite disjunctions could also be avoided as an argument of Δ̂, then a further adaptation of the method would be possible, showing that replacing Δ by Δ̂ in the modal logic for BB^{Δ} would yield a logic with equal expressivity. However, the following example suggests that infinite disjunctions under Δ̂ cannot always be avoided.

Example 5.1. For a_{1}, a_{2}, a_{3}, … and b_{0}, b_{1}, b_{2}, … be infinite sequences of distinct actions and consider the formula

φ = Δ̂ (⋁_{i=0}^{∞} (¬ (⊤ ⟨a_{i}⟩ ⊤) ∧ (⊤ ⟨b_{i}⟩ ⊤))) .

The formula φ holds in a state iff there exists an infinite τ-path such that in every state there is an i ≥ 0 such that the action b_{i} is still possible, whereas the action a_{i} is not. Note that φ holds in the state s of the transition system in Figure 3; each of the disjuncts ¬ (⊤ ⟨a_{i}⟩ ⊤) ∧ (⊤ ⟨b_{i}⟩ ⊤) holds in precisely one state.

We conjecture that the formula of Example 5.1 is not globally equivalent to a formula in Φ_{jb}^{Δ}, and that, hence, replacing Δ by Δ̂ in the modal logic for BB^{Δ} yields a strictly more expressive logic. We conclude the paper with a proof that the equivalence ∼′ ⊆ S × S induced on states by validity of formulas in ΦΔ̂ ; jb, defined by

s ∼′ t iff ∀φ ∈ ΦΔ̂ ; jb. s ⊧ φ ⇔ t ⊧ φ ,

nevertheless also coincides with \underline{↔}_{b}^{Δ}.

Theorem 5.3. For all states s and t: s \underline{↔}_{b}^{Δ} t iff s ∼′ t.

Proof For the implication from left to right, we prove by structural induction on φ that if s \underline{↔}_{b}^{Δ} t and s ⊧ φ, then t ⊧ φ. We only treat the case φ = Δ̂ψ, for the case φ = ψ a χ is already treated in the proof of Theorem 5.1 and the other two cases are trivial. So, suppose φ = Δ̂ψ and s ⊧ φ. Then there exists an infinite sequence (s_{k})_{k∈ω} of states such that s = s_{0}, s_{k} ⟶^{τ} s_{k+1} and s_{k} ⊧ ψ for all k ∈ ω. From Corollary 3.3 it follows that \underline{↔}_{b}^{Δ} satisfies (D_{1}), so there exist an infinite sequence of states (t_{l})_{l∈ω} and a mapping σ : ω → ω such that t = t_{0}, t_{l} ⟶^{τ} t_{l+1} and s_{σ(l)} \underline{↔}_{b}^{Δ} t_{l} for all l ∈ ω. By the induction hypothesis t_{l} ⊧ ψ for all l ∈ ω, and hence t ⊧ φ.

To establish the implication from right to left, note that if s ∼′ t, then, since every formula in Φ_{jb}^{Δ} is equivalent to a formula in ΦΔ̂ ; jb, also s ∼ t, so by Theorem 5.1 it follows that s \underline{↔}_{b}^{Δ} t. □

Comment on Definition 5.1 If in Definition 5.1 we had used a notion of equivalence between modal formulas φ and ψ that merely requires that s ⊧ φ ⇔ s ⊧ ψ for all states s in the presupposed labelled transition system, rather than quantifying over all labelled transition systems, the resulting concept of equally expressive logics would be much weaker, and the logics Φ_{jb}^{Δ} and ΦΔ̂ ; jb would be equally expressive.

In general, let ∼ be an equivalence relation on the set of states S, and consider two logics L_{1} and L_{2} that both have negation and arbitrary infinite conjunction, and both characterise ∼. For every pair of states s, t ∈ S with s ≁ t take a formula φ_{s,t} from L_{1} such that s ⊧ φ_{s,t} but t |̸= φ_{s,t}. Then χ_{s} = ⋀{φ_{s,t} | t ≁ s} is called a characteristic formula of s: one has t ⊧ χ_{s} iff t ∼ s. Now let ψ be a formula from L_{2}. Then ⋁{χ_{s} | s ⊧ ψ} is equivalent to ψ, in the sense that for all states t ∈ S we have t ⊧ ψ ⇔ t ⊧ ⋁{χ_{s} | s ⊧ ψ}. This proves that the two logics are equally expressive.

Similar reasoning using the notion of global equivalence from Definition 5.1 would break down, because one cannot take conjunctions of a proper class of formula.

References

[1] T. Basten (1996): Branching bisimulation is an equivalence indeed! Information Processing Letters 58(3), pp. 141–147.

[2] R. De Nicola & F.W. Vaandrager (1995): Three logics for branching bisimulation. Journal of the ACM 42(2), pp. 458–487.

[3] R. Gerth, R. Kuiper, D. Peled & W. Penczek (1999): A partial order approach to branching time logic model checking. Information and Computation 150(2), pp. 132–152.

[4] R.J. van Glabbeek (1993): The linear time - branching time spectrum II. In E. Best, editor: Proceedings CONCUR’93, LNCS 715, Springer, pp. 66–81.

[5] R.J. van Glabbeek, B. Luttik & N. Trčka: Computation tree logic and deadlock detection. Submitted. Available

   at http://theory.stanford.edu/~rvg/abstracts.html#73.

[6] R.J. van Glabbeek & W.P. Weijland (1996): Branching time and abstraction in bisimulation semantics. Journal of the ACM 43(3), pp. 555–600.

[7] F. Laroussinie, S. Pinchinat & Ph. Schnoebelen (1995): Translations between modal logics of reactive systems. Theoretical Computer Science 140(1), pp. 53–71.

[8] S. Nejati (2003): Refinement relations on partial specifications. Master’s thesis, University of Toronto.