Abstract
A subset of LTL is presented that can be translated to ω automata with only a linear number of states. The translation is completely based on closures under temporal and boolean operators. Moreover, it is shown how this enhancement can be combined with traditional translations so that all LTL formulas can be translated. Exponential savings are possible in terms of reachable states, as well as in terms of runtime and memory requirements for model checking.
This work has been financed by the DFG project ‘Verification of embedded systems' in the priority program ‘Design and design methodology of embedded systems'
Chapter PDF
Similar content being viewed by others
Keywords
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
K. Schneider and D. Hoffmann. A HOL conversion for translating linear time temporal logic to ω-automata. In Higher Order Logic Theorem Proving and its Applications, LNCS, Nice, France, September 1999. Springer Verlag.
E. M. Clarke, O. Grumberg, and K. Hamaguchi. Another look at LTL model checking. In Conference on Computer Aided Verification (CAV), LNCS 818, pp. 415–427, Standford, California, USA, June 1994. Springer-Verlag.
G.G de Jong. An automata theoretic approach to temporal logic. In Computer Aided Verification (CAV), LNCS 575, pp. 477–487, Aalborg, July 1991. Springer-Verlag.
W. Thomas. Automata on infinite objects. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 133–191, Amsterdam, 1990. Elsevier Science Publishers.
K. Schneider. CTL and equivalent sublanguages of CTL✻. In C. Delgado Kloos, editor, IFIP Conference on Computer Hardware Description Languages and their Applications (CHDL), pp. 40–59, Toledo, Spain, April 1997. IFIP, Chapman and Hall.
K. Schneider. Model checking on product structures. In Formal Methods in Computer-Aided Design, LNCS 1522, pp. 483–500, Palo Alto, CA, November 1998. Springer Verlag.
O. Kupferman and M. Y. Vardi. Freedom, weakness, and determinism: From lineartime to branching-time. In IEEE Symposium on Logic in Computer Science, 1998.
K. Wagner. On ✻ regular sets. Information and control, 43:123–177, 1979.
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
Schneider, K. (1999). Yet Another Look at LTL Model Checking. In: Pierre, L., Kropf, T. (eds) Correct Hardware Design and Verification Methods. CHARME 1999. Lecture Notes in Computer Science, vol 1703. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48153-2_25
Download citation
DOI: https://doi.org/10.1007/3-540-48153-2_25
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66559-5
Online ISBN: 978-3-540-48153-9
eBook Packages: Springer Book Archive