Slides of the MFCS presentation (pdf file, 156 K)
Technical report LIAFA 2003-10 (18 pages), Université PARIS 7 (196 K)
Extended abstract of this technical report in the Proceedings of MFCS'03, Lecture Notes in Computer Science 2747, p. 439-448, 2003.
Partial support of DFG program MERCATOR and of the GAMES project is gratefully acknowledged.
Abstract: It is crucial for a model checker using LTL as a specification language to have very efficient translation of LTL formulas to Büchi automata. Most such algorithms are based on a tableau construction. Recently, an implementation using very-weak alternating automata as an intermediary step proved to be dramatically faster than previous implementations based on the tableau construction. In this paper, we want to generalize this method to PLTL (LTL with past modalities). For this, we study two-way very-weak alternating automata (2VWAA). Our main result is an efficient translation of 2VWAA to generalized Büchi automata (GBA). Since we can easily transform a PLTL formula to an equivalent 2VWAA, this algorithm allows to use PLTL specifications with classical model checkers such as SPIN.
Keywords: Temporal logics, Model checking, automata
BibTeX entry:
@InProceedings(GaOd03mfcs,
Author = "Gastin, P. and Oddoux, D.",
Title = "{LTL} with past and two-way very-weak alternating automata",
BookTitle = "Proceedings of the 28th International Symposium on Mathematical
Foundations of Computer Science (MFCS'03)",
Editor = "Rovan, B.",
Publisher = SPRINGER,
Series = LNCS,
Number = 2747,
Year = 2003,
Pages = "439-448")
Last update: August 26, 2003