bisimulation

Given two labelled state transition systems (LTS) $M=(S_1,\mathrm{\Sigma },{\to }_1)$, $N=(S_2,\mathrm{\Sigma },{\to }_2)$, a binary relation $\approx \subseteq S_1\times S_2$ is called a simulation if whenever $p\approx q$ and $p{\stackrel{\alpha }{\to }}_1{p}^{\prime }$, then there is a $q^{\prime }$ such that $p^{\prime }\approx q^{\prime }$ and $q{\stackrel{\alpha }{\to }}_2{q}^{\prime }$. An LSTS $M=(S_1,\mathrm{\Sigma },{\to }_1)$ is similar to an LTS $N=(S_2,\mathrm{\Sigma },{\to }_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. if $M$ is similar to $N$ and $N$ is similar to $P$, then $M$ is similar to $P$:

   Proof.

   Let $M=(S_1,\mathrm{\Sigma },{\to }_1)$, $N=(S_2,\mathrm{\Sigma },{\to }_2)$, and $P=(S_3,\mathrm{\Sigma },{\to }_3)$ be LSTS, and suppose $p{\approx }_1\circ {\approx }_{2}q$ with $p{\stackrel{\alpha }{\to }}_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{\stackrel{\alpha }{\to }}_2{r}^{\prime }$. But then since ${\approx }_2$ is a simulation, there is a $q^{\prime }$ such that $q{\stackrel{\alpha }{\to }}_3{q}^{\prime }$. As a result, ${\approx }_1\circ {\approx }_2$ is a simulation. ∎

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\stackrel{\alpha }{\to }{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\stackrel{\alpha }{\to }{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\text{ for some }a\in A\}\text{ and }C(B):=\{a\in S_1\mid a\approx b\text{ 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\mathit{\hspace{1em}}\text{iff}\mathit{\hspace{1em}}A\subseteq C(B)\text{ 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 \mathrm{\Sigma }$, let

$${\delta }_1(p,a)=\{q\in S_1\mid p{\stackrel{\alpha }{\to }}_{1}q\}.$$

We can similar define function ${\delta }_2:S_2\times \mathrm{\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 \mathrm{\Sigma }$.

Let $M=(S_1,\mathrm{\Sigma },{\to }_1)$, $N=(S_2,\mathrm{\Sigma },{\to }_2)$, and $P=(S_3,\mathrm{\Sigma },{\to }_3)$ be LTS. The following are some basic properties of bisimulation:

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

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. 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. 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\stackrel{\alpha }{\to }{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\stackrel{\alpha }{\to }{q}^{\prime }$. This means that $p^{\prime }{\approx }^{-1}{q}^{\prime }$, implying that ${\approx }^{-1}$ is a simulation. Hence $\approx$ is a bisimulation. ∎

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,\mathrm{\Sigma },\to )$, 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 $[\to ]$ on $S\times \mathrm{\Sigma }\times S$ by

$$[p]\stackrel{\alpha }{[\to ]}[q]\mathit{\hspace{1em}\hspace{1em}}\text{iff}\mathit{\hspace{1em}\hspace{1em}}p\stackrel{\alpha }{\to }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 }\stackrel{\alpha }{\to }{q}^{\prime }$. Now, $[M]:=([S],\mathrm{\Sigma },[\to ])$ 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