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

1.
Let $\Rightarrow $ be the reflexive^{} and transitive closures^{} of $\stackrel{\tau}{\to}$. In other words, $p\Rightarrow q$ iff either $p=q$, or there is a positive integer $n>1$ and states ${r}_{1},\mathrm{\dots},{r}_{n}$ such that $p={r}_{1}$ and $q={r}_{n}$ and ${r}_{i}\stackrel{\tau}{\to}{r}_{i+1}$, where $i=1,\mathrm{\dots},n1$.

2.
Next, for any label $\alpha $ that is not the silent step $\tau $ in $\mathrm{\Sigma}$, define
$$\stackrel{\alpha}{\Rightarrow}:=\stackrel{\alpha}{\to}\circ \Rightarrow \circ \stackrel{\alpha}{\to},$$ where $\circ $ denotes the relational composition^{} operation^{}. In other words, $p\stackrel{\alpha}{\Rightarrow}q$ iff there are states $r$ and $s$ such that $p\stackrel{\alpha}{\to}r$, $r\Rightarrow s$, and $s\stackrel{\alpha}{\to}q$.

3.
Finally, for any label $\alpha \in \mathrm{\Sigma}$, let
$$\stackrel{(\alpha )}{\Rightarrow}:=\{\begin{array}{cc}\Rightarrow \hfill & \text{if}\alpha =\tau \hfill \\ \stackrel{\alpha}{\Rightarrow}\hfill & \text{otherwise.}\hfill \end{array}$$
Definition. Let $M=({S}_{1},\mathrm{\Sigma},{\to}_{1})$ and $N=({S}_{2},\mathrm{\Sigma},{\to}_{2})$ be two labelled state transition systems, with $\tau \in \mathrm{\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{\stackrel{\alpha}{\to}}_{1}{p}^{\prime}$, there is a state ${q}^{\prime}\in {S}_{2}$ such that ${p}^{\prime}\approx {q}^{\prime}$ and ${p}^{\prime}{\stackrel{(\alpha )}{\Rightarrow}}_{2}q$. $\approx $ is a weak bisimulation if both $\approx $ and its converse^{} ${\approx}^{1}$ are weak simulations.
Title  weak bisimulation 

Canonical name  WeakBisimulation 
Date of creation  20130322 19:30:55 
Last modified on  20130322 19:30:55 
Owner  CWoo (3771) 
Last modified by  CWoo (3771) 
Numerical id  10 
Author  CWoo (3771) 
Entry type  Definition 
Classification  msc 68Q85 
Synonym  invisible step 
Defines  silent step 
Defines  weak simulation 