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

Formal definition 1

Alternative definitions 2

Relational definition 2.1

Fixpoint definition 2.2

Game theoretical definition 2.3

Coalgebraic definition 2.4

Variants of bisimulation 3

Bisimulation and modal logic 4

See also 5

Software tools 6

References 7

Further reading 8
Formal definition
Given a labelled state transition system (S, Λ, →), a bisimulation relation is a binary relation R over S (i.e., R ⊆ S × S) such that both R^{−1} and R are simulations.
Equivalently R is a bisimulation if for every pair of elements p, q in S with (p,q) in R, for all α in Λ:
for all p' in S,


p \overset{\alpha}{\rightarrow} p'

implies that there is a q' in S such that


q \overset{\alpha}{\rightarrow} q'

and (p',q') \in R;
and, symmetrically, for all q' in S


q \overset{\alpha}{\rightarrow} q'

implies that there is a p' in S such that


p \overset{\alpha}{\rightarrow} p'

and (p',q') \in R.
Given two states p and q in S, p is bisimilar to q, written p \, \sim \, q, if there is a bisimulation R such that (p, q) is in R.
The bisimilarity relation \, \sim \, 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 p simulates q and q simulates p then they are bisimilar. For p and q to be bisimilar, the simulation between p and q must be the inverse of the simulation between q and p. Counterexample (in CCS, describing a coffee machine) : M=p.\overline{c}.M+p.\overline{t}.M+p.(\overline{c}.M+\overline{t}.M) and M'=p.(\overline{c}.M'+\overline{t}.M') simulate each other but are not bisimilar.
Alternative definitions
Relational definition
Bisimulation can be defined in terms of composition of relations as follows.
Given a labelled state transition system (S, \Lambda, \rightarrow), a bisimulation relation is a binary relation R over S (i.e., R ⊆ S × S) such that \forall\alpha\in\Lambda


R\ ;\ \overset{\alpha}{\rightarrow}\quad {\subseteq}\quad \overset{\alpha}{\rightarrow}\ ;\ R

and

R^{1}\ ;\ \overset{\alpha}{\rightarrow}\quad {\subseteq}\quad \overset{\alpha}{\rightarrow}\ ;\ R^{1}
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.
Fixpoint definition
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 (S, Λ, →), define F:\mathcal{P}(S \times S) \to \mathcal{P}(S \times S) to be a function from binary relations over S to binary relations over S, as follows:
Let R be any binary relation over S. F(R) is defined to be the set of all pairs (p,q) in S × S such that:

\forall \alpha \in \Lambda. \, \forall p' \in S. \, p \overset{\alpha}{\rightarrow} p' \, \Rightarrow \, \exists q' \in S. \, q \overset{\alpha}{\rightarrow} q' \,\textrm{ and }\, (p',q') \in R
and

\forall \alpha \in \Lambda. \, \forall q' \in S. \, q \overset{\alpha}{\rightarrow} q' \, \Rightarrow \, \exists p' \in S. \, p \overset{\alpha}{\rightarrow} p' \,\textrm{ and }\, (p',q') \in R
Bisimilarity is then defined to be the greatest fixed point of F.
Game theoretical definition
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, \alpha, from (p,q). I.e.:
(p,q) \overset{\alpha}{\rightarrow} (p',q) or (p,q) \overset{\alpha}{\rightarrow} (p,q')
The "Defender" must then attempt to match that transition, \alpha from either (p',q) or (p,q') depending on the attacker's move. I.e., they must find an \alpha such that:
(p',q) \overset{\alpha}{\rightarrow} (p',q') or (p,q') \overset{\alpha}{\rightarrow} (p',q')
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 (p,q) 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 (p,q), 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
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 (S, \Lambda, \rightarrow) is bijectively a function \xi_{\rightarrow} from S to the powerset of S indexed by \Lambda written as \mathcal{P}(\Lambda \times S), defined by


p \mapsto \{ (\alpha, q) \in S : p \overset{\alpha}{\rightarrow} q \}.
Let \pi_i \colon S \times S \to S be ith projection mapping (p, q) to p and q respectively for i = 1, 2; and \mathcal{P}(\Lambda \times \pi_1) the forward image of \pi_1 defined by dropping the third component


P \mapsto \{ (\alpha, p) \in \Lambda \times S : \exists q . (\alpha, p, q) \in P \}
where P is a subset of \Lambda \times S \times S. Similarly for \mathcal{P}(\Lambda \times \pi_2).
Using the above notations, a relation R \subseteq S \times S is a bisimulation on a transition system (S, \Lambda, \rightarrow) if and only if there exists a transition system \gamma \colon R \to \mathcal{P}(\Lambda \times R) on the relation R such that the diagram
commutes, i.e. for i = 1, 2, the equations


\xi_\rightarrow \circ \pi_i = \mathcal{P}(\Lambda \times \pi_i) \circ \gamma
hold where \xi_{\rightarrow} is the functional representation of (S, \Lambda, \rightarrow).
Variants of bisimulation
In special contexts the notion of bisimulation is sometimes refined by adding additional requirements or constraints. For example if the state transition system includes a notion of silent (or internal) action, often denoted with \tau, i.e. actions that are not visible by external observers, then bisimulation can be relaxed to be weak bisimulation, in which if two states p and q are bisimilar and there is some number of internal actions leading from p to some state p' then there must exist state q' such that there is some number (possibly zero) of internal actions leading from q to q'. A relation \mathcal{R} on processes is a weak bisimulation if the following holds (with \mathcal{S} \in \{ \mathcal{R}, \mathcal{R}^{1} \}, and a,\tau being an observable and mute transition respectively):
\forall p, q. \quad (p,q) \in \mathcal{S} \Rightarrow p \stackrel{\tau}{\rightarrow} p' \Rightarrow \exists q' . \quad q \stackrel{\tau^\ast}{\rightarrow} q' \wedge (p',q') \in \mathcal{S}
\forall p, q. \quad (p,q) \in \mathcal{S} \Rightarrow p \stackrel{a}{\rightarrow} p' \Rightarrow \exists q' . \quad q \stackrel{\tau^\ast a \tau^\ast}{\rightarrow} q' \wedge (p',q') \in \mathcal{S}
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.
Bisimulation and modal logic
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 firstorder logic invariant under bisimulation (Van Benthem's theorem).
See also
Software tools

CADP: tools to minimize and compare finitestate systems according to various bisimulations

mCRL2 tools to minimize and compare finitestate systems according to various bisimulations]

The Bisimulation Game Game
References

Park, David (1981). "Concurrency and Automata on Infinite Sequences". In Deussen, Peter. Theoretical Computer Science. Proceedings of the 5th GIConference, Karlsruhe.

Milner, Robin (1989). Communication and Concurrency.
Further reading

Davide Sangiorgi. (2011). Introduction to Bisimulation and Coinduction. Cambridge University Press. ISBN 9781107003637
This article was sourced from Creative Commons AttributionShareAlike License; additional terms may apply. World Heritage Encyclopedia content is assembled from numerous content providers, Open Access Publishing, and in compliance with The Fair Access to Science and Technology Research Act (FASTR), Wikimedia Foundation, Inc., Public Library of Science, The Encyclopedia of Life, Open Book Publishers (OBP), PubMed, U.S. National Library of Medicine, National Center for Biotechnology Information, U.S. National Library of Medicine, National Institutes of Health (NIH), U.S. Department of Health & Human Services, and USA.gov, which sources content from all federal, state, local, tribal, and territorial government publication portals (.gov, .mil, .edu). Funding for USA.gov and content contributors is made possible from the U.S. Congress, EGovernment Act of 2002.
Crowd sourced content that is contributed to World Heritage Encyclopedia is peer reviewed and edited by our editorial staff to ensure quality scholarly research articles.
By using this site, you agree to the Terms of Use and Privacy Policy. World Heritage Encyclopedia™ is a registered trademark of the World Public Library Association, a nonprofit organization.