CTL* Model Checking for SPIN
Willem I. Visser, Howard Barringer · 1998
We describe an efficient CTL* model checking algorithm based on alternating automata and games. A CTL* formula, expressing a correctness property, is first translated to a hesitant alternating automaton and then composed with a Kripke structure representing the model to be checked, this resulting automaton is then checked for nonemptiness. We introduce the nonemptiness game that checks the nonemptiness of a hesitant alternating automata (HAA). In the same