Equivalence of two formulas

Question

S1 = AF(p or q)

S2 = AFp or AFq

I understand the meaning of these two formulas.

But can you explain me how to construct a new kripke structure that one follows and not others. How to interpret this type of problems. Like which formula I try to solve first either s1 or s2

Answer 1

For these kinds of exam problems, I recommend to use your intuition. Once you understood the difference between the two formulas, you should be able to express that difference in terms of a transition system. 

If you don't have that intuition, one way to apprach a difference is to consider the recursion of the temporal logic formulas. In the mentioned case, we get

AF(p∨q) = (p∨q) ∨ AXAF(p∨q) = p ∨ q ∨ AXAF(p∨q)
(AF p)∨(AF q) = (p ∨ AXAF p)∨(q ∨ AXAF q) = p ∨ q ∨ (AXAF p) ∨ (AXAF q)

Hence, both formulas are satisfied if p ∨ q holds, so we have to make both false for a counterexample. Then, you can satisfy the first formula if some successor states satisfy p, but not q, and the remaining successor states satisfy q but not p. Thus, you need an initial state where p and q are false and the two successor states with self-loops.

The above idea with the recursion usually works fine.