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

## closed as unclear what you're asking by David Richerby, Evil, vonbrand, Luke Mathieson, Ran G.Feb 1 '16 at 21:12

Please clarify your specific problem or add additional details to highlight exactly what you need. As it's currently written, it’s hard to tell exactly what you're asking. See the How to Ask page for help clarifying this question. If this question can be reworded to fit the rules in the help center, please edit the question.

• 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. – Shaull Jan 27 '16 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? – Pieter Verschaffelt Jan 27 '16 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? – Pieter Verschaffelt Jan 28 '16 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. – Shaull Jan 27 '16 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? – Pieter Verschaffelt Jan 27 '16 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$. – Shaull Jan 27 '16 at 16:10