# weak bisimulation

Let $M=(S,\Sigma,\rightarrow)$ be a labelled state transition system (LTS). Recall that for each label $\alpha\in\Sigma$, there is an associated binary relation $\lx@stackrel{{\scriptstyle\alpha}}{{\rightarrow}}$ on $S$. Single out a label $\tau\in\Sigma$, and call it the silent step. Define the following relations:

1. 1.

Let $\Rightarrow$ be the reflexive and transitive closures of $\lx@stackrel{{\scriptstyle\tau}}{{\rightarrow}}$. In other words, $p\Rightarrow q$ iff either $p=q$, or there is a positive integer $n>1$ and states $r_{1},\ldots,r_{n}$ such that $p=r_{1}$ and $q=r_{n}$ and $r_{i}\lx@stackrel{{\scriptstyle\tau}}{{\rightarrow}}r_{i+1}$, where $i=1,\ldots,n-1$.

2. 2.

Next, for any label $\alpha$ that is not the silent step $\tau$ in $\Sigma$, define

 $\lx@stackrel{{\scriptstyle\alpha}}{{\Rightarrow}}\;\;\;:=\;\;\;\lx@stackrel{{% \scriptstyle\alpha}}{{\rightarrow}}\circ\Rightarrow\circ\lx@stackrel{{% \scriptstyle\alpha}}{{\rightarrow}},$

where $\circ$ denotes the relational composition operation. In other words, $p\lx@stackrel{{\scriptstyle\alpha}}{{\Rightarrow}}q$ iff there are states $r$ and $s$ such that $p\lx@stackrel{{\scriptstyle\alpha}}{{\rightarrow}}r$, $r\Rightarrow s$, and $s\lx@stackrel{{\scriptstyle\alpha}}{{\rightarrow}}q$.

3. 3.

Finally, for any label $\alpha\in\Sigma$, let

 $\lx@stackrel{{\scriptstyle(\alpha)}}{{\Rightarrow}}\;\;\;:=\;\;\;\left\{\begin% {array}[]{ll}\Rightarrow&\mbox{if }\alpha=\tau\\ \lx@stackrel{{\scriptstyle\alpha}}{{\Rightarrow}}&\textrm{otherwise.}\end{% array}\right.$

Definition. Let $M=(S_{1},\Sigma,\rightarrow_{1})$ and $N=(S_{2},\Sigma,\rightarrow_{2})$ be two labelled state transition systems, with $\tau\in\Sigma$ the silent step. A relation $\approx\subseteq S_{1}\times S_{2}$ is called a weak simulation if whenever $p\approx q$ and any labelled transition $p\lx@stackrel{{\scriptstyle\alpha}}{{\rightarrow}}_{1}p^{\prime}$, there is a state $q^{\prime}\in S_{2}$ such that $p^{\prime}\approx q^{\prime}$ and $p^{\prime}\lx@stackrel{{\scriptstyle(\alpha)}}{{\Rightarrow}}_{2}q$. $\approx$ is a weak bisimulation if both $\approx$ and its converse $\approx^{-1}$ are weak simulations.

Title weak bisimulation WeakBisimulation 2013-03-22 19:30:55 2013-03-22 19:30:55 CWoo (3771) CWoo (3771) 10 CWoo (3771) Definition msc 68Q85 invisible step silent step weak simulation