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.
Equivalently is a bisimulation if for every pair of elements in with in , for all α in Λ:
for all in ,
and, symmetrically, for all in
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 inverse 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 (, Λ, →), 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:
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.:
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:
Attacker and defender continue to take alternating turns until:
By the above definition the system is a bisimulation if and only if there exists a winning strategy for the defender.
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 τ, i.e. actions which 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 .
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).