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?

$\endgroup$
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).

$\endgroup$
  • $\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 '15 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 '15 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 '15 at 23:01

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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