CTL, LTL and CTL*

Question

1. S1 = EF((X(a → b)) ⊕ (a → b))

   S2 = EF((a ∧ ¬b) ∧ X(a → b))

Can I draw a path with

 with states s0(initial state) and s1 with b in s0 and a in s1 with an infinite loop on s1 ? I am guessing this would satisfy S1 but not S2 since state s0 has a in it?

2.  S1 = ¬XX (G(a ⊕ b) ⊕ F(a ↔ b))

     S2 = XXG((a ⊕ Xa) ∧ (b ⊕ XXb))

Can I draw a path with states s0 (initial state), s1 and s2. Both states s0 and s1 are empty and s2 has {a,b} in it with an infinite loop. I believe this will satisfy S2 since S1 is always false.

3. S1 = c ∧ F [b U G(¬a ↔ Xa)]

    S2 = c ∧ [(Fb) U G(¬a ↔ Xa)]

Can I draw a path with states s0 (initial state), s1 and s2. State s0 has c, s1 is empty and s2 has {a} with an infinite loop. (in the exam solutions states s1 and s2 have an alternating loop. Is it alright if I draw an infinite loop on s2?) I believe it would still satisfy S1 and not S2.

Answer 1

If you have a Kripke structure with just one infinite path, then the path quantifiers don't matter, i.e., E and A become the same, and you can express that in LTL as well. For example, you can check whether your ideas are right as follows using the LTL prover: 

First example: 

    S1 = EF((X(a → b)) ⊕ (a → b))
    S2 = EF((a ∧ ¬b) ∧ X(a → b))

You can prove the following to see that you are right:

    (!a&b) & (X G(a&!b)) -> F((X(a → b)) ⊕ (a → b))
    (!a&b) & (X G(a&!b)) -> !F((a ∧ ¬b) ∧ X(a → b))

and you can see that also with the following traces:

                            a : 01...
                            b : 10...
                        a → b : 10...
                     X(a → b) : 00...
                       a ∧ ¬b : 01...
         (X(a → b)) ⊕ (a → b) : 10...
          (a ∧ ¬b) ∧ X(a → b) : 00...

Second example: First note that G(a⊕b) = ¬F(a↔b), hence, G(a⊕b) ⊕ F(a↔b) is true, so that S1 is always false and we focus on satisfying S2 = XXG((a ⊕ Xa) ∧ (b ⊕ XXb)). I think that you are wrong due to the following traces:

                a : 00 11
                b : 00 11
               Xa : 01 11
             a⊕Xa : 01 00
              XXb : 11 11
            b⊕XXb : 11 00
   (a⊕Xa)∧(b⊕XXb) : 01 00

Third example: I guess these were SU (?):

    S1 = c ∧ F[b SU G(¬a ↔ X a)]
    S2 = c ∧ [(F b) SU G(¬a ↔ X a)]

             a : 00 11
             b : 00 00
             c : 10 00
            Xa : 01 11
         ¬a↔Xa : 01 00
      G(¬a↔Xa) : 00 00

and thus the SU will be false.

Maybe I made mistakes, please check!