# Weak bisimulation up-to $\approx$

Given this definition of weak bisimilarity:

A configuration relation $\mathcal{R}$ is a weak bisimulation provided that whenever $P\ \mathcal{R}\ Q$ and $\alpha$ is $\mu$ or $\tau$ action then:

1. $P \to^\alpha P'$ then $Q \Rightarrow^\widehat{\alpha} Q'$ for some $Q'$ s.t. $P'\ \mathcal{R}\ Q'$

2. $Q \to^\alpha Q'$ then $P \Rightarrow^\widehat{\alpha} P'$ for some $P'$ s.t. $P'\ \mathcal{R}\ Q'$

P and Q are weakly bisimilar, written $P \ \approx \ Q$, if $P \ \mathcal{R} \ Q$ for some configuration relation $\mathcal{R}$.

My questions are:

1. For the relation $\mathcal{R} = \{(\tau.a, 0)\}$, $\mathcal{R} \nsubseteq \approx$ but $\mathcal{R} \subseteq \, \approx \! \mathcal{R} \approx$. Why is $\mathcal{R} \subseteq \, \approx \! \mathcal{R} \approx$?
2. According to Sangiorgi's book, P uses $\tau$ and ends up with $a \approx \tau.a$ and Q has $0$ and ignores the move. I am wondering, how is it that you can ignore the move? I thought that one is forced to do a move...

3. Could you please provide an detailed explanation of why weak bisimilarity up-to $\approx$ is unsound? (You can use the example above but I would appreciate a detailed explanation

Thanks.

1. For the relation $\mathcal{R} = \{(\tau.a, 0)\}$, $\mathcal{R} \nsubseteq \approx$ but $\mathcal{R} \subseteq \, \approx \! \mathcal{R} \approx$. Why is $\mathcal{R} \subseteq \, \approx \! \mathcal{R} \approx$?

Actually, the inclusion $\mathcal{R} \subseteq \, \approx \! \mathcal{R} \approx$ holds for any relation $\mathcal{R}$, and not just the one mentioned. Indeed, if we have $P \mathcal{R} Q$, then we also have $P \approx P \mathcal{R} Q \approx Q$, by reflexivity of weak bisimulation.

1. According to Sangiorgi's book, P uses $\tau$ and ends up with $a \approx \tau.a$ and Q has $0$ and ignores the move. I am wondering, how is it that you can ignore the move? I thought that one is forced to do a move...

You have to check that $0\xrightarrow{{\hat\tau}} 0$, which (if I remember correctly) is defined as $0\xrightarrow{{\tau}}^* 0$ which holds since the Kleene's star includes "zero steps".

I seem to remember that the "$\hat\alpha$" move definition made a special case for $\hat\tau$, specifically to allow for zero steps.

• but based on the definition, what move can play 0 as visible move? I am missing how you prove the right to left – Kiko Fernandez Feb 3 '18 at 6:16
• @KikoFernandez I don't understand your question. For any $x$ and relation $R$, we have $xR^*x$ by definition of the $*$. It does not matter that $x$ is a process ($0$, in this case) and that $R$ is the transition relation -- only the Kleene's star matters for this. It also does not matter that $0$ makes no move at all. – chi Feb 3 '18 at 10:12
• I mean that for the right to left direction, which is point 2: $Q \to^\alpha Q'$ then $P \to^\widehat{\alpha} P'$ for some $P'$ s.t. $P'\ \mathcal{R}\ Q'$, the process Q in this case is $0$ and has to play an $\alpha$ move, which either is either $\tau$ or some visible action. But it cannot play any moves! I thought that the definition of $\to$ forces a move, so the Kleene's star is only valid for $\widehat{\alpha}$ – Kiko Fernandez Feb 3 '18 at 19:33
• @KikoFernandez In such case the hypothesis is false, and from that we can conclude anything. False implies anything. As you say, $0$ can not move, so assuming $0 \to^\alpha Q'$ we can prove any thesis. In such cases sometimes one says that the implication is "vacuously true". – chi Feb 3 '18 at 20:58