3
$\begingroup$

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.

$\endgroup$
2
$\begingroup$

(partial answer)

  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.

$\endgroup$
  • $\begingroup$ but based on the definition, what move can play 0 as visible move? I am missing how you prove the right to left $\endgroup$ – Kiko Fernandez Feb 3 '18 at 6:16
  • $\begingroup$ @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. $\endgroup$ – chi Feb 3 '18 at 10:12
  • $\begingroup$ 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}$ $\endgroup$ – Kiko Fernandez Feb 3 '18 at 19:33
  • $\begingroup$ @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". $\endgroup$ – chi Feb 3 '18 at 20:58

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.