LTL and CTL semantic Xpast and X future operator

Question

The Que is from 2016 sept prob 7.b

How is (past(X)a <->a) = Ga //why not Ga V G neg(a)

Answer 1

The PSX (past-strong-X) and PWX (past-weak-X) are defined such that they check whether their argument formula φ holds on the point of time right before the considered point of time. They differ at the initial point of time: PSXφ is false there, and PWXφ is true there.

Now, consider G((PWX a) <-> a): It means, that (PWX a) <-> a holds at all points of time. At time 0, this means true<->a since PWX a is true there, and at time 1, it means a(0) <-> a(1), and thus a(1) must hold, and so on. Thus, always a(t) holds, and that means Ga holds.