bisimulation

Given two labelled state transition systems (LTS) $M=(S_{1},\Sigma,\rightarrow_{1})$, $N=(S_{2},\Sigma,\rightarrow_{2})$, a binary relation $\approx\subseteq S_{1}\times S_{2}$ is called a simulation if whenever $p\approx q$ and $p\lx@stackrel{{\scriptstyle\alpha}}{{\rightarrow}}_{1}p^{\prime}$, then there is a $q^{\prime}$ such that $p^{\prime}\approx q^{\prime}$ and $q\lx@stackrel{{\scriptstyle\alpha}}{{\rightarrow}}_{2}q^{\prime}$. An LSTS $M=(S_{1},\Sigma,\rightarrow_{1})$ is similar to an LTS $N=(S_{2},\Sigma,\rightarrow_{2})$ if there is a simulation $\approx S_{1}\times S_{2}$.

For example, any LTS is similar to itself, as the identity relation on the set of states is a simulation. In addition,

1. 1.

if $M$ is similar to $N$ and $N$ is similar to $P$, then $M$ is similar to $P$:

Proof.

Let $M=(S_{1},\Sigma,\rightarrow_{1})$, $N=(S_{2},\Sigma,\rightarrow_{2})$, and $P=(S_{3},\Sigma,\rightarrow_{3})$ be LSTS, and suppose $p\approx_{1}\circ\approx_{2}q$ with $p\lx@stackrel{{\scriptstyle\alpha}}{{\rightarrow}}_{1}p^{\prime}$, where $\approx_{1}$ and $\approx_{2}$ are simulations. Then there is an $r$ such that $p\approx_{1}r$ and $r\approx_{2}q$. Since $\approx_{1}$ is a simulation, there is an $r^{\prime}$ such that $r\lx@stackrel{{\scriptstyle\alpha}}{{\rightarrow}}_{2}r^{\prime}$. But then since $\approx_{2}$ is a simulation, there is a $q^{\prime}$ such that $q\lx@stackrel{{\scriptstyle\alpha}}{{\rightarrow}}_{3}q^{\prime}$. As a result, $\approx_{1}\circ\approx_{2}$ is a simulation. ∎

2. 2.

a union of simulations is a simulation.

Proof.

Let $\approx$ be the union of simulations $\approx_{i}$, where $i\in I$, and suppose $p\approx q$, with $p\lx@stackrel{{\scriptstyle\alpha}}{{\rightarrow}}p^{\prime}$. Then $p\approx_{i}q$ for some $i$. Since $\approx_{i}$ is a simulation, there is a state $q^{\prime}$ such that $p^{\prime}\approx_{i}q^{\prime}$ and $q\lx@stackrel{{\scriptstyle\alpha}}{{\rightarrow}}q^{\prime}$. So $p^{\prime}\approx q^{\prime}$ and therefore $\approx$ is a simulation. ∎

A binary relation $\approx$ between $S_{1}$ and $S_{2}$ is a bisimulation if both $\approx$ and its converse $\approx^{-1}$ are simulations. A bisimulation is also called a strong bisimulation, in contrast with weak bisimulation. When there is a bisimulation between the state sets of two LTS, we say that the two systems are bisimilar, or strongly bisimilar. By abuse of notation, we write $M\approx N$ to denote that $M$ is bisimilar to $N$.

An equivalent formulation of bisimulation is given by extending the binary relation on the sets to a binary relation on the corresponding power sets. Here’s how: let $\approx\subseteq S_{1}\times S_{2}$. For any $A\subseteq S_{1}$ and $B\subseteq S_{2}$, define

 $C(A):=\{b\in S_{2}\mid a\approx b\mbox{ for some }a\in A\}\mbox{ and }C(B):=\{% a\in S_{1}\mid a\approx b\mbox{ for some }b\in B\}.$

Then the binary relation $\approx$ can be extended to a binary relation from $P(S_{1})$ to $P(S_{2})$, still denoted by $\approx$, as

 $A\approx B\quad\textrm{iff}\quad A\subseteq C(B)\textrm{ and }B\subseteq C(A),$

for any $A\subseteq S_{1}$ and $B\subseteq S_{2}$. In other words, $A\approx B$ iff for any $a\in A$, there is a $b\in B$ such that $a\approx b$ and for any $b\in B$, there is an $a\in A$ such that $a\approx b$. Now, for any $p\in S_{1}$ and $\alpha\in\Sigma$, let

 $\delta_{1}(p,a)=\{q\in S_{1}\mid p\lx@stackrel{{\scriptstyle\alpha}}{{% \rightarrow}}_{1}q\}.$

We can similar define function $\delta_{2}:S_{2}\times\Sigma\to P(S_{2})$. So a binary relation $\approx$ between $S_{1}$ and $S_{2}$ is a bisimilation iff for any $(p,q)\in S_{1}\times S_{2}$ such that $p\approx q$, we have $\delta_{1}(p,a)\approx\delta_{2}(q,a)$ for any $a\in\Sigma$.

Let $M=(S_{1},\Sigma,\rightarrow_{1})$, $N=(S_{2},\Sigma,\rightarrow_{2})$, and $P=(S_{3},\Sigma,\rightarrow_{3})$ be LTS. The following are some basic properties of bisimulation:

1. 1.

The identity relation $=$ is a bisimilation on any LTS, since $=$ is a simulation and $=^{-1}$ is just $=$.

2. 2.

If $M$ is bisimilar to $N$ via $\approx$, then $N$ is bisimilar to $M$ via $\approx^{-1}$, since both $\approx^{-1}$ and $(\approx^{-1})^{-1}=\approx$ are simulations.

3. 3.

If $M\approx_{1}$ and $N\approx_{2}P$, then $M\approx_{1}\circ\approx_{2}P$, since $\approx_{1}\circ\approx_{2}$ and $(\approx_{1}\circ\approx_{2})^{-1}=\approx_{2}^{1-}\circ\approx_{1}^{-1}$ are both simulations according to the argument above.

4. 4.

A union of bisimilations is a bisimilation.

Proof.

Let $\approx$ be the union of bisimulations $\approx_{i}$, where $i\in I$. Then $\approx$ is a simulation by the argument above. Now, suppose $p\approx^{-1}q$ and $p\lx@stackrel{{\scriptstyle\alpha}}{{\rightarrow}}p^{\prime}$, then $q\approx p$. Then $q\approx_{i}p$ for some $i\in I$. So $p\approx_{i}^{-1}q$. Since $\approx_{i}$ is a bisimulation, so is $\approx_{i}^{-1}$, and therefore for some state $q^{\prime}$, $p^{\prime}\approx_{i}^{-1}q^{\prime}$ and $q\lx@stackrel{{\scriptstyle\alpha}}{{\rightarrow}}q^{\prime}$. This means that $p^{\prime}\approx^{-1}q^{\prime}$, implying that $\approx^{-1}$ is a simulation. Hence $\approx$ is a bisimulation. ∎

5. 5.

The union of all bisimilations on an LTS is a bisimulation that is also an equivalence relation.

Proof.

For an LTS $M$, let $\approx_{M}$ be the union of all bisimulations on $M$. Then $\approx_{M}$ is a bisimulation by the previous result. Since $=$ is a bisimulation on $M$, $\approx_{M}$ is reflexive. If $p\approx_{M}q$, $p\approx q$ for some bisimulation $\approx$ on $M$. Then $\approx^{-1}$ is a bisimulation and therefore $q\approx^{-1}p$ implies that $q\approx_{M}p$, so that $\approx_{M}$ is symmetric. Finally, if $p\approx_{M}q$ and $q\approx_{M}r$, then $p\approx_{1}q$ and $q\approx_{2}r$ for some bisimulations $\approx_{1}$ and $\approx_{2}$. So $\approx_{1}\circ\approx_{2}$ is a bisimulation. Since $p\approx_{1}\circ\approx_{2}r$, $p\approx_{M}r$ and therefore $\approx_{M}$ is transitive. ∎

For an LTS $M=(S,\Sigma,\rightarrow)$, let $\approx_{M}$ be the maximal bisimulation on $M$ as defined above. Since $\approx_{M}$ is an equivalence relation, we can form an equivalence class $[p]$ for each state $p\in S$. Let $[S]$ be the set of all such equivalence classes: $[S]:=\{[p]\mid p\in S\}$. Define $[\rightarrow]$ on $S\times\Sigma\times S$ by

 $[p]\lx@stackrel{{\scriptstyle\alpha}}{{[\rightarrow]}}[q]\qquad\mbox{iff}% \qquad p\lx@stackrel{{\scriptstyle\alpha}}{{\rightarrow}}q.$

This is a well-defined ternary relation, for if $p\approx_{M}p^{\prime}$ and $q\approx_{M}q^{\prime}$, we have $p^{\prime}\lx@stackrel{{\scriptstyle\alpha}}{{\rightarrow}}q^{\prime}$. Now, $[M]:=([S],\Sigma,[\rightarrow])$ is an LSTS, and $M$ is bisimilar to it, with bisimulation given by the relation $\{(p,[p])\mid p\in S\}$.

 Title bisimulation Canonical name Bisimulation Date of creation 2013-03-22 19:23:14 Last modified on 2013-03-22 19:23:14 Owner CWoo (3771) Last modified by CWoo (3771) Numerical id 44 Author CWoo (3771) Entry type Definition Classification msc 03B45 Classification msc 68Q85 Classification msc 68Q10 Synonym strong bisimulation Synonym strongly bisimilar Related topic PMorphism Defines simulation Defines bisimilar