Translation between different logics

Question

How FGb is translated to EFGb ?

Does that mean FGb can be written as EFGb ?

Answer 1

FG b is not equivalent to EFG b, since the former is a path formula and the latter is a state formula. Above, the context makes the two exchangeable. The E quantifier comes from the outer A quantifier and is generated by the following rule (page 42):

A[ψ B φ] = A[ψ B (Eφ)]

Comments

I understood.
Thank you for clarifying this.