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.

Improve this question
$\endgroup$
4
  • 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, 2019 at 12:33
  • $\begingroup$ @chi Like this imgur.com/a/p78PUVj ? $\endgroup$
    – user82869
    May 14, 2019 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$
    – user82869
    May 14, 2019 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$
    – user82869
    May 14, 2019 at 14:46

1 Answer 1

Reset to default
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.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.