CTL equivalences

Question

Hello,

the question is: why is AG(a ↔ Xa) = A(Ga ∨ G¬a) ?
The equivalence was used in the solution for the exam from 06.09.2016 in Task 7b).

I see that AG(a ↔ Xa) = A (G (¬a ∨ X a) & G (¬X a ∨ a)) but how does that translate to A(Ga ∨ G¬a) ?

Thank you!

Answer 1

a <-> Xa = aaaaa or neg(a) neg(a0......

hence I think G(a) V G(neg(a))....

Comments

Absolutely right. Maybe I should add something about AG(a ↔ Xa).

It requires that all paths satisfy at any point in time that the next state in the path has an a if and only if the current one has one. This means, there cannot be any place where there is a change between ¬a and a or between a and ¬a. Hence, the only two paths satisfying this formula are a^omega and (¬a)^omega. And these are the paths described by Ga ∨ G¬a.

Answer 2

Forget about the A-quantifier, and consider G(a ↔ Xa) and let's find all of its models. Variable a may be initially either true or false. If it is false, then also ¬Xa must hold, since a ↔ Xa must be true at time 0. Same for time 1, and so on and by induction, we see that in that case G¬a holds.

If "a" would be initially true, the same arguments will prove that Ga holds.

Hence, G(a ↔ Xa) implies that we either have Ga or G¬a. Conversely, Ga and also G¬a imply G(a ↔ Xa).