# How to draw an LTS based on the parallel process “|” in CCS Milner's logic?

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): 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]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: 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.

• 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. – chi May 14 '19 at 12:33
• @chi Like this imgur.com/a/p78PUVj ? – Does it matter May 14 '19 at 14:36
• @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. – Does it matter May 14 '19 at 14:44
• And maybe it's an idea to introduce Hennessy–Milner logic tag? You can do it as you have enough reputation. – Does it matter May 14 '19 at 14:46

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.