1
$\begingroup$

I'm trying to provide a Hennessy-Milner logic formula for CCS expressions that are not (strongly) bisimilar. An example with a sketch:

For each of the following CCS expressions, decide whether they are strongly bisimilar and if no, find a distinguishing formula in Hennessy-Milner logic.

$b.a.Nil+b.Nil$ and $b(a.Nil+b.Nil)$

I first draw these two to get a better understanding as follows (excuse my awful drawing skills but I couldn't figure out how to put it in LaTeX so I used draw.io):

enter image description here

You can clearly see the Right Hand Side could do $b.b$ but the Left Hand Side can't respond to that. And my distinguishing HML formula is $[b]<b>tt$. On the LHS you get: $[b]\{b.a.Nil+b.Nil\} = \emptyset$ and on the RHS you get: $[b]\{b(a.Nil+b.Nil), a.Nil+b.Nil\} = b(a.Nil+b.Nil)$. Therefore this is a valid distinguishing formula.

Hopefully, I made what the exercise is about clear. Now, the following CCS expressions that I have to distinguish are:

$a.Nil|b.Nil$ and $a.b.Nil + b.a.Nil$.

I know how to draw the RHS because the + denotes a choice but I don't have any idea of how the parallelism work in CCS and couldn't understand it after reading. My guess is the following but it doesn't make sense and is probably wrong:

enter image description here

Could someone help me understand how to sketch the LHS so that I can complete this exercise?

P.S My tags are probably not correct but I couldn't find any tags to Hennessy-Milner logic, so feel free to edit them.

$\endgroup$
  • 1
    $\begingroup$ Your last LTS is wrong, it should be a diamond-shaped graph, where on one side you perform a then b, and on the other b then a, both sides leading to Nil. Also note that if you can't distinguish between two processes, maybe they are bisimilar, and you could try proving that instead. $\endgroup$ – chi May 14 at 12:33
  • $\begingroup$ @chi Like this imgur.com/a/p78PUVj ? $\endgroup$ – Does it matter May 14 at 14:36
  • $\begingroup$ @chi If my drawing is correct, then your comment is exactly what I needed. Please feel free to add your comment as an answer so that I can accept it. $\endgroup$ – Does it matter May 14 at 14:44
  • $\begingroup$ And maybe it's an idea to introduce Hennessy–Milner logic tag? You can do it as you have enough reputation. $\endgroup$ – Does it matter May 14 at 14:46
2
$\begingroup$

The last LTS in your question is wrong. It should be a diamond-shaped graph, where on one side you perform action $a$ then $b$, and on the other you perform action $b$ then $a$, both sides leading to $\sf Nil$.

This is because the $a$ action is run in parallel w.r.t. the $b$ action, so we get all the possible "interleavings" between such events.

The fixed LTS you posted in the comments looks right, instead.

$\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.