Advertisement

Abstract

In automata-theoretic model checking we compose the design under verification with a Büchi automaton that accepts traces violating the specification. We then use graph algorithms to search for a counterexample trace. The basic theory of this approach was worked out in the 1980s, and the basic algorithms were developed during the 1990s. Both explicit and symbolic implementations, such as SPIN and and SMV, are widely used. It turns out, however, that there are still many gaps in our understanding of the algorithmic issues involved in automata-theoretic model checking. This paper covers the fundamentals of automata-theoretic model checking, review recent progress, and outlines areas that require further research.

Keywords

Model Check Temporal Logic Linear Temporal Logic Label Transition System Symbolic Model Check 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Albin, K., et al.: Property specification language reference manual. Technical Report Version 1.1, Accellera (2004)Google Scholar
  2. 2.
    Armoni, R., et al.: Efficient LTL compilation for SAT-based model checking. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, Springer, Heidelberg (2005)Google Scholar
  3. 3.
    Armoni, R., et al.: The ForSpec temporal logic: A new temporal property-specification logic. In: Katoen, J.-P., Stevens, P. (eds.) ETAPS 2002 and TACAS 2002. LNCS, vol. 2280, Springer, Heidelberg (2002)CrossRefGoogle Scholar
  4. 4.
    Armoni, R., Korchemny, D., Tiemeyer, A.: Deterministic dynamic monitors for linear-time assertions. In: Havelund, K., et al. (eds.) Formal Approaches to Software Testing and Runtime Verification. LNCS, vol. 4262, Springer, Heidelberg (2006)CrossRefGoogle Scholar
  5. 5.
    Balcázar, J.L., Lozano, A.: The complexity of graph problems for succinctly represented graphs. In: Nagl, M. (ed.) WG 1989. LNCS, vol. 411, pp. 277–285. Springer, Heidelberg (1990)Google Scholar
  6. 6.
    Barnat, J., Brim, L., Cerna, I.: Cluster-based LTL model checking of large systems. In: de Boer, F.S., et al. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 259–279. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  7. 7.
    Biere, A., Artho, C., Schuppan, V.: Liveness checking as safety checking. In: Proc. 7th Int’l Workshop on Formal Methods for Industrial Critical Systems, Electr. Notes Theor. Comput. Sci., vol. 66, no. 2 (2002)Google Scholar
  8. 8.
    Biere, A., et al.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) ETAPS 1999 and TACAS 1999. LNCS, vol. 1579, Springer, Heidelberg (1999)Google Scholar
  9. 9.
    Bloem, R., Gabow, H.N., Somenzi, F.: An algorithm for strongly connected component analysis in n logn symbolic steps. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol. 1954, Springer, Heidelberg (2000)Google Scholar
  10. 10.
    Bloem, R., Ravi, K., Somenzi, F.: Efficient decision procedures for model checking of linear time logic properties. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, Springer, Heidelberg (1999)CrossRefGoogle Scholar
  11. 11.
    Bryant, R.E.: Graph-based algorithms for boolean-function manipulation. IEEE Trans. on Computers C-35(8) (1986)Google Scholar
  12. 12.
    Büchi, J.R.: On a decision method in restricted second order arithmetic. In: Proc. International Congress on Logic, Method, and Philosophy of Science 196, pp. 1–12. Stanford University Press, Stanford (1962)Google Scholar
  13. 13.
    Burch, J.R., et al.: Symbolic model checking: 1020 states and beyond. Information and Computation 98(2), 142–170 (1992)zbMATHCrossRefMathSciNetGoogle Scholar
  14. 14.
    Bustan, D., Fisman, D.: John Havlicek.: Automata construction for psl. Technical report, The Weizmann Institute of Science, Technical Report MCS05-04 (May 2005)Google Scholar
  15. 15.
    Choueka, Y.: Theories of automata on ω-tapes: A simplified approach. Journal of Computer and System Sciences 8, 117–141 (1974)zbMATHMathSciNetGoogle Scholar
  16. 16.
    Cimatti, A., et al.: Nusmv 2: An opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, Springer, Heidelberg (2002)CrossRefGoogle Scholar
  17. 17.
    Cimatti, A., Roveri, M., Semprini, S., Tonetta, S.: From psl to nba: A modular symbolic encoding. In: Proc. 6th Int’l Conf. on Formal Methods in Computer-Aided design (2006)Google Scholar
  18. 18.
    Cimatti, A., Roveri, M., Sheridan, D.: Bounded verification of past ltl. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, Springer, Heidelberg (2004)Google Scholar
  19. 19.
    Clarke, E.M., Grumberg, O., Hamaguchi, K.: Another look at ltl model checking. Formal Methods in System Design 10(1), 47–71 (1997)CrossRefGoogle Scholar
  20. 20.
    Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems 8(2), 244–263 (1986)zbMATHCrossRefGoogle Scholar
  21. 21.
    Clarke, E.M., Grumberg, O., Hamaguchi, K.: Another look at LTL model checking. In: Computer Aided Verification, Proc. 6th International Conference, Stanford, California, USA, June 21-23, pp. 415–427. Springer, New York (1994)Google Scholar
  22. 22.
    Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
  23. 23.
    Clarke, E.M., Kurshan, R.P.: Computer aided verification. IEEE Spectrum 33, 61–67 (1986)CrossRefGoogle Scholar
  24. 24.
    Clarke, E.M., Wing, J.M.: Formal methods: State of the art and future directions. ACM Computing Surveys 28, 626–643 (1996)CrossRefGoogle Scholar
  25. 25.
    Copty, F., et al.: Benefits of bounded model checking at an industrial setting. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, Springer, Heidelberg (2001)Google Scholar
  26. 26.
    Cormen, T.H., Leiserson, C.E., Rivest, R.L.: Introduction to Algorithms. MIT Press and McGraw-Hill, Cambridge (1990)zbMATHGoogle Scholar
  27. 27.
    Courcoubetis, C., et al.: Memory efficient algorithms for the verification of temporal properties. Formal Methods in System Design 1, 275–288 (1992)CrossRefGoogle Scholar
  28. 28.
    Couvreur, J-M.: On-the-fly verification of linear temporal logic. In: Proc. World Congress on Formal Methods, pp. 253–271 (1999)Google Scholar
  29. 29.
    Couvreur, J.M., Duret-Lutz, A., Poitrenaud, D.: On-the-fly emptiness checks for generalized Büchi automata. In: Godefroid, P. (ed.) Model Checking Software. LNCS, vol. 3639, Springer, Heidelberg (2005)Google Scholar
  30. 30.
    Daniele, N., Guinchiglia, F., Vardi, M.Y.: Improved automata generation for linear temporal logic. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, Springer, Heidelberg (1999)CrossRefGoogle Scholar
  31. 31.
    Duret-Lutz, A., Poitrenaud, D.: Spot: An extensible model checking library using transition-based generalized büchi automata. In: Proc. 12th Int’l Workshop on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems, pp. 76–83. IEEE Computer Society Press, Los Alamitos (2004)Google Scholar
  32. 32.
    Emerson, E.A., Clarke, E.M.: Characterizing correctness properties of parallel programs using fixpoints. In: de Bakker, J.W., van Leeuwen, J. (eds.) Automata, Languages and Programming. LNCS, vol. 85, pp. 169–181. Springer, Heidelberg (1980)Google Scholar
  33. 33.
    Emerson, E.A., Lei, C.-L.: Efficient model checking in fragments of the propositional μ-calculus. In: Proc. 1st Symp. on Logic in Computer Science, pp. 267–278, Cambridge (June 1986)Google Scholar
  34. 34.
    Etessami, K., Holzmann, G.J.: Optimizing Büchi automata. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 153–167. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  35. 35.
    Fisler, K., et al.: Is there a best symbolic cycle-detection algorithm? In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol. 2031, pp. 420–434. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  36. 36.
    Friedgut, E., Kupferman, O., Vardi, M.Y.: Büchi complementation made tighter. Int’l J. of Foundations of Computer Science 17(4), 851–867 (2006)zbMATHCrossRefMathSciNetGoogle Scholar
  37. 37.
    Fritz, C.: Constructing Büchi automata from linear temporal logic using simulation relations for alternating bchi automata. In: Ibarra, O.H., Dang, Z. (eds.) CIAA 2003. LNCS, vol. 2759, pp. 35–48. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  38. 38.
    Fritz, C.: Concepts of automata construction from LTL. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 728–742. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  39. 39.
    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)Google Scholar
  40. 40.
    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, Springer, Heidelberg (2004)Google Scholar
  41. 41.
    Gentilini, R., Piazza, C., Policriti, A.: Computing strongly connected components in a linear number of symbolic steps. In: 14th ACM-SIAM Symposium on Discrete Algorithms, Baltimore, Maryland, pp. 573–582 (2003)Google Scholar
  42. 42.
    Gerth, R., et al.: Simple on-the-fly automatic verification of linear temporal logic. In: Dembiski, P., Sredniawa, M. (eds.) Protocol Specification, Testing, and Verification, pp. 3–18. Chapman and Hall, Boca Raton (1995)Google Scholar
  43. 43.
    Giannakopoulou, D., Lerda, F.: From states to transitions: Improving translation of LTL formulae to büchi automata. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol. 2529, pp. 308–326. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  44. 44.
    Godefroid, P., Holzmann, G.J.: On the verification of temporal properties. In: Proc. 13th Int. Conf on Protocol Specification Testing and Verification, pp. 109–124 (1993)Google Scholar
  45. 45.
    Gurumurthy, S., Bloem, R., Somenzi, F.: Fair simulation minimization. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, Springer, Heidelberg (2002)CrossRefGoogle Scholar
  46. 46.
    Gurumurthy, S., et al.: On complementing nondeterministic Büchi automata. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 96–110. Springer, Heidelberg (2003)Google Scholar
  47. 47.
    Hardin, R.H., Har’el, Z., Kurshan, R.P.: COSPAN. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, Springer, Heidelberg (1996)Google Scholar
  48. 48.
    Hardin, R.H., et al.: A new heuristic for bad cycle detection using BDDs. Formal Methods in System Design 18, 131–140 (2001)zbMATHCrossRefGoogle Scholar
  49. 49.
    Holzmann, G.J.: The model checker SPIN. IEEE Trans. on Software Engineering 23(5), 279–295 (1997)CrossRefMathSciNetGoogle Scholar
  50. 50.
    Holzmann, G.J., Peled, D., Yannakakis, M.: On nested depth-first search. In: Proc. 2nd Spin Workshop on The Spin Verification System, pp. 23–32. Amer. Math. Soc. (1996)Google Scholar
  51. 51.
    Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Formal methods in System Design 19(3), 291–314 (2001)zbMATHCrossRefMathSciNetGoogle Scholar
  52. 52.
    Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. ACM Trans. on Computational Logic 2(2), 408–429 (2001)CrossRefMathSciNetzbMATHGoogle Scholar
  53. 53.
    Kupferman, O., Vardi, M.Y.: From complementation to certification. Theoretical Computer Science 305, 591–606 (2005)MathSciNetGoogle Scholar
  54. 54.
    Kupferman, O., Vardi, M.Y.: From linear time to branching time. ACM Trans. on Computational Logic 6(2 6(2), 273–294 (2005)CrossRefMathSciNetGoogle Scholar
  55. 55.
    Kurshan, R.P.: Computer Aided Verification of Coordinating Processes. Princeton Univ. Press (1994)Google Scholar
  56. 56.
    Kurshan, R.P.: Formal verification in a commercial setting. In: Proc. Conf. on Design Automation (DAC‘97), vol. 34, pp. 258–262 (1997)Google Scholar
  57. 57.
    Latvala, T., et al.: Simple is better: Efficient bounded model checking for past ltl. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 380–395. Springer, Heidelberg (2005)Google Scholar
  58. 58.
    Löding, C.: Optimal bounds for the transformation of omega-automata. In: Pandu Rangan, C., Raman, V., Ramanujam, R. (eds.) Foundations of Software Technology and Theoretical Computer Science. LNCS, vol. 1738, pp. 97–109. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  59. 59.
    McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Norwell (1993)zbMATHGoogle Scholar
  60. 60.
    Michel, M.: Complementation is more difficult with automata on infinite words. CNET, Paris (1988)Google Scholar
  61. 61.
    Pnueli, A.: The temporal logic of programs. In: Proc. 18th IEEE Symp. on Foundation of Computer Science, pp. 46–57 (1977)Google Scholar
  62. 62.
    Pnueli, A.: The temporal logic of programs. In: Proc. 18th IEEE Symp. on Foundation of Computer Science, pp. 46–57. IEEE Computer Society Press, Los Alamitos (1977)Google Scholar
  63. 63.
    Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in Cesar. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) International Symposium on Programming. LNCS, vol. 137, pp. 337–351. Springer, Heidelberg (1982)Google Scholar
  64. 64.
    Rabin, M.O., Scott, D.: Finite automata and their decision problems. IBM Journal of Research and Development 3, 115–125 (1959)MathSciNetCrossRefGoogle Scholar
  65. 65.
    Safra, S.: On the complexity of ω-automata. In: Proc. 29th IEEE Symp. on Foundations of Computer Science, pp. 319–327, White Plains (October 1988)Google Scholar
  66. 66.
    Schwoon, S., Esparza, J.: A note on on-the-fly verification algorithms. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, Springer, Heidelberg (2005)Google Scholar
  67. 67.
    Sebastiani, R., Tonetta, S.: more deterministic” vs. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 126–140. Springer, Heidelberg (2003)Google Scholar
  68. 68.
    Sebastiani, R., Tonetta, S., Vardi, M.Y.: Symbolic systems, explicit properties: on hybrid approaches for LTL symbolic model checking. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, Springer, Heidelberg (2005)Google Scholar
  69. 69.
    Sistla, A.P., Vardi, M.Y., Wolper, P.: The complementation problem for Büchi automata with applications to temporal logic. Theoretical Computer Science 49, 217–237 (1987)zbMATHCrossRefMathSciNetGoogle Scholar
  70. 70.
    Somenzi, F., Bloem, R.: Efficient Büchi automata from LTL formulae. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, Springer, Heidelberg (2000)CrossRefGoogle Scholar
  71. 71.
    Somenzi, F., Ravi, K., Bloem, R.: Analysis of symbolic scc hull algorithms. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, Springer, Heidelberg (2002)Google Scholar
  72. 72.
    Tauriainen, H.: Nested emptiness search for generalized Büchi automata. Fundamenta Informaticae 70(1–2), 127–154 (2006)zbMATHMathSciNetGoogle Scholar
  73. 73.
    Thirioux, X.: Simple and efficient translation from LTL formulas to Büchi automata. Electr. Notes Theor. Comput. Sci. 66(2) (2002)Google Scholar
  74. 74.
    Vardi, M.Y.: Nontraditional applications of automata theory. In: Hagiya, M., Mitchell, J.C. (eds.) TACS 1994. LNCS, vol. 789, pp. 575–597. Springer, Heidelberg (1994)Google Scholar
  75. 75.
    Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency. LNCS, vol. 1043, pp. 238–266. Springer, Heidelberg (1996)Google Scholar
  76. 76.
    Vardi, M.Y.: Branching vs. linear time: Final showdown. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol. 2031, pp. 1–22. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  77. 77.
    Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proc. 1st Symp. on Logic in Computer Science, Cambridge, June 1986, pp. 332–344 (1986)Google Scholar
  78. 78.
    Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Information and Computation 115(1), 1–37 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  79. 79.
    Wolper, P.: Temporal logic can be more expressive. Information and Control 56(1–2), 72–99 (1983)zbMATHCrossRefMathSciNetGoogle Scholar
  80. 80.
    Wolper, P.: The tableau method for temporal logic: An overview. Logique et Analyse 136, 110–111 (1985)MathSciNetGoogle Scholar
  81. 81.
    Wolper, P., Vardi, M.Y., Sistla, A.P.: Reasoning about infinite computation paths. In: Proc. 24th IEEE Symp. on Foundations of Computer Science, Tucson, pp. 185–194 (1983)Google Scholar
  82. 82.
    Yan, Q.: Lower bounds for complementation of ω-automata via the full automata technique. In: Bugliesi, M., et al. (eds.) ICALP 2006. LNCS, vol. 4052, pp. 589–600. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  83. 83.
    Zhang, L., Malik, S.: The quest for efficient Boolean satisfiability solvers. In: Voronkov, A. (ed.) Automated Deduction - CADE-18. LNCS (LNAI), vol. 2392, pp. 295–313. Springer, Heidelberg (2002)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2007

Authors and Affiliations

  • Moshe Y. Vardi
    • 1
  1. 1.Rice University, Department of Computer Science, Houston, TX 77251-1892USA

Personalised recommendations