Doubt in Temporal Logic

Question

How did we get the new equation (a|XG-a) from the question? Can someone please explain?

Answer 1

Note that Fa is equivalent to a ⋁ XFa, so that a<->Fa is equivalent to a<->(a ⋁ XFa). Now, if a is true, so is that equivalence, and if a is false, then we get 0<->(0 ⋁ XFa) which is !XFa, i.e., XG!a.

You can also argue like this:

    a<->(a ⋁ XFa)
    = a⋀(a ⋁ XFa) ⋁ !a⋀!(a ⋁ XFa)
    = a ⋁ !a⋀!(a ⋁ XFa)
    = a ⋁ !a⋀!a ⋀ !XFa
    = a ⋁ !a⋀!XFa
    = a ⋁ !a⋀XG!a
    = a ⋁ XG!a