LTL equivalnace

Question

Hello All,

Could someone help with the interpretation of the XOR in this question? What does XOR mean in this context?

Answer 1

As we have ¬F¬a = Ga, and p⊕¬p = 1, it follows that S1 is always true. S2, however, can become false, as you can see with the following traces:

                a : 0101...
               Ga : 0000...
              XGa : 0000...
               !a : 1010...
              G!a : 0000...
      (XGa)⊕(G!a) : 0000...

Here, you can see that the ⊕ operator (just as any other boolean operator) will be applied to the corresponding points of time of the two inputs, i.e., p⊕q denotes pointwise xor of the signal p and q. 

Comments

Thank you for the explanation.