Relation between transition systems in computer science
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.
Formal definition.
Given a labeled state transition system ,
where S is a set of states, formula_1 is a set of labels and → is a set of labelled transitions (i.e., a subset of formula_2),
a bisimulation is a binary relation formula_3,
such that both R and its converse formula_4 are simulations. From this follows that the symmetric closure of a bisimulation is a bisimulation, and that each symmetric simulation is a bisimulation. Thus some authors define bisimulation as a symmetric simulation.
Equivalently, R is a bisimulation if and only if for every pair of states formula_5 in R and all labels "λ" in formula_1:
Given two states p and q in S, p is bisimilar to q, written formula_13, if and only if there is a bisimulation R such that formula_14. This means that the bisimilarity relation is the union of all bisimulations: formula_15 precisely when formula_14 for some bisimulation R.
The set of bisimulations is closed under union; therefore, the bisimilarity relation is itself a bisimulation. Since it is the union of all bisimulations, it is the unique largest bisimulation. Bisimulations are also closed under reflexive, symmetric, and transitive closure; therefore, the largest bisimulation must be reflexive, symmetric, and transitive. From this follows that the largest bisimulation—bisimilarity—is an equivalence relation.
Alternative definitions.
Relational definition.
Bisimulation can be defined in terms of composition of relations as follows.
Given a labelled state transition system formula_17, a "bisimulation" relation is a binary relation R over S (i.e., ) such that formula_18
formula_19
and
formula_20
From the monotonicity and continuity of relation composition, it follows immediately that the set of 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 (formula_21, Λ, →), define formula_22 to be a function from binary relations over formula_21 to binary relations over formula_21, as follows:
Let formula_25 be any binary relation over formula_21. formula_27 is defined to be the set of all pairs formula_5 in formula_21 × formula_21 such that:
formula_31
and
formula_32
Bisimilarity is then defined to be the greatest fixed point of formula_33.
Ehrenfeucht–Fraïssé game 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, formula_34, from formula_5. That is,
formula_36
or 
formula_37
The "Defender" must then attempt to match that transition, formula_34 from either formula_39 or formula_40 depending on the attacker's move.
I.e., they must find an formula_34 such that:
formula_42
or 
formula_43
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.
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 formula_17 can be mapped bijectively to a function formula_47 from formula_21 to the powerset of formula_21 indexed by formula_1 written as formula_51, defined by
formula_52
Let formula_53 be formula_54-th projection, mapping
formula_55 to formula_56 and formula_57 respectively for formula_58; and
formula_59 the forward image of formula_60 defined by dropping the third component
formula_61
where formula_62 is a subset of formula_63. Similarly for formula_64.
Using the above notations, a relation formula_65 is a bisimulation on a transition system formula_17 if and only if there exists a transition system formula_67 on the relation formula_25 such that the diagram
commutes, i.e. for formula_58, the equations
formula_70
hold
where formula_71 is the functional representation of formula_17.
Variants of bisimulation.
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").
A different variant applies if the state transition system includes a notion of "silent" (or "internal") action, often denoted with formula_73, i.e. actions that are not visible by external observers, then bisimulation can be relaxed to be "weak bisimulation", in which if two states formula_56 and formula_57 are bisimilar and there is some number of internal actions leading from formula_56 to some state formula_77 then there must exist state formula_78 such that there is some number (possibly zero) of internal actions leading from formula_57 to formula_78. A relation formula_81 on processes is a weak bisimulation if the following holds (with formula_82, and formula_83 being an observable and mute transition respectively):
formula_84
formula_85
This is closely related to the notion of 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 (respectively bisimilarity) 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 first-order logic invariant under bisimulation (van Benthem's theorem).
Algorithm.
Checking that two finite transition systems are bisimilar can be done in polynomial time. The fastest algorithms are quasilinear time using partition refinement through a reduction to the coarsest partition problem.
Notes.
 ;templatestyles src="Reflist/styles.css" / ;
References.
 ;templatestyles src="Reflist/styles.css" / ;