Determining set of states that satisfy a CTL formulae

Question

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:

1. 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.
2. 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?

Answer 1

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.