Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It only takes a minute to sign up.
Sign up to join this community
I'm a little confused about some LTL syntax.
When the Global and Future operator (GFx) or []<>x is used, what does it mean. In the lecture slides it is given as infinitely often. But I don't understand it.
When used as FGx or <>[]x, I understand it as eventually in the future something will be true forever. E.g. eventually x will become 3 (x = 3) and x will stay as 3 forever.
Can someone explain what GFx means?
Consider just $Fx$. It means that at some point in time, say $t_k$, from the perspective of current moment $t_0$, $x$ will be true. After this moment, $x$ may never again be true. Specificaly, at the moment $t_{k+1}$ the formula $Fx$ may not hold.
If we add $G$, we are saying that at every moment from current moment something most hold. $GFx$, that is $G(Fx)$, says that $Fx$ must hold in every moment, meaning that, in the above situation, even at $t_{k+1}$ $Fx$ holds, that is — there must be some future moment where $x$ holds.
We have that for any moment $t_i$ $Fx$ must hold. That means that for any $t_i$ $x$ must hold at some future $t_j$. Wherever we are in time, $x$ will hold eventually. And that is the same as saying that $x$ holds infinitely many times.
