Validity of CTL formula $s_0 \models EG\ AF\ p$ in given model - Computer Science Stack Exchange most recent 30 from cs.stackexchange.com 2019-09-18T03:19:47Z https://cs.stackexchange.com/feeds/question/102001 https://creativecommons.org/licenses/by-sa/4.0/rdf https://cs.stackexchange.com/q/102001 1 Validity of CTL formula $s_0 \models EG\ AF\ p$ in given model Bowen Peng https://cs.stackexchange.com/users/98062 2018-12-24T15:16:46Z 2018-12-25T17:17:06Z <p>I have been learning <strong>Verification by model checking</strong> recently and I get the following question:</p> <blockquote> <p>Is the CTL formula <span class="math-container">$s_{0} \models EG\ AF\ p$</span> valid in the following model?</p> <p><a href="https://i.stack.imgur.com/H8RUT.png" rel="nofollow noreferrer"><img src="https://i.stack.imgur.com/H8RUT.png" alt="Model"></a></p> </blockquote> <p>I think it is incorrect because there is a deadlock or infinite loop about <span class="math-container">$s_0$</span> after the state is starting from <span class="math-container">$s_0$</span>, which make it invalid under <span class="math-container">$EG\ AF\$</span> condition. </p> <p>Am I correct? How can I prove it (or give a counterexample)?</p> https://cs.stackexchange.com/questions/102001/validity-of-ctl-formula-s-0-models-eg-af-p-in-given-model/102014#102014 1 Answer by alias for Validity of CTL formula $s_0 \models EG\ AF\ p$ in given model alias https://cs.stackexchange.com/users/76804 2018-12-24T23:51:32Z 2018-12-25T17:17:06Z <p>You're correct. Another way to see would be to consider the de-morgan equivalent: <span class="math-container">$\neg (AF~EG~\neg p)$</span>. To show this invalid, we can show its negation <span class="math-container">$AF~EG~\neg p$</span> is valid, which is easier: The formula <span class="math-container">$AF~EG~\neg p$</span> says on all paths starting at <span class="math-container">$s_0$</span>, we eventually get to a state such that there is a path where <span class="math-container">$\neg p$</span> holds forever. And indeed that is true in the path <span class="math-container">$s_0 \rightarrow s_0 \rightarrow\ldots~.$</span> Since we established the negation, your original formula is invalid as you yourself concluded.</p> <p>Thinking about CTL can be tricky. A good way is to always double-check using a CTL model checker, like the following:</p> <pre><code>MODULE main() VAR state: {s0, s1, s2, s3}; ASSIGN init(state) := s0; next(state) := case state = s0: {s0, s1, s3}; state = s1: s2; state = s2: s1; state = s3: s2; esac; DEFINE p := (state = s1) | (state = s3); r := (state = s0) | (state = s1) | (state = s2); q := (state = s2) | (state = s3); t := (state = s1); SPEC EG AF p; </code></pre> <p>Using nuSMV (<a href="http://nusmv.fbk.eu/" rel="nofollow noreferrer">http://nusmv.fbk.eu/</a>), I get:</p> <pre><code>-- specification EG (AF p) is false -- as demonstrated by the following execution sequence Trace Description: CTL Counterexample Trace Type: Counterexample -&gt; State: 1.1 &lt;- state = s0 t = FALSE q = FALSE r = TRUE p = FALSE </code></pre> <p>Which is NuSMV's way of saying you can simply stay in the starting state and it would be a counter-example to your property.</p>