LTL and CTL equivalence

Question

I would like to understand the difference between the two formulas. My first attempt to answer this question was trying to satisfy S2 with one of these:

In my understanding, both satisfy S2 and not S1. However, I do not understand how the solution given satisfies S1.

Can someone please clarify?

Answer 1

It looks good! Consider the structure in the example solution:

             0 1 2 3 4 5 6
           a 0 0 0 0 0 0 ...
           b 1 0 1 0 1 0 ...
    [a SU b] 1 0 1 0 1 0 ...
   X[a SU b] 0 1 0 1 0 1 ...
          Xa 0 0 0 0 0 0 ...
   [Xa SU b] 1 0 1 0 1 0 ...

Note that [a SU b] becomes equivalent to "b" if "a" is always false. Thus, the two formulas X[a SU b] and [Xa SU b] just become equivalent to Xb and b, respectively.

Your first structure generates the following

             0 1 2 3 4 5 6
           a 0 1 0 0 0 0 ...
           b 0 0 1 1 1 1 ...
    [a SU b] 0 1 1 1 1 1 ...
   X[a SU b] 1 1 1 1 1 1 ...
          Xa 1 0 0 0 0 0 ...
           b 0 0 1 1 1 1 ...
   [Xa SU b] 0 0 1 1 1 1 ...

So, here X[a SU b] holds, and [Xa SU b] is false. 

Finally, your second structure:

             0 1 2 3 4 5 6
           a 0 0 0 0 0 0 ...
           b 0 1 1 1 1 1 ...
    [a SU b] 0 1 1 1 1 1 ...
   X[a SU b] 1 1 1 1 1 1 ...
          Xa 0 0 0 0 0 0 ...
           b 0 1 1 1 1 1 ...
   [Xa SU b] 0 1 1 1 1 1 ...

Again, here X[a SU b] holds, and [Xa SU b] is false. 

Comments

Thank you very much for the instructive answer! It clarified everything.