Branching Bisimulation with Explicit Divergence

Rob van Glabbeek^{1}

National ICT Australia, Sydney, Australia

School of Computer Science and Engineering, Univ. of New South Wales, Sydney

Bas Luttik^{2}

Dept. of Math. and Comput. Sci. Technische Universiteit Eindhoven, The Netherlands

CWI, The Netherlands

Nikola Trčka^{3}

Dept. of Math. and Comput. Sci. 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 an action-based modal logic with until modality and explicit divergence.

Key words: Branching bisimulation, divergence, coloured traces.

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

1 Email: rvg@cs.stanford.edu
2 Email: s.p.luttik@tue.nl
3 Email: n.trcka@tue.nl

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 of the relational and modal characterisation from [4], and also provide a different modal characterisation of BB^{Δ}, in the style of [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′) ∈ →; we abbreviate the statement ‘s ⟶^{a} s′ or (a = τ and s = s′)’ by s ⟶^{(a)} s′; and we denote by ↠ the reflexive-transitive closure of the binary relation ⟶^{τ} on S.

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]. 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, has the so-called stuttering property, and can equivalently be defined by replacing (D) by any of the following alternatives:

(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 ∈ ω.

(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 ∈ ω.

(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}^{Δ_{0}} t, respectively s \underline{↔}_{b}^{Δ_{1}} t, if there exists a symmetric binary relation R satisfying (T) and (D_{0}), respectively (D_{1}), such that s R t. Note that (D_{0}) is a weaker requirement than either (D) or (D′_{1}); hence \underline{↔}_{b}^{Δ} ⊆ \underline{↔}_{b}^{Δ_{0}} and \underline{↔}_{b}^{Δ_{1}} ⊆ \underline{↔}_{b}^{Δ_{0}}. Condition (D_{0}) appears in a definition of divergence-sensitive stuttering simulation in [7]. Condition (D_{1}) is a technically convenient reformulation of (D′_{1}) that shows more clearly how the condition preserves divergence (infinite sequences of τ-transitions).

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

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

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

(i) Suppose that R_{i} satisfies (T) for 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 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

(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_{1} ; R_{2} 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.4 \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}^{Δ}

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

Proof. By definition, \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, \underline{↔}_{b}^{Δ_{1}} is the largest symmetric binary relation satisfying (T) and (D_{1}).

Lemma 3.6 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.5, 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.4, \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.7 \underline{↔}_{b}^{Δ_{1}} ⊆ \underline{↔}_{b}^{Δ}.

Proof. By Theorem 3.4, the relation \underline{↔}_{b}^{Δ_{1}} is symmetric. By Lemma 3.5, it satisfies (T), and by Lemma 3.6 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.8 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 converts any binary relation R on S into a larger relation R̂ that has the stuttering property.

Definition 3.9 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^{♭}} .

Clearly R ⊆ R̂. We establish a few basic properties of the stuttering closure.

Lemma 3.10 The stuttering closure R̂ of a binary relation R has the stuttering property.

Proof. 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}. □

Lemma 3.11 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.12 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.13 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.12 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

Lemma 3.14 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.12 there exist t_{0}, …, t_{n} such that t = t_{0} ⟶^{τ}⋯⟶^{τ}t_{n} and s R t_{n}. By Lemma 3.10, 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. If s_{k} R t for all k ∈ω, then a state t′ with the desired properties exists by condition (D_{0}). The case that remains is where 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.10 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}. □

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

Proof. The implication from left to right is trivial. For the implication from right to left, 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:

(i) We define t_{0} = t and σ(0) = 0; it then clearly holds that s_{σ(0)} R t_{0}. (ii) 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′. □

Theorem 3.16 \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.11 the stuttering closure R̂ of R is symmetric, by Lemma 3.13 it satisfies (T), and by Lemmas 3.14 and 3.15 it satisfies (D_{1}). Moreover, s R̂ t. Hence, s \underline{↔}_{b}^{Δ_{1}} t. □

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

Corollary 3.18 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.5, and hence also the weaker condition (D_{0}). It satisfies (D) by Lemma 3.6.

Corollary 3.19 \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.20 The relation \underline{↔}_{b}^{Δ} has the stuttering property.

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

Remark 3.21 Since \underline{↔}_{b}^{Δ} = \underline{↔}_{b}^{Δ_{0}}, 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.

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 of 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 exist 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.2 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.3 ≡_{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.18 it is an equivalence relation. We also use that it satisfies (T) and (D) (Corollary 3.19) and has the stuttering property (Corollary 3.20). We invoke Lemma 4.2 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^{Δ}

The class of formulas Φ of Hennessy-Milner logic with until, explicit divergence and infinite conjunctions is generated by the following grammar:

φ ::= ¬φ | ⋀ Ψ | φ ⟨a⟩ φ | Δφ (a ∈ A, φ ∈ Φ and Ψ ⊆ Φ).

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 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 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} ⊧ ψ; (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 ∈ ω.

The until modality above stems from De Nicola & Vaandrager [2]. However, instead of our modality ⟨τ⟩ they use ⟨ϵ⟩, whose validity is defined by

(iii) s ⊧ φ⟨ϵ⟩ψ iff either s ⊧ ψ, or there is a sequence of states s_{0}, …, s_{n}, s_{n+1}

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

and s_{n+1} ⊧ ψ.

Using this modality yields an equally expressive language as ours, since

\begin{matrix}s ⊧ φ ⟨ϵ⟩ ψ ⇔ & s ⊧ ψ ∨ φ ⟨τ⟩ ψ and \\ s ⊧ φ ⟨τ⟩ ψ ⇔ & s ⊧ φ ∧ φ ⟨ϵ⟩ ψ . \end{matrix}

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

s ∼ t iff ∀φ ∈ Φ. s ⊧ φ ⟺ t ⊧ φ .

Lemma 5.1 If s \underline{↔}_{b}^{Δ} t and s = s_{0} ⟶^{τ} ⋯ ⟶^{τ} s_{n} ⟶^{(a)} s_{n+1}, then there exist

t_{0}, …, t_{m}, t_{m+1} such that t = t_{0} ⟶^{τ} ⋯ ⟶^{τ} t_{m} ⟶^{(a)} t_{m+1}, s_{n+1} \underline{↔}_{b}^{Δ} t_{m+1} and for

all 0 ≤ i ≤ m there exists 0 ≤ j ≤ n such that s_{j} \underline{↔}_{b}^{Δ} t_{i}.

Proof. First note that by (T), Corollary 3.20 and a straightforward induction on n there exist t_{0}, …, t_{m} such that t = t_{0} ⟶^{τ} ⋯ ⟶^{τ} t_{m} and for all 0 ≤ i ≤ m there exists 0 ≤ j ≤ n such that s_{j} \underline{↔}_{b}^{Δ} t_{i}.

Now, if a = τ and s_{n} = s_{n+1}, then the sequence t_{0}, …, t_{m}, t_{m+1} with t_{m+1} = t_{m} satisfies the lemma. Otherwise, it follows from s_{n} \underline{↔}_{b}^{Δ} t_{m} by (T) and Corollary 3.20 that there exist t′_{0}, …, t′_{k}, t′_{k+1} (k ≥ 0) such that t_{m} =

t′_{0} ⟶^{τ} ⋯ ⟶^{τ} t′_{k} ⟶^{(a)} t′_{k+1}, s_{n} \underline{↔}_{b}^{Δ} t′_{i} for all 0 ≤ i ≤ k and s_{n+1} \underline{↔}_{b}^{Δ} t′_{k+1}; then

the sequence t_{0}, …, t_{m}, t′_{1}, …, t′_{k}, t′_{k+1} satisfies the lemma. □

Theorem 5.2 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.

(i) Suppose φ = ψ ⟨a⟩ χ and s ⊧ φ. Then there exist 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} ⊧ χ. By Lemma 5.1, there exists a se-

quence of states t_{0}, …, t_{m}, t_{m+1} such that t = t_{0} ⟶^{τ} ⋯ ⟶^{τ} t_{m} ⟶^{(a)} t_{m+1},

s_{n+1} \underline{↔}_{b}^{Δ} t_{n+1} and for all i (0 ≤ i ≤ m) there exists j (0 ≤ j ≤ n) such that s_{j} \underline{↔}_{b}^{Δ} t_{i}. From the latter, by the induction hypothesis, it follows that t_{i} ⊧ ψ for all 0 ≤ i ≤ m. From s_{n+1} \underline{↔}_{b}^{Δ} t_{m+1}, by the induction hypothesis, it follows that t_{m+1} ⊧ χ. Hence, t ⊧ φ.

(ii) Suppose φ = Δψ and suppose 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 ∈ ω. From Corollary 3.19 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 ⊧ φ.

For the implication from right to left, we prove that ∼ is a branching bisimulation with explicit divergence.

Clearly, ∼ is symmetric.

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 such that s′ ⊧ ψ_{t′} and t′ |̸= ψ_{t′}, and let ψ = ⋀{ψ_{t′} | t′ ∈ T′}. Note that s ⊧ φ ⟨a⟩ ψ, and hence, since s ∼ t, also t ⊧ φ ⟨a⟩ ψ. So, there exists a sequence of states

t_{0}, …, t_{n}, t_{n+1} such that t = t_{0} ⟶^{τ}⋯⟶^{τ}t_{n} ⟶^{(a)}t_{n+1}, t_{i} ⊧ φ for all i = 0, …, n

and t_{n+1} ⊧ ψ. From t_{n} ⊧ φ it follows that t_{n} ∉ T′′, so s ∼ t_{n}; from t_{n+1} ⊧ ψ it follows that t_{n+1} ∉ T′, so s′ ∼ t_{n+1}. Thereby, condition (T) of Definition 2.1 is established.

To establish condition (D) of Definition 2.1, 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 ℓ ∈ ω. From the latter it follows that t_{ℓ} ∉ T^{∞}, so s ∼ t_{ℓ}, for all ℓ ∈ ω, and hence s_{k} ∼ s ∼ t_{ℓ} for all k, ℓ ∈ ω. □

The modal logic for BB^{Δ} proposed in [4] has, instead of our until modalities, for every a ∈ A a binary modality a, and, instead of our divergence modality, a unary modality Δ′; the validity of these modalities is defined by

(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 ∈ ω.

We denote by ∼′ the equivalence induced on states by validity in the modal logic of [4]. Below we shall establish that ∼′ coincides with \underline{↔}_{b}^{Δ}, using the following modal stuttering property.

Lemma 5.3 Let φ be a formula of the modal logic of [4]. If s ⊧ φ and u ⊧ φ, then t ⊧ φ for all states t such that s −↠ t −↠ u.

Proof. Suppose that s, t and u are states such that s ⊧ φ, u ⊧ φ and s −↠ t −↠ u; we prove that t ⊧ φ with induction on φ.

First, we consider two special cases:

(i) A downward formula is a formula of the form ψ a χ or Δ′ψ. If φ is a downward formula, then it is clear from the definition of validity that if u ⊧ φ, then also t ⊧ φ.

(ii) An upward formula is the negation of a downward formula. Suppose that φ is an upward formula, say φ = ¬ψ with ψ a downward formula, and s ⊧ φ; then s |̸= ψ, so by the previous case and contraposition it follows that t |̸= ψ, and therefore t ⊧ φ.

Since by De Morgan’s laws we can assume that φ is composed from downward and upward formulas by means of (infinite) conjunctions and disjunctions, it remains to consider the cases where φ is a conjunction or a disjunction.

Suppose that φ = ⋀ Ψ. From s ⊧ Ψ and u ⊧ Ψ it follows that s ⊧ ψ and u ⊧ ψ for all ψ ∈ Ψ, so by the induction hypothesis, t ⊧ ψ for all ψ ∈ Ψ. Hence, t ⊧ φ. The proof for the case where φ is a disjunction is similar. □

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

Proof. “Only if”: Note that the modalities from the modal logic of [4] can be expressed in our modal logic:

\begin{matrix}s ⊧ φ a ψ ⇔ & s ⊧ ⊤ ⟨τ⟩ (φ ⟨a⟩ ψ) and \\ s ⊧ Δ′φ ⇔ & s ⊧ ⊤ ⟨τ⟩ (Δφ) . \end{matrix}

So, ∼ ⊆ ∼′ and hence, by Theorem 5.2, it follows that, for all states s and t, if s \underline{↔}_{b}^{Δ} t, then s ∼′ t.

“If”: The proof is similar to the proof for the implication from right to left of Theorem 5.2. Again, it is clear that ∼′ is symmetric, and condition (T) can be established as in the proof of Theorem 5.2, with φ a ψ instead of φ ⟨a⟩ ψ.

To establish condition (D) of Definition 2.1, 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 ∈ ω. Let T^{∞} and φ be defined as in the proof of Theorem 5.2. 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_{ℓ})_{ℓ∈ω} and m ∈ ω such that t = t_{0}, t_{ℓ} ⟶^{τ} t_{ℓ+1} and t_{ℓ} ⊧ φ for all ℓ ≥ m. From s ∼′ t we furthermore obtain t = t_{0} ⊧ φ. Since t_{0} ⊧ φ and t_{m} ⊧ φ, it follows by Lemma 5.3 that t_{ℓ} ⊧ φ also for all 0 < ℓ < m. It follows that t_{ℓ} ∉ T^{∞}, so s ∼′ t_{ℓ}, for all ℓ ∈ ω, and hence s_{k} ∼′ s ∼′ t_{ℓ} for all k, ℓ ∈ ω. □

References

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

[2] Rocco De Nicola & Frits W. Vaandrager (1995): Three logics for branching

bisimulation. J. ACM 42(2), pp. 458–487.

[3] Rob Gerth, Ruurd Kuiper, Doron Peled & Wojciech Penczek (1999): A

partial order approach to branching time logic model checking. Information and Computation 150(2), pp. 132–152.

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

[5] Rob van Glabbeek, Bas Luttik & Nikola Trčka: Computation tree logic and

deadlock detection. In preparation.

[6] Rob van Glabbeek & Peter Weijland (1996): Branching time and abstraction in bisimulation semantics. J. ACM 43(3), pp. 555–600.

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