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$

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.

  • $\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.