Question

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.

No correct solution

Licensed under: CC-BY-SA with attribution
Not affiliated with cs.stackexchange
scroll top