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 },n-1$.

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

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.