Currently I'm trying to understand the CTL* model checking algorithm from this book. The basic idea is clear to that we can use the LTL algorithm to whenever we have a subformular $E\phi$ or $A\phi$ but I have still a question I can't figure out:


Why is there no case for $\phi_1 U \phi_2$ in this algorithm? Of course we can write the until modality as a release modality but this case isn't here either. So is this algorithm incomplete or have I missed something?


The algorithm is full and correct. If you look back to definition 6.80 in the same book, you will see that the until operator is part of path formulae, which in the CTL* MC algorithm are checked via a standard LTL model checker as written in the last switch case ($\exists \varphi$). The $\varphi$ stands for any path formula.

The algorithm also states that you take the negation of $\varphi$. So then you need to take the complement of the satisfaction set.


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.