. CTL, LTL and CTL∗

Question

^{what can be solution for below question:}

S1 = ¬XX (G(a ⊕ b) ⊕ F(a ↔ b)) S2 = XXG((a ⊕ Xa) ∧ (b ⊕ XXb))

Answer 1

See the example solution: G(a ⊕ b) ⊕ F(a ↔ b) = G(a ⊕ b) ⊕ ¬¬F(a ↔ b) = G(a ⊕ b) ⊕ ¬G(a ⊕ b) = 1, thus S1 is false, and we just need to satisfy S2. We first ignore the XX and add two states later to adjust that, and consider now G((a ⊕ Xa) ∧ (b ⊕ XXb)) = G(a ⊕ Xa) ∧ G(b ⊕ XXb). 

G(a ⊕ Xa) means that a must always toggle its value when following transitions, and G(b ⊕ XXb) means that b does so with a period of 2. So, for example, we could create a model by repeating the following four states in a cycle: {a,b} -> {b} -> {a} -> {}