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.
Contents
- Formal definition
- Relational definition
- Fixpoint definition
- Game theoretical definition
- Coalgebraic definition
- Variants of bisimulation
- Bisimulation and modal logic
- References
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.
Formal definition
Given a labelled state transition system (
Equivalently
for all
and, symmetrically, for all
Given two states
The bisimilarity relation
Note that it is not always the case that if
Relational definition
Bisimulation can be defined in terms of composition of relations as follows.
Given a labelled state transition system
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 (
Let
and
Bisimilarity is then defined to be the greatest fixed point of
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,
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.
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
Let
where
Using the above notations, a relation
commutes, i.e. for
hold where
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
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 first-order logic invariant under bisimulation (van Benthem's theorem).