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.

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.

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.

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
Canonical name	WeakBisimulation
Date of creation	2013-03-22 19:30:55
Last modified on	2013-03-22 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