1
$\begingroup$

I'm trying to verify if the following model satisfy $A [a \cup b]$:

The model on which i want to verify the formula

The algorithm I'm using is taken from "Concepts, Algorithms, and Tools for Model Checking", Joost-Pieter Katoen. In particular I applied the SatAU part (previous calculation of the states in which a and b are valid):

SatAU algorithm

Intuitively the formula is verified in state $\{s_1, s_2, s_3, s_4\}$ (so the model does not satisfy the property because the set doesn't contain the other initial state $s_0$). But if I apply the algorithm above the only state that I get are $\{s_2, s_3, s_4\}$, because the condition to generate the new $Q$ set (row 7) says to take a state s only if it has a connection with EACH element of the old $Q$ set. Is it correct my interpretation of the algorithm? How can I get also $s_1$ from the algorithm?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
3
$\begingroup$

Your answer $Sat(A(a \cup b)) = \{ s_1, s_2, s_3, s_4 \}$ is correct. And your conclusion that the model does not satisfy the property is also correct because the initial state $s_0 \notin Sat(A(a \cup b))$.

In my opinion, there is a typo in Line 7: $$Q := Q \cup \left( \{ s \mid \forall s' \in Q. (s,s') \in R \} \cap Sat(\phi) \right).$$

According to the fixed point interpretation, $Sat(A(\phi \cup \psi))$ is the smallest set $T \subseteq S$ satisfying $$Sat(\psi) \cup \{ s \in Sat(\phi) | Post(s) \subseteq T \} \subseteq T.$$ Therefore, the iteration step for Line 7 should be: $$Q := Q \cup \left( \{ s \mid \forall (s,s') \in R. s' \in Q \} \cap Sat(\phi) \right),$$ or concisely, $$Q := Q \cup \{ s \in Sat(\phi) \mid \forall (s,s') \in R. s' \in Q \}.$$

By the way, this lecture note by Joost-Pieter Katoen is quite out-of-date (back to 1999). In 2007, along with Christel Baier, he has published a wonderful book on model checking "Principles of Model Checking (The MIT Press)". You should read it now (online version avaiable).

Improve this answer
$\endgroup$
3
  • $\begingroup$ Seconding the recommendation of the Baier-Katoen book. Note, however, that the CTL model checking algorithm in the book assumes a formula in existential normal form, which may take getting used to $\endgroup$
    – Klaus Draeger
    Jan 29, 2015 at 13:34
  • $\begingroup$ Thank you again @hengxin.I think you're right again because i was reading again the part on the algorithm and i see this:"The difference between SatEU and SatAU is that for the latter a new state is labelled if φ holds in that state and if all successor states are already labelled, i.e. are member of Q′. This corresponds to AX." This definition clarify what the author was trying to show with the algorithm (and this definition is similar to the one you wrote above). $\endgroup$
    – Fabrizio Duroni
    Jan 29, 2015 at 23:00
  • $\begingroup$ Thank you also to @KlausDraeger, I'm just giving a try to "principle of model checking", even if the notes of the course are all based on the first publication I mentioned before :) $\endgroup$
    – Fabrizio Duroni
    Jan 29, 2015 at 23:01

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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