<p>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 <em>is</em> satisfied there.</p>

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

<p>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.</p>

CC BY-SA 3.0
2018-04-30T19:06:49.447Z
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
CC BY-SA 3.0
2018-04-30T19:10:20.010Z
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
CC BY-SA 3.0
2018-04-30T19:12:35.843Z
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
CC BY-SA 3.0
2018-04-30T19:23:00.333Z
A model, or Kripke structure, satisfies an LTL formula, when
all its paths do. (page 17)
Serge
CC BY-SA 3.0
2018-04-30T19:28:24.330Z
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
CC BY-SA 3.0
2018-04-30T20:29:03.857Z
That cleared up my doubts nicely. Just one quick and final question : what would have happened it were a formula in CTL* (I couldn't find any good resource for it, so I don't know how to work it out there) ? Would the same truth value hold?
Akshit
CC BY-SA 3.0
2018-04-30T20:33:13.097Z
A(GFp -> GFq) is not satisfied in this model.
Serge
CC BY-SA 3.0
2018-04-30T20:41:38.007Z
AGAFp ⟹ AGAFq is satisfied. GFp -> GFq is malformed. https://en.wikipedia.org/wiki/CTL* for the definition.
Serge
CC BY-SA 3.0
2018-04-30T18:14:25.020Z
2018-04-30T18:14:25.020Z
Shaull
<h2>The flaw in your reasoning</h2>

<p>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. </p>

<h2>Difference between LTL and Boolean Logic</h2>

<p>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. </p>

<p>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.</p>

<p>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.</p>

CC BY-SA 3.0
2018-04-30T19:08:15.857Z
can you check the comments I posted on Shaull's answer?
Akshit
CC BY-SA 3.0
2018-04-30T17:29:47.030Z
2018-05-01T01:33:39.710Z
2018-05-01T01:33:39.710Z
Serge
<p>I came across <a href="http://www.cs.utexas.edu/users/moore/acl2/seminar/2010.05-19-krug/slides.pdf" rel="nofollow noreferrer">these slides</a> while learning about the differences between CTL and LTL and am confused about what is written in the last slide.</p>

<p>The problem is proving that $GF p \implies GF q$ and $ AG AF p \implies AG AF q$ are not equivalent.<a href="https://i.sstatic.net/COMhH.png" rel="nofollow noreferrer"><img src="https://i.sstatic.net/COMhH.png" alt="enter image description here"></a></p>

<p>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.</p>

<p>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. </p>

<p>Where is the fault in my logic?</p>

CC BY-SA 3.0
2018-04-30T20:36:05.463Z
Any reason for the downvote? There have been questions like this here in the past, like [this one](https://cstheory.stackexchange.com/questions/21866/ctl-and-ltl-logic-difference?rq=1).
Akshit
<temporal-logic><linear-temporal-logic>
Linear temporal logic in computational trees
Akshit
# Linear temporal logic in computational trees

(Asked by: username_0 on 2018-04-30)

I came across [these slides](http://www.cs.utexas.edu/users/moore/acl2/seminar/2010.05-19-krug/slides.pdf) 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.[![enter image description here](https://i.sstatic.net/COMhH.png)](https://i.sstatic.net/COMhH.png)

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?

**Tags:** temporal-logic, linear-temporal-logic

> **Comments:**
> **username_0**: Any reason for the downvote? There have been questions like this here in the past, like [this one](https://cstheory.stackexchange.com/questions/21866/ctl-and-ltl-logic-difference?rq=1).  

---

## 2 answers

### Answer by username_1 on 2018-04-30. Score: 1 | Accepted answer

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.

> **Comments:**
> **username_0**: 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?  
> **username_2**: 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.  
> **username_2**: 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  
> **username_2**: A model, or Kripke structure, satisfies an LTL formula, when all its paths do. (page 17)  
> **username_2**: 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.  
> **username_0**: That cleared up my doubts nicely. Just one quick and final question : what would have happened it were a formula in CTL* (I couldn't find any good resource for it, so I don't know how to work it out there) ? Would the same truth value hold?  
> **username_2**: A(GFp -> GFq) is not satisfied in this model.  
> **username_2**: AGAFp ⟹ AGAFq is satisfied. GFp -> GFq is malformed. https://en.wikipedia.org/wiki/CTL* for the definition.  

---

### Answer by username_2 on 2018-04-30. Score: 0

## 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.

> **Comments:**
> **username_0**: can you check the comments I posted on username_1's answer?  

---

