Determining set of states that satisfy a CTL formulae I'm trying to understand CTL formulae, and until now I've understood everything (or at least I thought I did). I have the following Kripke strucure:



Now given the following CTL formulae A(g U EG (b v y)) , which states does it satisfy?

I know that the answer is {s1,s2,s3} (according to lecture notes), but I don't understand that.

This is what I have tried so far to solve it:


I solve EG(b v y) first and for this I get {s1,s3} because from these states there exists a path where either b or y holds globally.  
Then I group it together again and solving A(g U EG(b v y)) which I understand as "Along all paths, g holds until there exist a path where b or y holds" and as I already know the last part of it, I understand it as "Along all paths, g holds until either s1 or s3 holds".


To me s2 is the only obvious answer because g holds in s2 until y holds in s1. I don't understand why s1 or s3, is a part of the answer.

Anyone care to explain? Or at least show the steps you take to derive the answer?
The semantics of the "Until" operator allows for the eventuality to be satisfied immediately. That is, $pUq$ holds both in the computation $ppppq$, but also in $q$.

Thus, in your formula, the eventuality is satisfied immediately in states $s_1,s_3$, and satisfied within 1 step in $s_2$. But all of them satisfy it.