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.