# Counterexample for LTL - CTL equivalence [closed]

I have to find an example of a model where the LTL-formula $F G p \wedge F q$ is valid and the CTL-formula $EF AG p \wedge AF q$ is not valid. I found this example, but I'm not completely sure whether it's correct:

• Your example is incorrect, since the LTL formula doesn't hold: in the computation $s_0,s_1,s_2,s_3^\omega$ the formula $FGp$ doesn't hold. Jan 27, 2016 at 12:48
• Hmm yes, you're right. Do you know an example in which it does hold and the CTL-formula doesn't? Or would it be easier to find an example in which the CTL-formula does hold and the LTL-formula doesn't hold? Jan 27, 2016 at 12:50
• The actual problem is the fact that I don't really understand the difference between the A (all paths) in CTL and a normal LTL-formula which also holds for all paths? Jan 28, 2016 at 7:27

Consider the following model: you have 3 states, $s_0,s_1,s_2$ with the transitions: $s_0\to s_0$, $s_0\to s_1$, $s_1\to s_2$ and $s_2\to s_2$ and the labels are $L(s_0)=\{p,q\}$, $L(s_1)=\emptyset$ and $L(s_2)=p$.
Then, every computation starts with $q$, so $Fq$ holds, and every infinite computation eventually gets stuck in $s_2$, or it is $s_0^\omega$, and both satisfy $FGp$, so the LTL formula holds.
However, it never holds that $AFq$, so the CTL formula does not hold.
• As with most problems, there is no "trick", just reasoning and some experience. Conceptually, it is possible to find such an example algorithmically: let $\phi$ be an LTL formula and $\psi$ be a CTL formula, then you can construct the CTL* formula $A\phi\wedge \neg \psi$, and then use CTL* satisfiabilityto find a model for the formula. But the complexity of this algorithm is terrible - 2EXPTIME, so it's not suited for solving exercises. Jan 27, 2016 at 13:33
• I have one more little question: I don't quite understand why $AF q$ never holds? The computation starts with q, so at that point $AF q$ is satisfied? Or not? Jan 27, 2016 at 14:08
• Hmm. I read your CTL formula as $EF(AGp\wedge AFq)$, in which case my example is fine. But if it's intended as $(EFAGp)\wedge AFq$, then my answer is incorrect, and I think that there is no (non-empty) model that will have the desired property - obviously $AFq$ has to hold, by the LTL formula, and if $EFAGp$ doesn't hold, then along every path, every state has a path from it in which $AGp$ doesn't hold, which means we can construct a path that does not satisfy $FGp$. Jan 27, 2016 at 16:10