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\}$.