CTL, LTL, CTL* [2018.02 8b]

Question

Here, in the path from s0 Fa is valid and a is valid only in s0. Also since the formula S1 is weak until, b does not necessarily have to be true. Hence, it will satisfy formula S1 also, right? 

Since a is not satisfied in s1, a and Gb both are false in s1, hence it does not hold for formula S2 right?

Answer 1

You are wrong with this: On the path s0->s1^omega, "a" holds at t=0, but not for any t>0, and therefore Fa also holds at t=0, but not for any t>0. Variable b does never hold on that path, so S1 becomes equivalent to GFa, which is false on that path. Therefore, S1 does not hold on the path (not for any position t). Note that the weak until demands that the formula (in this case Fa) holds for any t, but it does only hold at t=0 in the example.

S2 holds on the path at t=0 since [(G b) SU a] is equivalent to a|b&X[(G b) SU a] and since "a" holds at t=0, also S2 holds there. S2 does however not hold for any t>0 on the path.

It is however enough that S1 and S2 differ at time t=0 on the path.