Skip to main content
SpringerLink
Log in
Book cover

International Conference on Logic for Programming Artificial Intelligence and Reasoning

LPAR 2001: Logic for Programming, Artificial Intelligence, and Reasoning pp 39–54Cite as

Improving Automata Generation for Linear Temporal Logic by Considering the Automaton Hierarchy

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 2250))

Abstract

We present newalgorithms to translate linear time temporal logic (LTL) formulas with past operators to equivalent ω-automata. The resulting automata are given in a symbolic representation that directly supports symbolic model checking. Furthermore, this has the advantage that the translations run in linear time wrt. the length of the input formula. To increase the efficiency of the model checking, our translations avoid as far as possible the introduction of computationally expensive fairness constraints, or at least replace them by simpler reachability constraints. Using the well-known automaton hierarchy, we show that our improvements are complete. Finally, we show how large parts of the formulas can be translated to the simpler logic CTL, which accelerates the LTL model checking by orders of magnitude which is shown by experimental results.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. R. Bloem, H. Gabow, and F. Somenzi. An algorithm for strongly connected component analysis in n log(n) symbolic steps. In International Conference on Formal Methods in Computer Aided Design (FMCAD), LNCS 1954, pp. 37–54. Springer Verlag, 2000.

    Chapter  Google Scholar 

  2. R. Bloem, K. Ravi, and F. Somenzi. Efficient decision procedures for model checking of linear time logic properties. In Conference on Computer Aided Verification (CAV), LNCS 1633, Trento, Italy, 1999. Springer-Verlag.

    Chapter  Google Scholar 

  3. J. Burch, E. Clarke, K. McMillan, D. Dill, and L. Hwang. Symbolic Model Checking: 1020 States and Beyond. Information and Computing, 98(2):142–170, June 1992.

    Article  MATH  MathSciNet  Google Scholar 

  4. A. Cimatti, E. Clarke, F. Giunchiglia, and M. Roveri. NuSMV:Anewsymbolic model verifier. In Conference on Computer AidedVerification (CAV), 3 1633, pp. 495–499, Trento, Italy, 1999. Springer-Verlag.

    Google Scholar 

  5. E. Clarke and E. Emerson. Design and Synthesis of Synchronization Skeletons using Branching Time Temporal Logic. In Workshop on Logics of Programs, LNCS 131, pp. 52–71, Yorktown Heights, NewYork, May 1981. Springer-Verlag.

    Chapter  Google Scholar 

  6. E. Clarke, O. Grumberg, and K. Hamaguchi. Another look at LTL model checking. In Conference on Computer Aided Verification (CAV), LNCS 818, pp. 415–427, lStandford, California, USA, June 1994. Springer-Verlag.

    Google Scholar 

  7. R. Cleaveland and B. Steffen. A linear-time model checking algorithm for the alternation-free μ-calculus. Formal Methods in System Design, 2(2):121–147, April 1993.

    Article  MATH  Google Scholar 

  8. J.-M. Couvreur. On-the-fly verification of linear temporal logic. In FM’99-Formal Methods, LNCS 1708, pp. 233–252, Toulouse, France, 1999. Springer Verlag.

    Chapter  Google Scholar 

  9. M. Daniele, F. Giunchiglia, and M. Vardi. Improved automata generation for linear temporal logic. In Conference on Computer Aided Verification (CAV), LNCS 1633, Trento, Italy, 1999. Springer-Verlag.

    Chapter  Google Scholar 

  10. E. Emerson. Temporal and Modal Logic. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pp. 996–1072, Amsterdam, 1990. Elsevier Science Publishers.

    Google Scholar 

  11. E. Emerson and J. Halpern. “sometimes” and “not never” revisited: On branching versus linear time temporal logic. Journal of the ACM, 33(1):151–178, January 1986.

    Article  MATH  MathSciNet  Google Scholar 

  12. E. Emerson and C.-L. Lei. Modalities for model checking: Branching time strikes back. In ACM Symposium on Principles of Programming Languages, pp. 84–96, NewYork, 1985.

    Google Scholar 

  13. K. Etessami and G. Holzmann. Optimizing Büchi automata. In International Conference on Concurrency Theory, LNCS 1877, pp. 153–168. Springer Verlag, 2000.

    Google Scholar 

  14. P. Gastin and D. Oddoux. Fast LTL to Büchi automata translation. In Conference on Computer Aided Verification (CAV), LNCS 2102, pp. 53–65, Paris, France, 2001. Springer Verlag.

    Google Scholar 

  15. 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 (PSTV), Warsaw, June 1995. North-Holland.

    Google Scholar 

  16. M. Gordon and T. Melham. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993.

    Google Scholar 

  17. S. Johnson, P. Miner, and A. Camilleri. Studies of the single pulser in various reasoning systems. In International Conference on Theorem Provers in Circuit Design (TPCD), LNCS 901, pp. 126–145, Bad Herrenalb, Germany, September 1994. Springer-Verlag.

    Google Scholar 

  18. Y. Kesten, A. Pnueli, and L. Raviv. Algorithmic verification of linear temporal logic specifications. In Automata, Languages and Programming (ICALP), LNCS 1443, Aalborg, Denmark, 1998. Springer Verlag.

    Chapter  Google Scholar 

  19. O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In ACM Symposium on Principles of Programming Languages (POPL), pp. 97–107, NewYork, January 1985. ACM.

    Google Scholar 

  20. Z. Manna and A. Pnueli. Ahierarchy of temporal properties. In ACM Symposium on Principles of Distributed Computing, pp. 377–408, 1990.

    Google Scholar 

  21. K. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, Norwell Massachusetts, 1993.

    Google Scholar 

  22. K. McMillan. Cadence SMV, http://www-cad.eecs.berkeley.edu/~kenmcmil, 2000.

  23. M.Y. Vardi and P. Wolper. Reasoning about infinite computations. Information and Computation, 115(1):1–37, 1994.

    Article  MATH  MathSciNet  Google Scholar 

  24. A. Pnueli. The temporal logic of programs. In Symposium on Foundations of Computer Science, volume 18, pp. 46–57, NewYork, 1977. IEEE.

    Google Scholar 

  25. K. Ravi, R. Bloem, and F. Somenzi. A comparative study of symbolic algorithms for the computation of fair cycles. In International Conference on Formal Methods in Computer Aided Design (FMCAD), LNCS 1954. Springer Verlag, 2000.

    Chapter  Google Scholar 

  26. K. Schneider. CTL and equivalent sublanguages of CTL*. In IFIP Conference on Computer Hardware Description Languages and their Applications (CHDL), pp. 40–59, Toledo, Spain, April 1997. IFIP, Chapman and Hall.

    Google Scholar 

  27. K. Schneider. Model checking on product structures. In Formal Methods in Computer-Aided Design, LNCS 1522, pp. 483–500, Palo Alto, USA, November 1998. Springer Verlag.

    Chapter  Google Scholar 

  28. K. Schneider. Exploiting Hierarchies in Temporal Logics, Finite Automata, Arithmetics, and μ-Calculus for Efficiently Verifying Reactive Systems. Habilitation Thesis. University of Karlsruhe, 2001.

    Google Scholar 

  29. 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 1690, pp. 255–272, Nice, France, September 1999. Springer Verlag.

    Chapter  Google Scholar 

  30. K. Schneider and V. Sabelfeld. Introducing mutual exclusion in Esterel. In Andrei Ershov Third International Conference Perspectives of Systems Informatics, LNCS 1755, pp. 445–459, Akademgorodok, Novosibirsk, Russia, July 1999. Springer Verlag.

    Google Scholar 

  31. F. Somenzi and R. Bloem. Efficient Büchi automata from LTL formulae. In Conference on Computer Aided Verification, LNCS 1633, pp. 247–263, Trento, Italy, 2000. Springer-Verlag.

    Google Scholar 

  32. W. Thomas. Automata on infinite objects. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, vol. B, pp. 133–191, Amsterdam, 1990. Elsevier Science Publishers.

    Google Scholar 

  33. M. Vardi. Branching vs. linear time: Final showdown. In Tools and Algorithms for the Construction and Analysis of Systems, LNCS 2031, pp. 1–22, Genova, Italy, 2001. Springer Verlag.

    Chapter  Google Scholar 

  34. M. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In IEEE Symposium on Logic in Computer Science, pp. 332–344. IEEE Computer Society Press, June 1986.

    Google Scholar 

  35. W. Visser, H. Barringer, D. Fellows, G. Gough, and A. Williams. Efficient CTL* model hecking for analysis of rainbow designs. In Conference on Correct Hardware Design and Verification Methods, Montreal, Canada, October 1997. IFIP WG 10.5, Chapman and Hall.

    Google Scholar 

  36. K. Wagner. On ω-regular sets. Information and control, 43:123–177, 1979.

    Google Scholar 

  37. P. Wolper. Temporal logic can be more expressive. Information and Control, 56:72–99, 1983.

    Article  MATH  MathSciNet  Google Scholar 

  38. P. Wolper. Constructing automata from temporal logic formulas: A tutorial. In Summer School on Formal Methods in Performance Analysis, LNCS 2090, pp. 261–277. Springer Verlag, 2001.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science Institute for Computer Design and Fault Tolerance, University of Karlsruhe, P.O. Box 6980, 76128, Karlsruhe, Germany

    K. Schneider

Authors
  1. K. Schneider
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Software, Technical University of Catalonia, Jordi Girona 1, 08034, Barcelona, Spain

    Robert Nieuwenhuis

  2. Department of Computer Science, University of Manchester, Kilburn Building, Oxford Road, M13 9PL, Manchester, UK

    Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Schneider, K. (2001). Improving Automata Generation for Linear Temporal Logic by Considering the Automaton Hierarchy. In: Nieuwenhuis, R., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2001. Lecture Notes in Computer Science(), vol 2250. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45653-8_3

Download citation

  • DOI: https://doi.org/10.1007/3-540-45653-8_3

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-42957-9

  • Online ISBN: 978-3-540-45653-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation