Bisimulation

Get Bisimulation essential facts below. View Videos or join the Bisimulation discussion. Add Bisimulation to your PopFlock.com topic list for future reference or share this resource on social media.
## Formal definition

## Alternative definitions

### Relational definition

### Fixpoint definition

### Game theoretical definition

### Coalgebraic definition

## Variants of bisimulation

## Bisimulation and modal logic

## Algorithm

## See also

## References

## Further reading

## External links

### Software tools

This article uses material from the Wikipedia page available here. It is released under the Creative Commons Attribution-Share-Alike License 3.0.

Bisimulation

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

Intuitively two systems are **bisimilar** if they match each other's moves. In this sense, each of the systems cannot be distinguished from the other by an observer.

Given a labelled state transition system (, , →), where is a set of states, is a set of labels and → is a set of labelled transitions (i.e., a subset of × × ), a *bisimulation* relation is a binary relation over (i.e., ⊆ × ) such that both and its converse are simulations.

Equivalently is a bisimulation if for every pair of elements in with in , for all α in :

for all in ,

- implies that there is a in such that

- and ;

and, symmetrically, for all in

- implies that there is a in such that

- and .

Given two states and in , is **bisimilar** to , written , if there is a bisimulation such that is in .

The bisimilarity relation is an equivalence relation. Furthermore, it is the largest bisimulation relation over a given transition system.

Note that it is not always the case that if simulates and simulates then they are bisimilar. For and to be bisimilar, the simulation between and must be the converse of the simulation between and . Counter-example (in CCS, describing a coffee machine) : and simulate each other but are not bisimilar.

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 over (i.e., ⊆ × ) such that

- and

From the monotonicity and continuity of relation composition, it follows immediately that the set of the 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.

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 .

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 . I.e.:

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.

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 is bijectively 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 .

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").^{[1]}

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 to bisimulation up to a relation.

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, (bisimilarity resp.) relationship depending on the context.

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).

Checking that two finite transition systems are bisimilar can be done in polynomial time.^{[2]}

**^**Baier, Christel; Katoen, Joost-Pieter (2008).*Principles of Model Checking*. MIT Press. p. 527. ISBN 978-0-262-02649-9.**^**Baier & Katoen (2008), Cor. 7.45, p. 486.

- Park, David (1981). "Concurrency and Automata on Infinite Sequences". In Deussen, Peter (ed.).
*Theoretical Computer Science*. Proceedings of the 5th GI-Conference, Karlsruhe. Lecture Notes in Computer Science.**104**. Springer-Verlag. pp. 167-183. doi:10.1007/BFb0017309. ISBN 978-3-540-10576-3. - Milner, Robin (1989).
*Communication and Concurrency*. Prentice Hall. ISBN 0-13-114984-9. - Davide Sangiorgi. (2011).
*Introduction to Bisimulation and Coinduction*. Cambridge University Press. ISBN 9781107003637

- CADP: tools to minimize and compare finite-state systems according to various bisimulations
- mCRL2: tools to minimize and compare finite-state systems according to various bisimulations
- The Bisimulation Game Game

This article uses material from the Wikipedia page available here. It is released under the Creative Commons Attribution-Share-Alike License 3.0.

Popular Products

Music Scenes

Popular Artists