# Drawing a labelled transition system (LTS)

1. Jun 29, 2014

### XodoX

1. The problem statement, all variables and given/known data

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

2. Relevant equations

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

Those are the equations and how p1 is defined.

3. 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.

2. Jun 29, 2014

### Zondrina

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?

Last edited: Jun 29, 2014
3. Jun 30, 2014

### 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.