0 votes
ϕ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?
in * TF "Emb. Sys. and Rob." by (550 points)

1 Answer

0 votes
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.
by (98k points)
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.

Related questions

0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
Imprint | Privacy Policy
...