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:
$\begingroup$
$\endgroup$
4
asked Jan 27, 2016 at 12:12
-
$\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$– ShaullCommented Jan 27, 2016 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 VerschaffeltCommented Jan 27, 2016 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 RicherbyCommented Jan 28, 2016 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 VerschaffeltCommented Jan 28, 2016 at 7:27
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
6
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.
-
$\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$ Commented Jan 27, 2016 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$– ShaullCommented Jan 27, 2016 at 13:33
-
$\begingroup$ Thank you! I will practice more then :) Thank you for your help! $\endgroup$ Commented Jan 27, 2016 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$ Commented Jan 27, 2016 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$– ShaullCommented Jan 27, 2016 at 16:10