Commutative relation of temporal operators

Question

Hello,

While learning for the exam I've found the following two relations in the script:

FGa = GFa
GXa = XGa

And I've wondered if also the combination of all other operators are commutative especially if the following is true: FXa = XFa

Thanks in advance

Comments

I think you missed an X in the first equation, right? If so, please add it. If not, where did you see this equation? It is apparently wrong and needs to be corrected.

Answer 1

Not all of the above are true, so I am wondering where you found them. The X operators commutes with all other future operators, so we have

    G X p = X G p
    F X p = X F p
    [(X p) SU (X q) = X[p SU q]
    [(X p) WU (X q) = X[p WU q]
    [(X p) SB (X q) = X[p SB q]
    [(X p) WB (X q) = X[p WB q]

However, F G p is not equivalent to G F p. The former states that p holds always after some point of time, the latter says that it holds infinitely often. The two are not equivalent. You can check equivalences like these using the LTL tool; simply try (F G p) <-> (G F p) and you will see a counterexample.