Doubt in LTL Satisfiability

Question

According to the explanation given for EG!a above, I did not understand why is there a need for s0->s1? Doesn't the path s0->s2 satisfies EG!a as well? Can someone explain this? 

Answer 1

If you will drop the transition s0->s1, then there is no longer a path starting in s0 that would satisfy G!a, so that EG!a is then no longer true in s0. To satisfy property S1, we need both the paths s0->s1^omega as well as s0->s2^omega. For the outermost E of E(Fb & EG!a), we use the path s0->s2^omega which satisfies Fb & EG!a since b is reached on s2, and in state s0, we also have EG!a (because the other path is there).

So, property S1 holds in s0, but property S2 does not.