I'm trying to verify if the following model satisfy $A [a \cup b]$: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):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?
CTL - model checking for formula $A [a \cup b]$
logic;computation tree logic;temporal logic
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).