## You are here

Homebisimulation

## Primary tabs

# 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\stackrel{\alpha}{\rightarrow}_{1}p^{{\prime}}$, then there is a $q^{{\prime}}$ such that $p^{{\prime}}\approx q^{{\prime}}$ and $q\stackrel{\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. 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\stackrel{\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\stackrel{\alpha}{\rightarrow}_{2}r^{{\prime}}$. But then since $\approx_{2}$ is a simulation, there is a $q^{{\prime}}$ such that $q\stackrel{\alpha}{\rightarrow}_{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}{\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\stackrel{\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\stackrel{\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. 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}{\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\stackrel{\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. 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]\stackrel{\alpha}{[\rightarrow]}[q]\qquad\mbox{iff}\qquad p\stackrel{\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}}\stackrel{\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\}$.

## Mathematics Subject Classification

03B45*no label found*68Q85

*no label found*68Q10

*no label found*

- Forums
- Planetary Bugs
- HS/Secondary
- University/Tertiary
- Graduate/Advanced
- Industry/Practice
- Research Topics
- LaTeX help
- Math Comptetitions
- Math History
- Math Humor
- PlanetMath Comments
- PlanetMath System Updates and News
- PlanetMath help
- PlanetMath.ORG
- Strategic Communications Development
- The Math Pub
- Testing messages (ignore)

- Other useful stuff
- Corrections