Bisimulation

R.J. van Glabbeek

NICTA, Sydney, Australia. School of Computer Science and Engineering, The University of New South Wales, Sydney, Australia. Computer Science Department, Stanford University, CA 94305-9045, USA

                     http://theory.stanford.edu/~rvg        rvg@cs.stanford.edu

Bisimulation equivalence is a semantic equivalence relation on labelled transition systems, which are used to represent distributed systems. It identifies systems with the same branching structure.

Labelled transition systems

A labelled transition system consists of a collection of states and a collection of transitions between them. The transitions are labelled by actions from a given set A that happen when the transition is taken, and the states may be labelled by predicates from a given set P that hold in that state.

Definition 1 Let A and P be sets (of actions and predicates, respectively). A labelled transition system (LTS) over A and P is a triple (S, →, ⊧) with

• S a class (of states),

• → a collection of binary relations ⟶^{a} ⊆ S × S—one for every a ∈ A—(the transitions), such that for all s ∈ S the class {t ∈ S | s ⟶^{a} t} is a set,

• and ⊧ ⊆ S × P. s ⊧ p says that predicate p ∈ P holds in state s ∈ S.

LTSs with A a singleton (i.e. with → a single binary relation on S) are known as Kripke structures, the models of modal logic. General LTSs (with A arbitrary) are the Kripke models for polymodal logic. The name “labelled transition system” is employed in concurrency theory. There, the elements of S represent the systems one is interested in, and s ⟶^{a} t means that system s can evolve into system t while performing the action a. This approach identifies states and systems: the states of a system s are the systems reachable from s by following the transitions. In this realm P is often taken to be empty, or it contains a single predicate √ indicating successful termination.

Definition 2 A process graph over A and P is a tuple g = (S, I, →, ⊧) with (S, →, ⊧) an LTS over A and P in which S is a set, and I ∈ S.

Process graphs are used in concurrency theory to disambiguate between states and systems. A process graph (S, I, →, ⊧) represents a single system, with S the set of its states and I its initial state. In the context of an LTS (S, →, ⊧) two concurrent systems are modelled by two members of S; in the context of process graphs, they are two different graphs. The nondeterministic finite automata used in automata theory are process graphs with a finite set of states over a finite alphabet A and a set P consisting of a single predicate denoting acceptance.

Written August 2000 for the forgotten Encyclopedia of Distributed Computing (J.E. Urban & P. Dasgupta, eds.).

“Further reading” added November 2010. To appear in the Encyclopedia of Parallel Computing (D. Padua, ed.), Springer, 2011.

Bisimulation equivalence

Bisimulation equivalence is defined on the states of a given LTS, or between different process graphs.

Definition 3 Let (S, →, ⊧) be an LTS over A and P. A bisimulation is a binary relation R ⊆ S×S, satisfying:

∧ if sRt then s ⊧ p ⇔ t ⊧ p for all p ∈ P,

∧ if sRt and s ⟶^{a} s′ with a ∈ A, then there exists a t′ with t ⟶^{a} t′ and s′Rt′,

∧ if sRt and t ⟶^{a} t′ with a ∈ A, then there exists an s′ with s ⟶^{a} s′ and s′Rt′.

Two states s, t ∈ S are bisimilar, denoted s\underline{↔} t, if there exists a bisimulation R with sRt.

Bisimilarity turns out to be an equivalence relation on S, and is also called bisimulation equivalence.

Definition 4 Let g = (S, I, →, ⊧) and h = (S′, I′, →′, ⊧′) be process graphs over A and P. A bisimulation between g and h is a binary relation R ⊆ S × S′, satisfying IRI′ and the same three clauses as above. g and h are bisimilar, denoted g \underline{↔} h, if there exists a bisimulation between them.

b a  a c  \underline{↮}  b a c

Example The two process graphs above (over A = {a, b, c} and P = {√}), in which the initial states are indicated by short incoming arrows and the final states (the ones labelled with √) by double circles, are not bisimulation equivalent, even though in automata theory they accept the same language. The choice between b and c is made at a different moment (namely before vs. after the a-action); i.e. the two systems have a different branching structure. Bisimulation semantics distinguishes systems that differ in this manner.

Modal logic

(Poly)modal logic is an extension of propositional logic with formulas ^{/} \a^{\} /φ, saying that it is possible to follow an a-transition after which the formula φ holds. Modal formulas are interpreted on the states of labelled transition systems. Two systems are bisimilar iff they satisfy the same infinitary modal formulas.

Definition 5 The language L of polymodal logic over A and P is given by:

• ⊤ ∈ L,

• p ∈ L for all p ∈ P,

• if φ, ψ ∈ L for then φ ∧ ψ ∈ L,

• if φ ∈ L then ¬φ ∈ L,

• if φ ∈ L and a ∈ A then ^{/} \a^{\} /φ ∈ L.

Basic (as opposed to poly-) modal logic is the special case where |A| = 1; there ^{/} \a^{\} /φ is simply denoted ⋄φ. The Hennessy-Milner logic is polymodal logic with P = ∅. The language L^{∞} of infinitary polymodal logic over A and P is obtained from L by additionally allowing ⋀_{i∈I} φ_{i} to be in L^{∞} for arbitrary index sets I and φ_{i} ∈ L^{∞} for i ∈ I. The connectives ⊤ and ∧ are then the special cases I = ∅ and |I| = 2.

Definition 6 Let (S, →, ⊧) be an LTS over A and P. The relation ⊧ ⊆ S × P can be extended to the satisfaction relation ⊧ ⊆ S × L^{∞}, by defining

• s ⊧ ⋀_{i∈I} φ_{i} if s ⊧ φ_{i} for all i ∈ I—in particular, s ⊧ ⊤ for any state s ∈ S,

• s ⊧ ¬φ if s |̸= φ,

• s ⊧ ^{/} \a^{\} /φ if there is a state t with s ⟶^{a} t and t ⊧ φ.

Write L(s) for {φ ∈ L | s ⊧ φ}.

Theorem 1 [5] Let (S, →, ⊧) be an LTS and s, t ∈ S. Then s\underline{↔} t ⇔ L^{∞}(s) = L^{∞}(t).

In case the systems s and t are image finite, it suffices to consider finitary polymodal formulas only [3]. In fact, for this purpose it is enough to require that one of s and t is image finite.

Definition 7 Let (S, →, ⊧) be an LTS. A state t ∈ S is reachable from s ∈ S if there are s_{i} ∈ S

and a_{i} ∈ A for i = 0, ..., n with s = s_{0}, s_{i−1} ⟶^{a_{i}} s_{i} for i = 1, ..., n, and s_{n} = t. A state s ∈ S is

image finite if for every state t ∈ S reachable from s and for every a ∈ A, the set {u ∈ S | t ⟶^{a} u} is finite.

Theorem 2 [4] Let (S, →, ⊧) be an LTS and s, t∈S with s image finite. Then s\underline{↔} t ⇔ L(s) = L(t).

Non-well-founded sets

Another characterization of bisimulation semantics can be given by means of Aczel’s universe V of non-well-founded sets [1]. This universe is an extension of the Von Neumann universe of wellfounded sets, where the axiom of foundation (every chain x_{0} ∋ x_{1} ∋ ⋯ terminates) is replaced by an anti-foundation axiom.

Definition 8 Let (S, →, ⊧) be an LTS, and let B denote the unique function M : S → V satisfying, for all s ∈ S,

M(s) = {^{/} \a, M(t)^{\} / | s ⟶^{a} t}.

It follows from Aczel’s anti-foundation axiom that such a function exists. In fact, the axiom amounts to saying that systems of equations like the one above have unique solutions. B(s) could be taken to be the branching structure of s. The following theorem then says that two systems are bisimilar iff they have the same branching structure.

Theorem 3 [2] Let (S, →, ⊧) be an LTS and s, t ∈ S. Then s\underline{↔} t ⇔ B(s) = B(t).

Abstraction

In concurrency theory it is often useful to distinguish between internal actions, that do not admit interactions with the outside world, and external ones. As normally there is no need to distinguish the internal actions from each other, they all have the same name, namely τ. If A is the set of external actions a certain class of systems may perform, then A_{τ} := A ._{∪} {τ}. Systems in that class are then represented by labelled transition systems over A_{τ} and a set of predicates P. The variant of bisimulation equivalence that treats τ just like any action of A is called strong bisimulation equivalence. Often, however, one wants to abstract from internal actions to various degrees. A system doing two τ actions in succession is then considered equivalent to a system doing just one. However, a system that can do either a or b is considered different from a system that can do either a or first τ and then b, because if the former system is placed in an environment where b cannot happen, it can still do a instead, whereas the latter system may reach a state (by executing the τ action) in which a is no longer possible.

Several versions of bisimulation equivalence that formalize these desiderata occur in the literature. Branching bisimulation equivalence [2], like strong bisimulation, faithfully preserves the branching structure of related systems. The notions of weak and delay bisimulation equivalence, which were both introduced by Milner under the name observational equivalence, make more identifications, motivated by observable machine-behavior according to certain testing scenarios.

Write s ⟹ t for ∃n ≥ 0 : ∃s_{0}, ..., s_{n}: s = s_{0} ⟶^{τ} s_{1} ⟶^{τ} ⋯ ⟶^{τ} s_{n} = t, i.e. a (possibly empty) path of τ-steps from s to t. Furthermore, for a ∈ A_{τ}, write s ⟶^{(a)} t for s ⟶^{a} t ∨ (a = τ ∧ s = t). Thus ⟶^{(a)} is the same as ⟶^{a} for a ∈ A, and ⟶^{(τ)} denotes zero or one τ-steps.

Definition 9 Let (S, →, ⊧) be an LTS over A_{τ} and P. Two states s, t ∈ S are branching bisimulation equivalent, denoted s \underline{↔}_{b} t, if they are related by a binary relation R ⊆ S × S (a branching bisimulation), satisfying:

∧ if sRt and s ⊧ p with p ∈ P, then there is a t_{1} with t ⟹ t_{1} ⊧ p and sRt_{1},

∧ if sRt and t ⊧ p with p ∈ P, then there is a s_{1} with s ⟹ s_{1} ⊧ p and s_{1}Rt,

∧ if sRt and s ⟶^{a} s′ with a∈A_{τ}, then there are t_{1}, t_{2}, t′ with t ⟹ t_{1} ⟶^{(a)} t_{2} = t′, sRt_{1} and s′Rt′,

∧ if sRt and t ⟶^{a} t′ with a∈A_{τ}, then there are s_{1}, s_{2}, s′ with s⟹s_{1} ⟶^{(a)}s_{2} = s′, s_{1}Rt and s′Rt′.

Delay bisimulation equivalence, \underline{↔}_{d}, is obtained by dropping the requirements sRt_{1} and s_{1}Rt. Weak bisimulation equivalence [5], \underline{↔}_{w}, is obtained by furthermore relaxing the requirements t_{2} = t′ and s_{2} = s′ to t_{2} ⟹ t′ and s_{2} ⟹ s′.

These definition stem from concurrency theory. On Kripke structures, when studying modal or temporal logics, normally a stronger version of the first two conditions is imposed:

∧ if sRt and p ∈ P, then s ⊧ p ⇔ t ⊧ p.

For systems without τ’s all these notions coincide with strong bisimulation equivalence.

Concurrency

When applied to parallel systems, capable of performing different actions at the same time, the versions of bisimulation discussed here employ interleaving semantics: no distinction is made between true parallelism and its nondeterministic sequential simulation. Versions of bisimulation that do make such a distinction have been developed as well, most notably the ST-bisimulation [2], that takes temporal overlap of actions into account, and the history preserving bisimulation [2] that even keeps track of causal relations between actions. For this purpose, system representations such as Petri nets or event structures are often used instead of labelled transition systems.

References

[1] P. Aczel (1988): Non-well-founded Sets, CSLI Lecture Notes 14. Stanford University.

[2] R.J. van Glabbeek (1990): Comparative Concurrency Semantics and Refinement of Actions. PhD thesis, Free University, Amsterdam. Second edition available as CWI tract 109, CWI, Amsterdam 1996.

[3] M. Hennessy & R. Milner (1985): Algebraic laws for nondeterminism and concurrency. Journal of the ACM 32(1), pp. 137–161.

[4] M.J. Hollenberg (1995): Hennessy-Milner classes and process algebra. In A. Ponse, M. de Rijke & Y. Venema, editors: Modal Logic and Process Algebra: a Bisimulation Perspective, CSLI Lecture Notes 53, CSLI Publications, Stanford, California, pp. 187–216.

[5] R. Milner (1990): Operational and algebraic semantics of concurrent processes. In J. van Leeuwen, editor: Handbook of Theoretical Computer Science, chapter 19, Elsevier Science Publishers B.V. (North-Holland), pp. 1201–1242.

Further reading

Gentle introductions to bisimulation semantics, with many examples of applications, can be found in the textbooks:

− J.C.M. Baeten & W.P. Weijland (1990): Process Algebra, Cambridge University Press.

− R. Milner (1989): Communication and Concurrency, Prentice Hall.

An historical perspective on bisimulation appears in

− D. Sangiorgi (2009): On the origins of bisimulation and coinduction, ACM Transactions on Programming Languages and Systems 31(4).