Exam 2020 7. e)

Question

In the task we are given S2 = EF(q & EG(p & !q)).

1.) Can this even be true at any time? And if so, how would a corresponding Kripke structure look like?

2.) Is there a difference to the formula EF(q & G(p & !q))? This formula cannot be satisfied, right? Because q & G (!q) would need to hold at the same time?

Answer 1

S2 = EF(q & EG(p & !q)) is indeed equivalent to S2 = EF(q & G(p & !q)) and these formulas cannot be satisfied, since as you wrote q contradicts G!q. 

Comments

The example solution is correct, but it only explains that S2 does not hold on the discussed structure. Maybe you would like to read also that it does even not hold anywhere else and that therefore it is sufficient to construct a model for S1. Right, that is the case!