# Linear Temporal Logic (LTL) Syntax Infinitely Often

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.