1
$\begingroup$

I have already posted this question on the other page, but I was suggested to post it here as it might be more relevant.

I am currently following a course in concurrency theory and I am currently trying to prove that the Weak Bisimulation relation ≈ is an equivalence relation.

I have managed to prove cases for reflexivity and symmetry, however I can't seem to make the connection for transitivity. Does any one have any clues how can I go about this ?

I have tried the relation {(P,R) | ∃Q.P≈Q,and Q≈R} as my witness relation and then at one point I get stuck.

I assumed that P->a P' which gives me that there is Q =>a Q' and that P' ≈ Q' Now the thing is that since Q =>a Q' then by the definition of => Q ->tau* Q1 ->a Q2 ->tau* Q' Q1 ->a Q2 will cause some R1=>a R2 such that Q2 ≈ R2 Then I am not sure how to proceed to show that somehow there is a transition R =>a R' such that (P', R') are in R. May be I believe I have to use numerical induction on the number of tau ?

Thanks !

$\endgroup$
1
  • $\begingroup$ What other page are you referring to? Ah, I see, you previously asked on CSTheory.SE: cstheory.stackexchange.com/q/33221/5038. For future reference, please don't ask the same question on multiple Stack Exchange sites -- we want each site to have a fair shot at answering. $\endgroup$ – D.W. Dec 1 '15 at 6:45
2
$\begingroup$

You are on the right track. It can be useful to prove the following lemma: if $\sim$ is a weak bisimulation, if $P\sim Q$ and if you have a sequence of transitions $P\xrightarrow{w}P'$ for $w\in (Act\cup\{\tau\})^*$ then there must be a sequence $Q\xrightarrow{w'}Q'$ with $P'\sim Q'$ and $w =_{\tau} w'$, i.e., $w$ and $w'$ are "the same modulo $\tau$". This can be done by induction on $w$, and it will come in handy when you deal with transitivity. Check that $u=_\tau u'$ and $v=_\tau v'$ imply $uv=_\tau u'v'$, i.e., that $=_\tau$ is a congruence.

$\endgroup$

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.