0
$\begingroup$

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:

enter image description here

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Shaull Jan 27 '16 at 12:48
  • $\begingroup$ 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? $\endgroup$ – Pieter Verschaffelt Jan 27 '16 at 12:50
  • $\begingroup$ Your question already includes a complete answer to the original problem but no question about this answer. Thus, only "yes/no" answers may remain, helping neither you nor future visitors. Please read related meta discussions here and here and adjust your question accordingly, for example by formulating a specific question about a single element of your answer you are uncertain about. Can you figure out what it is that you don't understand that's stopping you from determining whether your answer is correct? $\endgroup$ – David Richerby Jan 28 '16 at 1:06
  • $\begingroup$ 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? $\endgroup$ – Pieter Verschaffelt Jan 28 '16 at 7:27
1
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Thank you very much! :) I see now. Is there some trick that helps you find such differences between LTL and CTL or is it just plane reasoning? $\endgroup$ – Pieter Verschaffelt Jan 27 '16 at 12:58
  • $\begingroup$ 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. $\endgroup$ – Shaull Jan 27 '16 at 13:33
  • $\begingroup$ Thank you! I will practice more then :) Thank you for your help! $\endgroup$ – Pieter Verschaffelt Jan 27 '16 at 13:50
  • $\begingroup$ 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? $\endgroup$ – Pieter Verschaffelt Jan 27 '16 at 14:08
  • $\begingroup$ 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$. $\endgroup$ – Shaull Jan 27 '16 at 16:10

Not the answer you're looking for? Browse other questions tagged or ask your own question.