Path and temporal qualifiers

+1 vote
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?

+1 vote

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?
by (147k points)
selected by
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.