Linear Temporal Logic Questions (2)

If you are not familiar with LTL (linear temporal logic), please skip this quest开发者_开发问答ion! 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.

I think that

Fp means that P will finally hold (somewhere on the subsequent path).

So, GFp should mean that p will hold somewhere on the subsequent path, wherever in teh path you will be "standing". Or, in other words, p will hold in an infinite subsequent places of the path.

FGp should mean that there is a place on the subsequent path where p stands always from then on.

I'm not sure but GFGp could be proven the same as FGp

and FGFp the same as GFp.

To make things easier to understand, I will use the alternative notation:

G = globally = [] = always
F = finally = <> = eventually

So []<>p means that p occurs infinitely often, i.e., it never stops occurring. For example **p ******* p*****p***p***...

The formula <>[]p means that there's some place in the sequence, after which only p occurs uninterrupted. For example ***ppppp...

Now <>[]<>p means that eventually p will be occurring infinitely often, which is exactly the same as p occurring infinitely often, i.e., <.[]<>p=[]<>p.

Similarly, []<>[]p means that from any point in time on, eventually always p. But this is exactly saying that eventually p, so []<>[]p=<>[]p.

GFGp = FGp example: all dogs eventually go to heaven, and some day will stay there forever

FGFp = GFp : sooner or latter all dogs go to heaven (and if they descend/reborn etc on earth they will go to haven again).