CTL LTL equivalance

Question

Consider the following 2 formula-

S1 = AG(PX <-> a) , S2 = AG(a <->Xa) (P means X with an arrow on top)

To me, it looks like S1 = A(Ga | G!a) and also, S2 = A(Ga | G!a), so these 2 formular are equivalent. (a <-> b = (a & b) | (!a | !b), using this)

But i found out that S1 = AGa and S2 = A(Ga | G!a). How did we get rid of the other part in S1? Is there any logic behind this?

Answer 1

It is about the initial point of time. G(a <-> Xa) means that whatever value a had on the initial point of time, that value must be kept on all the following states on the path. Since variable a is either true or false at the initial point of time, you are write that this means that we either have G(a) or G(!a) (depending on the value of a at the initial point of time).

The formula G(PWX a <-> a) means that always a must have the value it had the time before on the path. That sounds same as the formula above, however, it differs at the initial point of time. Regardless of the value of a at the initial point of time, PWX(a) is true at the initial point of time, and PSX(a) is false at the initial point of time. Since you found that S1 is AG a, you have used PWX that forced a to be true at the initial point of time, and that remains so for the rest of the path. If you would use PSX instead, your formula would become AG(!a) instead.