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 welldefined 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  20130322 19:23:14 
Last modified on  20130322 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 