Technischer Bericht TR-2004-06

Schwoon, Stefan; Esparza, Javier: A Note on On-The-Fly Verification Algorithms.
Universität Stuttgart, Fakultät Informatik, Elektrotechnik und Informationstechnik, Technischer Bericht Informatik Nr. 2004/06.
18 Seiten, englisch.
CR-Klassif.D.2.4 (Software Engineering Software/Program Verification)
F.3.1 (Specifying and Verifying and Reasoning about Programs)
G.2.2 (Discrete Mathematics Graph Theory)
KeywordsLTL; model checking; depth-first search

The automata-theoretic approach to verification of LTL relies on an algorithm for finding accepting cycles in the product of the system and a Büchi automaton for the negation of the formula. Explicit-state model checkers typically construct the product space "on the fly" and explore the states using depth-first search. We survey algorithms proposed for this purpose and propose two improved algorithms, one based on nested DFS, the other on strongly connected components. We compare these algorithms both theoretically and experimentally and determine cases where both algorithms can be useful.

Volltext und
andere Links
PDF (183777 Bytes)
PostScript (254132 Bytes)
Publications of the SZS group
Abteilung(en)Universität Stuttgart, Institut für Formale Methoden der Informatik, Sichere und Zuverlässige Softwaresysteme
Eingabedatum9. November 2004
   Publ. Informatik