HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

Truly On-The-Fly LTL Model Checking

Moritz Hammer 1 Alexander Knapp 1 Stephan Merz 2
2 MOSEL - Proof-oriented development of computer-based systems
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We propose a novel algorithm for automata-based LTL model checking that interleaves the construction of the generalized Büchi automaton for the negation of the formula and the emptiness check. Our algorithm first converts the LTL formula into a linear weak alternating automaton; configurations of the alternating automaton correspond to the locations of a generalized Büchi automaton, and a variant of Tarjan's algorithm is used to decide the existence of an accepting run of the product of the transition system and the automaton. Because we avoid an explicit construction of the Büchi automaton, our approach can yield significant improvements in runtime and memory, for large LTL formulas. The algorithm has been implemented within the SPIN model checker, and we present experimental results for some benchmark examples.
Document type :
Conference papers
Complete list of metadata

Cited literature [23 references]  Display  Hide  Download

Contributor : Stephan Merz Connect in order to contact the contributor
Submitted on : Wednesday, November 16, 2005 - 12:25:31 PM
Last modification on : Friday, February 4, 2022 - 3:21:56 AM
Long-term archiving on: : Friday, April 2, 2010 - 7:27:51 PM





Moritz Hammer, Alexander Knapp, Stephan Merz. Truly On-The-Fly LTL Model Checking. Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2005), Apr 2005, Edinburgh / U.K., pp.191-205. ⟨inria-00000753⟩



Record views


Files downloads