Global and local model checking

Question

Question paper for 06.09.2022,
1. Problem 4a (local model checking), how do we split for (a|b->[]x)?

1. Problem 4b (global model checking), how do we get the states for (a|b->[]x)?

Answer 1

An implication p->q is just an abbreviation for !p|q, so that we can use the rules for the latter.  However, there were brackets missing in the example solution that I have now added, maybe that was confusing for you. Please check again!

The same answer could be given for global model checking. Hence, States(p->q) = States(!p|q) = States(!p)∪States(q) = (S\States(p))∪States(q).