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.
Thus some authors define bisimulation as a symmetric simulation.
[1] Equivalently, R is a bisimulation if and only if for every pair of states
This means that the bisimilarity relation ∼ is the union of all bisimulations:
Bisimulations are also closed under reflexive, symmetric, and transitive closure; therefore, the largest bisimulation must be reflexive, symmetric, and transitive.
[2] Bisimulation can be defined in terms of composition of relations as follows.
Given a labelled state transition system
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 (
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,
The "Defender" must then attempt to match that transition,
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.
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
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
are bisimilar and there is some number of internal actions leading from
such that there is some number (possibly zero) of internal actions leading from
[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.
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.
[5] The fastest algorithms are quasilinear time using partition refinement through a reduction to the coarsest partition problem.