LTL Model checking

Question

In this solution, why wasn't q4 included in the state set, G[Fa U b] is represented as q4.

Also if i had added the fairness constraints for q3 and q4 it would still be a correct solution right ?

Answer 1

That seems to be a mistake. q4 must also be added to the set of state variables. Fairness constraints for q3 and q4 are not needed, but it is not wrong to add them. Which exam paper was this?

Comments

25th of August 2020

---

Thanks for pointing this out, it has been fixed now.