When are two simulations not a bisimulation?

Problem Detail: 

Given a labelled transition system $(S,\Lambda,\to)$, where $S$ is a set of states, $\Lambda$ is a set of labels, and $\to\subseteq S\times\Lambda\times S$ is a ternary relation. As usual, write $p \stackrel\alpha\rightarrow q$ for $(p,\alpha,q)\in\to$. The labelled transition $p\stackrel\alpha\to q$ denotes that the system in state $p$ changes state to $q$ with label $\alpha$, meaning that $\alpha$ is some observable action that causes the state change.

Now a relation $R \subseteq S \times S$ is a called a simulation iff $$ \forall (p,q)\in R, \text{ if } p \stackrel\alpha\rightarrow p' \text{ then } \exists q', \; q \stackrel\alpha\rightarrow q' \text{ and } (p',q')\in R. $$

One LTS is said to simulate another if there exists a simulation relation between them.

Similarly, a relation $R \subseteq S \times S$ is a bisimulation iff $\forall (p,q)\in R,$ $$ \begin{array}{l} \text{ if } p \stackrel\alpha\rightarrow p' \text{ then } \exists q', \; q \stackrel\alpha\rightarrow q' \text{ and } (p',q')\in R \text{ and } \\ \text{ if } q \stackrel\alpha\rightarrow q' \text{ then } \exists p', \; p \stackrel\alpha\rightarrow p' \text{ and } (p',q')\in R. \end{array} $$

Two LTSs are said to be bisimilar iff there exists a bisimulation between their state spaces.

Clearly these two notions are quite related, but they are not the same.

Under what conditions is it the case that an LTS simulates another and vice versa, but that the two LTSs are not bisimilar?

Asked By : Dave Clarke

Answered By : jmad

Because a CCS process is worth a thousand pixels – and it is easy to see the underlying LTS – here are two processes that simulates each other but are not bisimilar:

$$P = ab + a$$ $$Q = ab$$

$\mathcal{R_1}=\{(ab+a, ab), (b, b), (0,b), (0, 0)\}$ is a simulation.

$\mathcal{R_2}=\{(ab, ab+a), (b, b), (0,0)\}$ is a simulation.

$P\ \mathcal R_1\ Q$ and $Q\ \mathcal R_2\ P$ but $P$ and $Q$ are not bisimilar. Why not? Because $P\stackrel{a}→0$ and the only $Q'$ such that $Q\stackrel{a}→Q'$ is $b$ ... and $0$ is not bisimilar to $b$.

Why can they simulate each other, then? Because $P$ simulates $Q$ since it can do everything $Q$ does. And $Q$ simulates $P$ because even if $P$ can go in one $a$-step to a program that does nothing, $Q$ can still do that $a$-step, and that's all it takes to simulate something. The key difference with the bisimulation is really that, as Charles said, you have to relate the same processes with both simulations. (i.e. $\mathcal R$ such that both $\mathcal R$ and $\mathcal R^{-1}$ are simulations)

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/541