CTL and LTL logic difference

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.

• 'darxsys' asked about AGAFp vs GFp, and Klaus responded about a different pair of formulae, AFAGp vs FGp. I'd appreciate someone answering the original question, about AGAFp vs GFp, because it's on my mind today, too.
– user40446
Jun 16 '16 at 14:40
• @RichardRaimi, the answer by Klaus Draeger clearly states that AG AF p is equivalent to G F p. Jun 17 '16 at 4:26

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$.
• 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 react.uni-saarland.de/teaching/verification-11-12/downloads/… have some more information that you may find helpful (including the fairness issue, on slides 17,18). Apr 2 '14 at 13:41