CTL, LTL and CTL∗

Question

Please could someone explain on exam 2020.02.19 question 7.a ?  I am not sure how shall I solve this question, may advice any clue?

Edit: New Question:

Thanks in advance.

Answer 1

First, you should understand in that example that ¬XX(G(a⊕b)⊕F(a↔b)) is just false: Note that ¬G(a⊕b) = F¬(a⊕b) = F(a↔b), and since in general, p⊕p = false holds, we have G(a⊕b)⊕F(a↔b) = false. Thus, we have ¬XX false which is also false. To distinguish formulas S1 and S2, we therefore need to find a path that satisfies S2 since no path can satisfy S1. 

Now consider S2 = XXG((a⊕Xa)∧(b⊕XXb)): To satisfy this, we use some arbitrary two first states s0 and s1 on our path and from there we should satisfy G((a⊕Xa)∧(b⊕XXb)) which is equivalent to G(a⊕Xa) ∧ G(b⊕XXb). Hence, whenever we have a, next time we must not have a, and whenever we have b, it should be false two steps later. From here, you should understand the solution.

Comments

You wrote
¬G(a⊕b) = F¬(a⊕b) = F(a↔b) and p⊕p = false

but p⊕¬p = true

which implies: G(a⊕b)⊕F(a↔b) :=  G(a⊕b)⊕¬G(a⊕b) = true
therefore, ¬XX true = XX ¬true = false.

Correct me if I am wrong.

Follow up question: if S1 is false then no path can satisfy it and if S1 is true then, is it satisfied by all the paths?

---

Yes, we have G(a⊕b)⊕F(a↔b) = G(a⊕b)⊕¬G(a⊕b), thus, we don't need p⊕p = false, but instead p⊕¬p = true.  

Follow up question: yes!

---

New question: since b should be false in two steps later, may clarify how b became 10(0110) in XXb, should not it be 10(0100)? Please may correct me if I am wrong.

---

As we have b = 00(1001), we have XXb = 10(0110) that is correct in the example solution. What is that so? Maybe you see that clearer when I am writing the values of b[t]. We have b[0]=0, b[1]=0, b[2]=1, b[3]=0, b[4]=0, b[5]=1, and so on. Hence, (XXb)[t] = (Xb)[t+1] = b[t+2], and thus, (XXb)[0]=b[2]=1, (XXb)[1]=b[3]=0, (XXb)[2]=b[4]=0, (XXb)[3]=b[5]=1, and so on.

---

Thanks for your response. I am clear on above details, my doubt is:
 - why (XXb)[4]=b[6] = 1? it is because again 1001... input in incoming next times?
 - why (XXb)[5]=b[7] = 0?
since, there are not b[6] and b[7]. Thanks in advance.

---

Yes, the omega symbol means an infinite repetition of 1001.