Drawing a labelled transition system (LTS)

[XodoX]

Homework Statement

I want to draw an LTS with as few transitions as possible. The basis for this are Hennessy-Milner equations

Homework Equations

https://www.dropbox.com/s/ym3ygjdnhldz09r/HML Equations.jpg

Those are the equations and how p1 is defined.

The Attempt at a Solution

https://www.dropbox.com/s/fjxmulj8q9cjatr/LTS.jpg

No idea if that's correct. Can anybody confirm this? Don't think it can be less than that, though.

 

[STEMucator]

For reference, are you talking about these: http://en.wikipedia.org/wiki/Hennessy–Milner_logic ?

Some of the notation in the relevant equations seems a bit obscure. Are you assuming the existence of $\phi$ for the $L$ derivatives?

Are you simply trying to evaluate the logic in the most effective manner? i.e the least amount of states?

 

[XodoX]

Yeah, HML. The least amount of states. Right now it's 4. I have no idea if that's correct and/or if there is more than one solution. But this one above is what I have and it seems logical to me. I'm not 100% sure.