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.

Table of contents |

2 Variants of bisimulation 3 See also |

Given a labelled state transition system (S, Λ, →), a *bisimulation* relation is a binary relation R over S (i.e. R &sube S × S) such that both R and R^{-1} are simulation preorders.

Equivalently R is a bisimulation if for every pair of elements p, q in S, if (p,q)is in R then for all α in Λ, and for all p' in S,

implies that there is a q' in S such that

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

implies that there is a p' in S such that

and (p',q') in R.

Given two states p and q in S, p is **bisimilar** to q, written p ∼ q, if there is a bisimulation R such that (p, q) is in R.

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

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 rstrictions of the programming language. Therefore, in general, there may be more than one kind of bisimulation, (bisimilarity resp.) relationship depending on the context.

- Operational semantics
- State transition systems
- Simulation preorder
- Congruence relation