Vardi, Moshe Y[Rice University > Department of Computer Science > > >]
Wolper, Pierre[Université de Liège - ULg > Dép. d'électric., électron. et informat. (Inst.Montefiore) > Informatique (parallélisme et banques de données) >]
Proceedings of the Fifteenth IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification
International Symposium on Protocol Specification, Testing and Verification
[en] Model Checking ; linear temporal logic ; Büchi automata ; automatic verification
[en] We present a tableau-based algorithm for obtaining an automaton from a temporal logic formula. The algorithm is geared towards being used in model checking in an “on-the-fly” fashion, that is the automaton can be constructed simultaneously with, and guided by, the generation of the model. In particular, it is possible to detect that a property does not hold by only constructing part of the model and of the automaton. The algorithm can also be used to check the validity of a temporal logic assertion. Although the general problem is PSPACE-complete, experiments show that our algorithm performs quite well on the temporal formulas typically encountered in verification. While basing linear-time temporal logic model-checking upon a transformation to
automata is not new, the details of how to do this efficiently, and in “on-the-fly” fashion have never been given.