Skip to main content
SpringerLink
Log in

Larger Automata and Less Work for LTL Model Checking

  • Conference paper
Model Checking Software (SPIN 2006)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 3925))

Included in the following conference series:

Abstract

Many different automata and algorithms have been investigated in the context of automata-theoretic LTL model checking. This article compares the behaviour of two variations on the widely used Büchi automaton, namely (i) a Büchi automaton where states are labelled with atomic propositions and transitions are unlabelled, and (ii) a form of testing automaton that can only observe changes in state propositions and makes use of special livelock acceptance states. We describe how these variations can be generated from standard Büchi automata, and outline an SCC-based algorithm for verification with testing automata.

The variations are compared to standard automata in experiments with both random and human-generated Kripke structures and LTL_ X formulas, using SCC-based algorithms as well as a recent, improved version of the classic nested search algorithm. The results show that SCC-based algorithms outperform their nested search counterpart, but that the biggest improvements come from using the variant automata.

Much work has been done on the generation of small automata, but small automata do not necessarily lead to small products when combined with the system being verified. We investigate the underlying factors for the superior performance of the new variations.

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

Access this chapter

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 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Aho, A.V., Hopcroft, J.E., Ullman, J.D.: The Design and Analysis of Computer Algorithms. Addison-Wesley, Reading (1974)

    MATH  Google Scholar 

  2. Brim, L., Černá, I., Nečesal, M.: Randomization helps in LTL model checking. In: de Luca, L., Gilmore, S. (eds.) PROBMIV 2001, PAPM-PROBMIV 2001, and PAPM 2001. LNCS, vol. 2165, pp. 105–119. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  3. Büchi, J.R.: Weak second-order arithmetic and finite automata. Zeitschrift für mathematische Logik und Grundlagen der Math. 6, 66–92 (1960)

    Article  MathSciNet  MATH  Google Scholar 

  4. Büchi, J.R.: On a decision method in restricted second-order arithmetic. In: Proc. 1960 Intl. Congr. Logic, Method and Philosophy of Science, pp. 1–11. Stanford Univ. Press (June 1962)

    Google Scholar 

  5. Choueka, Y.: Theories of automata on ω-tapes: a simplified approach. Journal Computer and System Sciences 8, 117–141 (1974)

    Article  MathSciNet  MATH  Google Scholar 

  6. Courcoubetis, C., Vardi, M.Y., Wolper, P., Yannakakis, M.: Memory-efficient algorithms for the verification of temporal properties. In: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 233–242. Springer, Heidelberg (1991); Journal version: Formal Methods in System Design 1(2/3), 275–288 (1992)

    Chapter  Google Scholar 

  7. Couvreur, J.-M.: On-the-fly verification of linear temporal logic. In: Wing, J.M., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 253–271. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  8. Couvreur, J.-M.: On-the-fly emptiness checks for generalized Büchi automata. In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol. 3639, pp. 169–184. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  9. 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)

    Chapter  Google Scholar 

  10. Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Property specification patterns for finite-state verification. In: Proc. 2nd ACM Worksh. Formal Methods in Software Practice, pp. 7–15 (March 1998)

    Google Scholar 

  11. Edelkamp, S., Leue, S., Lluch Lafuente, A.: Directed explicit-state model checking in the validation of communication protocols. Technical Report 161, Institut für Informatik, Albert-Ludwigs-Universität Freiburg (October 2001)

    Google Scholar 

  12. Etessami, K.: A hierarchy of polynomial-time computable simulations for automata. In: Brim, L., Jančar, P., Křetínský, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 131–144. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  13. Etessami, K., Holzmann, G.J.: Optimizing Büchi automata. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 154–167. Springer, Heidelberg (2000)

    Google Scholar 

  14. 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)

    Chapter  Google Scholar 

  15. Gastin, P., Moro, P., Zeitoun, M.: Minimization of counterexamples in spin. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 92–108. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  16. 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)

    Chapter  Google Scholar 

  17. Geldenhuys, J., Valmari, A.: Tarjan’s algorithm makes on-the-fly LTL verification more efficient. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 205–219. Springer, Heidelberg (2004); Journal version: Theor. Computer Science 345(1), 60-82 (2005)

    Chapter  Google Scholar 

  18. Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Proc. 15th IFIP Symp. Protocol Spec., Testing, and Verif., June 1995, pp. 3–18 (1995)

    Google Scholar 

  19. Godefroid, P., Holzmann, G.J.: On the verification of temporal properties. In: Proc. 13th IFIP Symp. Protocol Spec., Testing, and Verif., May 1993, pp. 109–124 (1993)

    Google Scholar 

  20. Gurumurthy, S., Bloem, R., Somenzi, F.: Fair simulation minimization. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 610–624. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  21. Hansen, H., Penczek, W., Valmari, A.: Stuttering-insensitive automata for on-the-fly detection of livelock properties. In: Proc. 7th Intl. ERCIM Worksh. Formal Methods for Industrial Critical Systems, July 2002, pp. 185–200 (2002); Also published in Elec. Notes in Theor. Computer Science 66(2) (December 2002)

    Google Scholar 

  22. Holzmann, G.J., Peled, D., Yannakakis, M.: On nested depth first search. In: Proc. 2nd spin Worksh., August 1996. DIMACS Series, vol. 32, pp. 23–32 (1997)

    Google Scholar 

  23. Kamp, J.A.W.: Tense Logic and the Theory of Linear Order. PhD thesis, Univ. of California (1968)

    Google Scholar 

  24. Kripke, S.A.: Semantical analysis of modal logic I, normal propositional calculi. Zeitschrift für mathematische Logik und Grundlagen der Math 9, 67–96 (1963)

    Article  MathSciNet  MATH  Google Scholar 

  25. Kurshan, R.P.: Computer-aided Verification of Coordinating Processes: The Automata-theoretic Approach. Princeton University Press, Princeton (1994)

    MATH  Google Scholar 

  26. Rabin, M.O.: Decidability of second-order theories and automata on infinite trees. Trans. of the American Mathemathical Society 141, 1–35 (1969)

    MathSciNet  MATH  Google Scholar 

  27. Schwoon, S., Esparza, J.: A note on on-the-fly verification algorithms. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 174–190. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  28. Sebastiani, R., Tonetta, S.: More deterministic vs. Smaller büchi automata for efficient LTL model checking. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 126–140. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  29. Somenzi, F., Bloem, R.: Efficient Büchi automata from LTL formulae. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 248–267. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  30. Tarjan, R.E.: Depth-first search and linear graph algorithms. SIAM Journal of Computing 1(2), 146–160 (1972)

    Article  MathSciNet  MATH  Google Scholar 

  31. Tauriainen, H.: A randomized testbench for algorithms translating linear temporal logic formulae. In: Proc. Worksh. Concurrency, Specifications, and Programming, September 1999, pp. 251–262 (1999)

    Google Scholar 

  32. Tauriainen, H.: Nested emptiness search for generalized Büchi automata. Technical Report HUT–TCS–A79, Laboratory for Theoretical Computer Science, Helsinki Univ. of Technology (July 2003)

    Google Scholar 

  33. Valmari, A.: On-the-fly verification with stubborn sets. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 397–408. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  34. Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proc. 1st IEEE Symp. on Logic in Computer Science, June 1986, pp. 332–344 (1986)

    Google Scholar 

  35. Wolper, P.: Temporal logic can be more expressive. Information and Computation 56, 72–99 (1983)

    MathSciNet  MATH  Google Scholar 

  36. Wolper, P., Vardi, M.Y., Sistla, A.P.: Reasoning about infinite computation paths. In: Proc. 24th IEEE Symp. on the Foundations of Computer Science, November 1983, pp. 185–194. IEEE Computer Society Press, Los Alamitos (1983)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Stellenbosch University, Private Bag X1, 7602, Matieland, South Africa

    Jaco Geldenhuys

  2. Institute of Software Systems, Tampere University of Technology, PO Box 553, FI-33101, Tampere, Finland

    Henri Hansen

Authors
  1. Jaco Geldenhuys
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Henri Hansen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institute of Software Systems, Tampere University of Technology, PO Box 553, FI-33101, Tampere, Finland

    Antti Valmari

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Geldenhuys, J., Hansen, H. (2006). Larger Automata and Less Work for LTL Model Checking. In: Valmari, A. (eds) Model Checking Software. SPIN 2006. Lecture Notes in Computer Science, vol 3925. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11691617_4

Download citation

  • DOI: https://doi.org/10.1007/11691617_4

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-33102-5

  • Online ISBN: 978-3-540-33103-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation