Question

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?

No correct solution

Licensed under: CC-BY-SA with attribution
Not affiliated with cs.stackexchange
scroll top