Practical CTL^* model checking: Should SPIN be extended?

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, after which this resulting automaton is then checked for nonemptiness. We introduce the nonemptiness game that checks the nonemptiness of a hesitant alternating automaton (HAA). In the same way that alternating automata generalise nondeterministic automata, we show that this game for checking the nonemptiness of HAA, generalises the nested depth-first algorithm used to check the nonemptiness of nondeterministic Büchi automata (used in Spin).

Authors and Affiliations

1. RIACS, NASA Ames Research Center, Mountain View, CA, USA; E-mail: wvisser@ptolemy.arc.nasa.gov, , , , , , US

   Willem Visser

2. Department of Computer Science, University of Manchester, Manchester, UK; E-mail: howard@cs.man.ac.uk, , , , , , UK

   Howard Barringer

Reprints and permissions