Bisimulation

From Wikipedia, the free encyclopedia

In theoretical computer science a bisimulation is an equivalence relation between state transition systems, associating systems which behave in the same way in the sense that one system simulates the other and vice-versa.

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.

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 closed under bisimulation (Van Benthem's theorem).

[edit] Formal definition

Given a labelled state transition system (S, Λ, →), a bisimulation relation is a binary relation R over S (i.e. R ⊆ 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,

$\begin{matrix} & \alpha & \\ p & \rightarrow & p' \\ \end{matrix}$

implies that there is a q' in S such that

$\begin{matrix} & \alpha & \\ q & \rightarrow & q' \\ \end{matrix}$

and (p',q') in R, and for all q' in S, 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.

[edit] 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 actions, often denoted with τ, i.e. actions which are not visible by external observers, then bisimulation can be relaxed to be weak bisimulation, in which the silent actions are ignored.

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.