Translation between different logics

Question

ϕ3 = (EGFGF¬F(b ↔ a)) → c

= ¬(EGFGF¬F(b ↔ a)) ∨ c

= (AFGFGF(b ↔ a)) ∨ c

= (AGF(b ↔ a)) ∨ c // Since an alternation of F, G, ending in F is equal to GF

= A(c ∨GF(b ↔ a))

= (c ∨ AGAF(b ↔ a))

in above solution they have combined GFGF  as GF

so Can we write AXAX as AX?

Answer 1

No, you cannot: GF phi means that phi holds infinitely often on a path, and thus, GF GF phi does not say more than that. However, X phi says that phi holds at the next point of time, and X X phi means that phi holds two points of time after the considered one. That is not absorbed, and has a different meaning. However, you have that G G p is equivalent to G p and also F F p is equivalent to F p.

Comments

thank you, can we write FG/EG = G.

---

No, since Gp means for a path that p always holds on that path, while FG p means that after some point of time, p always holds. What happens before that point does not matter.

EGp on the other hand is a state formula that holds on a state if that state has an outgoing path where always p holds. We should not compare state and path formulas since the former demands something on states while the latter specifies properties of paths. That is not comparable.