CTL & LTL equivalence

Question

From September 2022:

For (c) I answered with what in (d) is represented in path S0(S2ˆ(omega)) to satisfy formula S2. Is that correct?

Then in (d) I am confused by the answer, how can {s0,s2} satisfy S2? 

I thought it would hold if the initial state was directly s2.

I read the formulas as:

S1: There exists a path where eventually a is strong until b

S2: There exists a path where exists a path where eventually a is strong until b

Is something wrong with my understanding?

Thank you in advance

Answer 1

Consider the path s0->s2->s2... of the structure in solution (d)

             0 1 2 3 4 5 6
           a 0 0 0 0 0 0 ...
           b 0 1 1 1 1 1 ...
    [a SB b] 0 0 0 0 0 0 ...
          !a 1 1 1 1 1 1 ...
   [!a SU b] 1 1 1 1 1 1 ...

So, [!a SU b] holds, and [a SB b] is false, so your are right!