2
$\begingroup$

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?

$\endgroup$
2
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.