Path and temporal qualifiers

Question

I am a bit confused about the meaning and combination of "E","A","F","G".

for example AFGa: does that mean: in all paths,eventually "a" always holds?

Answer 1

Yes, you have to read it from left to right: AFGa means on all infinite paths (A), eventually comes a point of time (F) so that from there on, always (G) a holds. But what would you say about A F E G PF a where PF means past-F?

Comments

AFEG: if my understanding is correct in all infinite paths, eventually , there exist a path in which something always holds... I didn't understand what is PF.

---

I agree. Important to note there is maybe that each new path quantifier (whether E or A) restarts time with t=0. PF should be the past-form of F (see http://es.cs.uni-kl.de/tools/teaching/QuartzRef.pdf whose syntax is used by the teaching tools). Note that the combination G PF a is vacuous, i.e., equivalent to a (equivalence to G a has been erroneously stated here before which is wrong as Sören points out below), so that also A F E G PF a is equivalent to AF EG a.

---

Thanks for the information.

---

First: Oh,I fail the time reset of A and E. Most of the time the tasked was looking in the future anyway.

Second: I'm not convinced that G PF a is equivalent to  G a. Because I think of the sequence t=0 a;t>=1 !a.
I thought there for each position t (Globally) we could look back in the past and find finally 'a' at t=0.

---

Very good!! You are right with your doubt. G PF a is not equivalent to G a, as your counterexample shows. I should have said that G PF a is equivalent to a, since a must hold at initial time for sure, and ensures at any later point of time that PF a holds.