# Linear temporal logic in computational trees

I came across these slides while learning about the differences between CTL and LTL and am confused about what is written in the last slide.

The problem is proving that $GF p \implies GF q$ and $AG AF p \implies AG AF q$ are not equivalent.

My doubt lies in whether $GF p \implies GF q$ is true or not. Till now, I was working with the assumption that an LTL formula is true in a computational tree iff it is true for all paths in the tree. So according to me, $GF p$ is false which makes the statement true.

But the slides say that in the path where we keep looping in $s_0$, $GF p$ is true and $GF q$ is false, so the statement is false.

Where is the fault in my logic?

• Any reason for the downvote? There have been questions like this here in the past, like this one. – Akshit Apr 30 '18 at 20:36

This question should (and will) probably be migrated to cs.se. In the meantime, consider the computation tree of the depicted structure: in almost all paths, $p$ is seen only finitely often, making the premise of $GFp\to GFq$ false, so the formula is satisfied there.

However, there is one path, namely $s_0^\omega$, in which $GFp$ does hold, but in this path $GFq$ does not hold.

We conclude that there exists a path on which the formula doesn't hold, so it is not the case that it is satisfied on every path. Thus, the formula is not satisfied in this structure.

• I have 2 doubts (both inter-related): firstly, why are you evaluating $GF p \implies GF q$ instead of just $GF p$ first? Secondly, why is $GF q$ evaluated on the same path as $GF p$? Aren't the $GF$ on the different sides of the arrow independent of each other? – Akshit Apr 30 '18 at 19:06
• in LTL you evaluate whole formula on all paths (not term by term). Never evaluate LTL part by part. Check the definition and my answer. – Serge Apr 30 '18 at 19:10
• you said " Till now, I was working with the assumption that an LTL formula is true in a computational tree iff it is true for all paths in the tree." PLEASE STICK TO THAT ASSUMPTION – Serge Apr 30 '18 at 19:12
• A model, or Kripke structure, satisfies an LTL formula, when all its paths do. (page 17) – Serge Apr 30 '18 at 19:23
• The conjunction, disjunction and negation are called 'deliberate puns', and their path semantic is defined for individual path only on page 10 earlier. The satisfaction of a formula by a model is defined as above on page 17. Hence you evaluate whole formula on each of path, not by applying boolean logic to fragments of formula. – Serge Apr 30 '18 at 19:28

## The flaw in your reasoning

According to you GF p is false ( and it is not satisfied by model speaking more properly). Yet your fault in assuming, than akin to Boolean logic, it make the whole LTL formula true. It does not. The only way is to evaluate an LTL formula is on all the model paths (see page 17 of you slides for the definition), not part by part, and as other answers explaines GF p => GF q does not holds on the $s_0$ loop.

## Difference between LTL and Boolean Logic

The example just shown that contrary to usual Boolean logic as well as CTL, even if LTL formula X is satisfied X->Y might be still do not satisfy the model. Material implication inference does not work here.

Many seemingly simple and intuitive inference laws valid for Boolean logic are not applicable to LTL. You might be well surprised, that even if X does not satisfies model, not X not necessarily. Check you lecture notes to see which inference rules work in LTL.

I guess you were assuming that only properly temporal operators, such as G and F need to be defined, while rest could be interpreted based on your intuition or previous experience with boolean logic. It is not the case, in Theoretical Computer Science the definition is your primary reference.

• can you check the comments I posted on Shaull's answer? – Akshit Apr 30 '18 at 19:08