Bisimulation

(Redirected from Bisimilarity)

In theoretical computer science a bisimulation is a binary relation between state transition systems, associating systems that behave in the same way in that one system simulates the other and vice versa.

Intuitively two systems are bisimilar if they, assuming we view them as playing a game according to some rules, match each other's moves. In this sense, each of the systems cannot be distinguished from the other by an observer.

Formal definition

edit

Given a labeled state transition system (S, Λ, →), where S is a set of states,   is a set of labels and → is a set of labelled transitions (i.e., a subset of  ), a bisimulation is a binary relation  , such that both R and its converse   are simulations. From this follows that the symmetric closure of a bisimulation is a bisimulation, and that each symmetric simulation is a bisimulation. Thus some authors define bisimulation as a symmetric simulation.[1]

Equivalently, R is a bisimulation if and only if for every pair of states   in R and all labels λ in  :

  • if  , then there is   such that  ;
  • if  , then there is   such that  .

Given two states p and q in S, p is bisimilar to q, written  , if and only if there is a bisimulation R such that  . This means that the bisimilarity relation is the union of all bisimulations:   precisely when   for some bisimulation R.

The set of bisimulations is closed under union;[Note 1] therefore, the bisimilarity relation is itself a bisimulation. Since it is the union of all bisimulations, it is the unique largest bisimulation. Bisimulations are also closed under reflexive, symmetric, and transitive closure; therefore, the largest bisimulation must be reflexive, symmetric, and transitive. From this follows that the largest bisimulation—bisimilarity—is an equivalence relation.[2]

Alternative definitions

edit

Relational definition

edit

Bisimulation can be defined in terms of composition of relations as follows.

Given a labelled state transition system  , a bisimulation relation is a binary relation R over S (i.e., RS × S) such that  

  and  

From the monotonicity and continuity of relation composition, it follows immediately that the set of bisimulations is closed under unions (joins in the poset of relations), and a simple algebraic calculation shows that the relation of bisimilarity—the join of all bisimulations—is an equivalence relation. This definition, and the associated treatment of bisimilarity, can be interpreted in any involutive quantale.

Fixpoint definition

edit

Bisimilarity can also be defined in order-theoretical fashion, in terms of fixpoint theory, more precisely as the greatest fixed point of a certain function defined below.

Given a labelled state transition system ( , Λ, →), define   to be a function from binary relations over   to binary relations over  , as follows:

Let   be any binary relation over  .   is defined to be the set of all pairs   in   ×   such that:

  and  

Bisimilarity is then defined to be the greatest fixed point of  .

Ehrenfeucht–Fraïssé game definition

edit

Bisimulation can also be thought of in terms of a game between two players: attacker and defender.

"Attacker" goes first and may choose any valid transition,  , from  . That is,   or  

The "Defender" must then attempt to match that transition,   from either   or   depending on the attacker's move. I.e., they must find an   such that:   or  

Attacker and defender continue to take alternating turns until:

  • The defender is unable to find any valid transitions to match the attacker's move. In this case the attacker wins.
  • The game reaches states   that are both 'dead' (i.e., there are no transitions from either state) In this case the defender wins
  • The game goes on forever, in which case the defender wins.
  • The game reaches states  , which have already been visited. This is equivalent to an infinite play and counts as a win for the defender.

By the above definition the system is a bisimulation if and only if there exists a winning strategy for the defender.

Coalgebraic definition

edit

A bisimulation for state transition systems is a special case of coalgebraic bisimulation for the type of covariant powerset functor. Note that every state transition system   can be mapped bijectively to a function   from   to the powerset of   indexed by   written as  , defined by  

Let   be  -th projection, mapping   to   and   respectively for  ; and   the forward image of   defined by dropping the third component   where   is a subset of  . Similarly for  .

Using the above notations, a relation   is a bisimulation on a transition system   if and only if there exists a transition system   on the relation   such that the diagram

 

commutes, i.e. for  , the equations   hold where   is the functional representation of  .

Variants of bisimulation

edit

In special contexts the notion of bisimulation is sometimes refined by adding additional requirements or constraints. An example is that of stutter bisimulation, in which one transition of one system may be matched with multiple transitions of the other, provided that the intermediate states are equivalent to the starting state ("stutters").[3]

A different variant applies if the state transition system includes a notion of silent (or internal) action, often denoted with  , i.e. actions that are not visible by external observers, then bisimulation can be relaxed to be weak bisimulation, in which if two states   and   are bisimilar and there is some number of internal actions leading from   to some state   then there must exist state   such that there is some number (possibly zero) of internal actions leading from   to  . A relation   on processes is a weak bisimulation if the following holds (with  , and   being an observable and mute transition respectively):

   

This is closely related[how?] to the notion of bisimulation "up to" a relation.[4]

Typically, if the state transition system gives the operational semantics of a programming language, then the precise definition of bisimulation will be specific to the restrictions of the programming language. Therefore, in general, there may be more than one kind of bisimulation (respectively bisimilarity) relationship depending on the context.

Bisimulation and modal logic

edit

Since Kripke models are a special case of (labelled) state transition systems, bisimulation is also a topic in modal logic. In fact, modal logic is the fragment of first-order logic invariant under bisimulation (van Benthem's theorem).

Algorithm

edit

Checking that two finite transition systems are bisimilar can be done in polynomial time.[5] The fastest algorithms are quasilinear time using partition refinement through a reduction to the coarsest partition problem.

See also

edit

Notes

edit
  1. ^ Meaning the union of two bisimulations is a bisimulation.

References

edit
  1. ^ Jančar, Petr and Srba, Jiří (2008). "Undecidability of Bisimilarity by Defender's Forcing". J. ACM. 55 (1). New York, NY, USA: Association for Computing Machinery: 26. doi:10.1145/1326554.1326559. ISSN 0004-5411. S2CID 14878621.{{cite journal}}: CS1 maint: multiple names: authors list (link)
  2. ^ Milner, Robin (1989). Communication and Concurrency. USA: Prentice-Hall, Inc. ISBN 0131149849.
  3. ^ Baier, Christel; Katoen, Joost-Pieter (2008). Principles of Model Checking. MIT Press. p. 527. ISBN 978-0-262-02649-9.
  4. ^ Damien Pous (2005). "Up-to techniques for weak bisimulation". Proc. 32nd ICALP. Lecture Notes in Computer Science. 3580. Springer Verlag: 730–741.
  5. ^ Baier & Katoen (2008), Corollary 7.45, p. 486.

Further reading

edit
edit

Software tools

edit