Non Equivalent Formulae 2021-02-17. 7c

Question

S1 = E[EFa U b]

S2 = b or (EFa) & (EXb) or EF(b & EFa)

Would this Kripke structure be sufficient to satisfy S1 and not S2

My understanding is that it satisfies [EFa U b] because of the weak until operator and thus E[EF a U b] is satisfied. But for the second formula, b is never satisfied anywhere so  EF(b & EFa) is never true and (EXb) is also never true. Since & bings stronger than or, the second formula is never satisfied. 

Did i go in the right direction? Is there an approach to solve these kinds of questions that generally applies to all of them or is it just the intuition about the formulae that counts?

Answer 1

You can use the CTL model check to answer your question: With input

vars a,b;
init 0;
labels 0:a; 
transitions 0->0;

E[E F a WU b];
b ∨ (E F a) ∧ (E X b) ∨ E F(b ∧ E F a)

You will see that the state of your structure satisfies EF a, and therefore also E[E F a WU b] (note that b never becomes true, so that the weak until demands that EG EF a holds which is true). 

In contrast, neither b nor (EF a) ∧ (EX b) nor EF(b ∧ EF a) holds on that path. 

So your structure distinguishes correctly between the two formulas.