<p>There are already some rather good related answers regarding LTL versus CTL. In a nutshell, LTL is first and foremost a logic of traces, and an LTL formula is true for a transition system $S$ if and only if it is true for each trace of $S$. CTL, on the other hand, is a branching-time logic, which can in a sense talk about multiple paths at the same time. </p>

<p>One standard example here (not the one you give, about which more below) is a labelled transition system $S=(Q,T,q_0,L)$ with set of locations $Q=\{q_0,q_1,q_2\}$, set of transitions $T=\{(q_0,q_0),(q_0,q_1),(q_1,q_2),(q_2,q_2)\}$, and labelling given by $L(q_0)=L(q_2)=\{p\}$, $L(q_1)=\emptyset$. This system satisfies $FGp$, but not $AFAGp$, which can be seen as follows.</p>

<p>$FGp$ means that for every path $\pi=s_1,s_2,\dots$ in a given system, there is some point after which $p$ is always satisfied, i.e. there is some $i$ such that for all $j\geq i$, $p\in L(s_i)$. This is satisfied by $S$ since every path in $S$ either remains in $q_0$ forever (such that $p$ is always satisfied) or eventually gets to $p_2$ (after which $p$ is always satisfied). </p>

<p>On the other hand, $AFAGp$ means that every path $\pi=s_1,s_2,\dots$ eventually reaches a state satisfying $AGp$, i.e. a state such that on <em>every path $\pi'$ starting there</em>, $p$ is always satisfied. Formally, this means that there is an $i$ such that for all $\pi'=s_1',s_2',\dots$ with $s_1'=s_i$ and all $j$, we have $p\in L(s_j')$. But in $S$, for the path which always remains in $q_0$, the transition to $q_1$, where $p$ is not satisfied, is always available, so that at no point of that path $AGp$ holds; therefore $AFAGp$ is not satisfied by $S$. </p>

<p>As for your example, this is actually a case where two formulas <em>are</em> equivalent. This does happen. The proof is a little involved, but I can add it if you are interested.</p>

CC BY-SA 3.0
2014-04-01T19:31:39.623Z
Thanks for help, but how is then not possible to give fairness constraints in CTL with AG AF if GF is used in LTL to do the same?
darxsys
CC BY-SA 3.0
2014-04-02T13:41:28.917Z
You can do that, if all you want to do is express that every path satisfies the (unconditional) fairness condition. What you usually want to express, though, is that all fair paths (or some fair path) satisfy some other formula, i.e. something like $A(fair\Rightarrow\varphi)$. This is not allowed in CTL - you cannot have boolean combinations of path formulas. The lecture slides at http://www.react.uni-saarland.de/teaching/verification-11-12/downloads/l10.pdf have some more information that you may find helpful (including the fairness issue, on slides 17,18).
Klaus Draeger
CC BY-SA 3.0
2014-04-01T18:56:06.777Z
2014-04-01T18:56:06.777Z
Klaus Draeger
<p>I am trying to understand these subtle differences between LTL and CTL logic and one thing I simply don't have an idea how to understand.</p>

<p>Formula </p>

<pre><code>AG AF p 
</code></pre>

<p>in CTL and a formula</p>

<pre><code>GF p
</code></pre>

<p>in LTL. Why aren't they equivalent? Can you give me an example, please? I tried finding and drawing things, but I simply can't find a counter example and there is no explanation in the lecture materials I have.</p>

CC BY-SA 3.0
2016-06-17T04:26:57.137Z
@RichardRaimi, the answer by Klaus Draeger clearly states that AG AF p is equivalent to G F p.
Radu GRIGore
<linear-temporal-logic><temporal-logic>
CTL and LTL logic difference
darxsys
# CTL and LTL logic difference

(Asked by: username_0 on 2014-04-01)

I am trying to understand these subtle differences between LTL and CTL logic and one thing I simply don't have an idea how to understand.
Formula 
AG AF p 

in CTL and a formula
GF p

in LTL. Why aren't they equivalent? Can you give me an example, please? I tried finding and drawing things, but I simply can't find a counter example and there is no explanation in the lecture materials I have.

**Tags:** linear-temporal-logic, temporal-logic
> **Comments:**
> **username_1**: @RichardRaimi, the answer by Klaus Draeger clearly states that AG AF p is equivalent to G F p.  

---

## 1 answers

### Answer by username_2 on 2014-04-01. Score: 9 | Accepted answer

There are already some rather good related answers regarding LTL versus CTL. In a nutshell, LTL is first and foremost a logic of traces, and an LTL formula is true for a transition system $S$ if and only if it is true for each trace of $S$. CTL, on the other hand, is a branching-time logic, which can in a sense talk about multiple paths at the same time.

One standard example here (not the one you give, about which more below) is a labelled transition system $S=(Q,T,q\_0,L)$ with set of locations $Q=\{q\_0,q\_1,q\_2\}$, set of transitions $T=\{(q\_0,q\_0),(q\_0,q\_1),(q\_1,q\_2),(q\_2,q\_2)\}$, and labelling given by $L(q\_0)=L(q\_2)=\{p\}$, $L(q\_1)=\emptyset$. This system satisfies $FGp$, but not $AFAGp$, which can be seen as follows.

$FGp$ means that for every path $\pi=s\_1,s\_2,\dots$ in a given system, there is some point after which $p$ is always satisfied, i.e. there is some $i$ such that for all $j\geq i$, $p\in L(s\_i)$. This is satisfied by $S$ since every path in $S$ either remains in $q\_0$ forever (such that $p$ is always satisfied) or eventually gets to $p\_2$ (after which $p$ is always satisfied).

On the other hand, $AFAGp$ means that every path $\pi=s\_1,s\_2,\dots$ eventually reaches a state satisfying $AGp$, i.e. a state such that on *every path $\pi'$ starting there*, $p$ is always satisfied. Formally, this means that there is an $i$ such that for all $\pi'=s\_1',s\_2',\dots$ with $s\_1'=s\_i$ and all $j$, we have $p\in L(s\_j')$. But in $S$, for the path which always remains in $q\_0$, the transition to $q\_1$, where $p$ is not satisfied, is always available, so that at no point of that path $AGp$ holds; therefore $AFAGp$ is not satisfied by $S$.

As for your example, this is actually a case where two formulas *are* equivalent. This does happen. The proof is a little involved, but I can add it if you are interested.

> **Comments:**
> **username_0**: Thanks for help, but how is then not possible to give fairness constraints in CTL with AG AF if GF is used in LTL to do the same?  
> **username_2**: You can do that, if all you want to do is express that every path satisfies the (unconditional) fairness condition. What you usually want to express, though, is that all fair paths (or some fair path) satisfy some other formula, i.e. something like $A(fair\Rightarrow\varphi)$. This is not allowed in CTL - you cannot have boolean combinations of path formulas. The lecture slides at http://www.react.uni-saarland.de/teaching/verification-11-12/downloads/l10.pdf have some more information that you may find helpful (including the fairness issue, on slides 17,18).  

---

