Abstract
We improve the state-of-the-art algorithm for obtaining an automaton from a linear temporal logic formula. The automaton is intended to be used for model checking, as well as for satisfiability checking. Therefore, the algorithm is mainly concerned with keeping the automaton as small as possible. The experimental results show that our algorithm outperforms the previous one, with respect to both the size of the generated automata and computation time. The testing is performed following a newly developed methodology based on the use of randomly generated formulas.
Chapter PDF
Similar content being viewed by others
Keywords
- Decision Procedure
- Linear Temporal Logic
- Acceptance Condition
- Linear Time Temporal Logic
- Linear Temporal Logic Formula
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
C. Courcoubetis, M. Vardi, P. Wolper, and M. Yannakakis. Memory efficient algorithms for the verification of temporal properties. In E. M. Clarke and R. P. Kurshan, editors, Proceedings of Computer-Aided Verification (CAV’ 90), volume 531 of LNCS, pages 233–242, Berlin, Germany, June 1991. Springer.
M. Daniele, F. Giunchiglia, and M. Y. Vardi. Improved automata generation for linear time temporal logic. Technical Report 9903-10, ITC-IRST, March 1999.
R. Gerth, D. Peled, M. Vardi, and P. Wolper. Simple on-the-fly automatic verification of linear temporal logic. In Protocol Specification Testing and Verification, pages 3–18, Warsaw, Poland, 1995. Chapman & Hall.
F. Giunchiglia and R. Sebastiani. Building decision procedures for modal logics from propositional decision procedures: the case study of modal K. In M. A. McRobbie and J. K. Slaney, editors, Proceedings of the Thirteenth International Conference on Automated Deduction (CADE-96), volume 1104 of LNAI, pages 583–597, Berlin, July30 August-3 1996. Springer.
G. J. Holzmann. The model checker spin. IEEE Trans. on Software Engineering, 23(5):279–295, May 1997. Special issue on Formal Methods in Software Practice.
Y. Kesten, Z. Manna, H. McGuire, and A. Pnueli. A decision algorithm for full propositional temporal logic. In C. Courcoubertis, editor, Proceedings of Computer-Aided Verification (CAV’93), volume 697 of LNCS, pages 97–109, Elounda, Greece, June 1993. Springer.
D. Mitchell, B. Selman, and H. Levesque. Hard and easy distributions of SAT problems. In W. Swartout, editor, Proceedings of the 10th National Conference on Artificial Intelligence, pages 459–465, San Jose, CA, July 1992. MIT Press.
S. Schwendimann. A new one-pass tableau calculus for PLTL. Lecture Notes in Computer Science, 1397:277–291, 1998.
W. Thomas. Automata on infinite objects. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, chapter 4, pages 133–191. Elsevier Science Publishers B. V., 1990.
M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In lics86, pages 332–344, 1986.
M. Y. Vardi and P. Wolper. Reasoning about infinite computations. Information and Computation, 115(1):1–37, 15 November 1994.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Daniele, M., Giunchiglia, F., Vardi, M.Y. (1999). Improved Automata Generation for Linear Temporal Logic. In: Halbwachs, N., Peled, D. (eds) Computer Aided Verification. CAV 1999. Lecture Notes in Computer Science, vol 1633. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48683-6_23
Download citation
DOI: https://doi.org/10.1007/3-540-48683-6_23
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66202-0
Online ISBN: 978-3-540-48683-1
eBook Packages: Springer Book Archive