If you are not familiar with LTL (linear temporal logic), please skip this question! And yes, LTL is very significant to programming, as it is a core to the model checking system we use to verify programs.
Given these proposition symbols and their meanings...
Gp - always P
Fp - sometimes P
What do the following statements mean?
GFGp = ?
FGFp = ?
I'm having a hard time with the logic surrounding LTL, and can't wrap my head around the above statements, thanks for any help!
Some terminology first:
Well-formed formulae are sentences in the logic that satisfy all of the combination rules. Usually there's an inductive definition of this to the effect that atomic propositions are well-formed formulae, and so are the following:
Combinations of well-formed formulae (WFF) with (replacing the usual logical symbols...) &&, ||, !, and => are also well-formed formulae. This is all standard FOL. (Linear) Temporal Logic adds a few more combination possibilities, so that F(WFF), G(WFF) and X(WFF) are themselves well-formed formulae.
Since F(WFF) can itself be a well-formed formulae, we can have F(F(WFF) as a well-formed formulae and so can G(F(F(WFF), and lots of other bizarre-looking agglomerations. But what do they mean?
Speaking personally, I find it useful to think in terms of sets of propositions for the complicated formulae, where G refers to a set of propositions, and F calls out a single proposition. As you mention, given some current node, Fp means that p will occur in at least one of the successors of that node, and Gp means that p will occur in all of the successors of the current node.
So then, GFp
says that every state (after this one) has at least one successor state where p
occurs. So, p
is guaranteed to occur (sometime in the future) after each operation.
FGp
means that there is at least one state (after this one) whose complete set of successors is p
. So there's a point in the process where it's p
's ever after.
Going further FGFp
says that there's some point after which GFp
holds. Again, GFp
requires that p
follows (at least once) from every operation, so the whole thing means roughly that sometime in the future we'll get p
from everything (of course, this could mean that it's all p
's from that point forth or that p
is just the last state).
GFGp
means that the successor of every state is FGp
. I suppose this means that every point in the path has some successor state whose descendants are all p
's (which seems close to, but is not the same, as the whole path is p
's).
Confused yet? I am.