LTL,CTL, CTL*

Question

Is this also correct.

In this [a SU b] holds in an infinite loop so globally. whereas Ga does not hold. 

So S1 is satisfied and S2 is not.

Answer 1

Yes, that is true which you can check with the LTL prover:

(a&!b) & 
G( ((a&!b)->X(!a&b)) & 
   ((!a&b)->X(a&!b)) 
 ) 
-> !((G a) & (F b)) & (G[a SU b])