We propose a novel algorithm for automata-based LTL model checking that interleaves the construction of the generalized Büchi automaton for the negation of the formula and the emptiness check. Our algorithm first converts the LTL formula into a linear weak alternating automaton; configurations of the alternating automaton correspond to the locations of a generalized Büchi automaton, and a variant of Tarjan’s algorithm is used to decide the existence of an accepting run of the product of the transition system and the automaton. Because we avoid an explicit construction of the Büchi automaton, our approach can yield significant improvements in runtime and memory, for large LTL formulas. The algorithm has been implemented within the Spin model checker, and we present experimental results for some benchmark examples.


Model Check Linear Temporal Logic Acceptance Condition Disjunctive Normal Form Transition 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.


  1. 1.
    Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Computers C-35(8), 677–691 (1986)CrossRefGoogle Scholar
  2. 2.
    Courcoubetis, C., Vardi, M.Y., Wolper, P., Yannakakis, M.: Memory-efficient algorithms for the verification of temporal properties. Formal methods in system design 1, 275–288 (1992)CrossRefGoogle Scholar
  3. 3.
    Daniele, M., Giunchiglia, F., Vardi, M.Y.: Improved automata generation for linear temporal logic. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 249–260. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  4. 4.
    Etessami, K., Holzmann, G.: Optimizing Büchi automata. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 153–167. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  5. 5.
    Fritz, C.: Constructing Büchi automata from linear temporal logic using simulation relations for alternating Büchi automata. In: Ibarra, O.H., Dang, Z. (eds.) CIAA 2003. LNCS, vol. 2759, pp. 35–48. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  6. 6.
    Fritz, C., Wilke, T.: State space reductions for alternating Büchi automata: Quotienting by simulation equivalences. In: Agrawal, M., Seth, A.K. (eds.) FSTTCS 2002. LNCS, vol. 2556, pp. 157–168. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  7. 7.
    Gastin, P., Oddoux, D.: Fast LTL to Büchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 53–65. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  8. 8.
    Geldenhuys, J., Valmari, A.: Tarjan’s algorithm makes LTL verification more efficient. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 205–219. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  9. 9.
    Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Dembinski, P., Sredniawa, M. (eds.) Protocol Specification, Testing, and Verification, Warsaw, Poland, pp. 3–18. Chapman & Hall, Boca Raton (1995)Google Scholar
  10. 10.
    Holzmann, G.: The Spin model checker. IEEE Trans. on Software Engineering 23(5), 279–295 (1997)CrossRefMathSciNetGoogle Scholar
  11. 11.
    Holzmann, G.: An analysis of bitstate hashing. Formal Methods in System Design 13(3), 289–307 (1998)CrossRefMathSciNetGoogle Scholar
  12. 12.
    Holzmann, G.: The SPIN Model Checker. Addison-Wesley, Reading (2003)Google Scholar
  13. 13.
    Kesten, Y., Pnueli, A.: Verifying liveness by augmented abstraction. In: Flum, J., Rodríguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol. 1683, pp. 141–156. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  14. 14.
    Löding, C., Thomas, W.: Alternating automata and logics over infinite words. In: Watanabe, O., Hagiya, M., Ito, T., van Leeuwen, J., Mosses, P.D. (eds.) TCS 2000. LNCS, vol. 1872, pp. 521–535. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  15. 15.
    Muller, D.E., Saoudi, A., Schupp, P.E.: Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time. In: 3rd IEEE Symp. Logic in Computer Science (LICS 1988), pp. 422–427. IEEE Press, Los Alamitos (1988)Google Scholar
  16. 16.
    Rohde, S.: Alternating automata and the temporal logic of ordinals. PhD thesis, Dept. of Math., Univ. of Illinois, Urbana-Champaign, IL (1997)Google Scholar
  17. 17.
    Schneider, K.: Yet another look at LTL model checking. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 321–326. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  18. 18.
    Somenzi, F., Bloem, R.: Efficient Büchi automata from LTL formulae. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 257–263. Springer, Heidelberg (1999)Google Scholar
  19. 19.
    Tarjan, R.E.: Depth first search and linear graph algorithms. SIAM Journal of Computing 1, 146–160 (1972)zbMATHCrossRefMathSciNetGoogle Scholar
  20. 20.
    Tauriainen, H.: On translating linear temporal logic into alternating and nondeterministic automata. Research Report A83, Helsinki Univ. of Technology, Lab. Theor. Comp. Sci., Espoo, Finland (December 2003)Google Scholar
  21. 21.
    Tauriainen, H.: Nested emptiness search for generalized Büchi automata. In: Kishnevsky, M., Darondeau, P. (eds.) 4th Intl. Conf. Application of Concurrency to System Design (ACSD 2004), pp. 165–174. IEEE Computer Society, Los Alamitos (2004)CrossRefGoogle Scholar
  22. 22.
    Thomas, W.: Languages, automata, and logic. In: Rozenberg, G., Salomaa, A. (eds.) Handbook of Formal Language Theory, vol. III, pp. 389–455. Springer, Heidelberg (1997)Google Scholar
  23. 23.
    Vardi, M.Y.: Alternating automata and program verification. In: van Leeuwen, J. (ed.) Computer Science Today. LNCS, vol. 1000, pp. 471–485. Springer, Heidelberg (1995)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Moritz Hammer
    • 1
  • Alexander Knapp
    • 1
  • Stephan Merz
    • 2
  1. 1.Institut für InformatikLudwig-Maximilians-Universität München 
  2. 2.INRIA Lorraine, LORIANancy

Personalised recommendations