Skip to main content
SpringerLink
Log in

Model Checking: A Tutorial Overview

  • Chapter
  • First Online:
Modeling and Verification of Parallel Processes (MOVEP 2000)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2067))

Included in the following conference series:

Abstract

We survey principles of model checking techniques for the automatic analysis of reactive systems. The use of model checking is exemplified by an analysis of the Needham-Schroeder public key protocol. We then formally define transition systems, temporal logic, ω-automata, and their relationship. Basic model checking algorithms for linear- and branching-time temporal logics are defined, followed by an introduction to symbolic model checking and partial-order reduction techniques. The paper ends with a list of references to some more advanced topics.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

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 52.95
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.

Similar content being viewed by others

References

  1. Martín Abadi and Leslie Lamport. Conjoining specifications. ACM Transactions on Programming Languages and Systems, 17(3):507–534, May 1995.

    Article  Google Scholar 

  2. R. Alur. Timed automata. In Verification of Digital and Hybrid Systems, NATO ASI Series. Springer-Verlag, 1998.

    Google Scholar 

  3. R. Alur, C. Courcoubetis, and D. Dill. Model-checking for real-time systems. In 5th Ann. IEEE Symp. on Logics in Computer Science, pages 414–425. IEEE Press, 1990.

    Google Scholar 

  4. R. Alur and T. A. Henzinger. Logics and models of real time: a survey. In Real Time: Theory in Practice, volume 600 of Lecture Notes in Computer Science, pages 74–106. Springer-Verlag, 1992.

    Google Scholar 

  5. R. Alur, G. J. Holzmann, and D. Peled. An analyzer for message sequence charts. In B. Steffen and T. Margaria, editors, Tools and Constructions for the Analysis of Systems (TACAS’96), volume 1055 of Lecture Notes in Computer Science, pages 35–48, Passau, Germany, 1996. Springer-Verlag. See also http://cm.belllabs. com/cm/cs/what/ubet/index.html.

  6. Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. Alternating-time temporal logic. In 38th IEEE Symposium on Foundations of Computer Science, pages 100–109. IEEE Press, October 1997.

    Google Scholar 

  7. A. Anuchitanukul. Synthesis of Reactive Programs. PhD thesis, Stanford University, 1995.

    Google Scholar 

  8. H. Barringer, R. Kuiper, and A. Pnueli. Now you may compose temporal logic specifications. In 16th ACM Symp. on Theory of Computing, pages 51–63. ACM Press, 1984.

    Google Scholar 

  9. K. Baukus, S. Bensalem, Y. Lakhnech, and K. Stahl. Abstracting WS1S systems to verify parameterized networks. In S. Graf and M. Schwartzbach, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2000), volume 1785 of Lecture Notes in Computer Science, pages 188–203. Springer-Verlag, 2000.

    Google Scholar 

  10. J. Bern, C. Meinel, and A. Slobodová. Global rebuilding of BDDs-avoiding the memory requirement maxima. In P. Wolper, editor, 7th Workshop on Computer Aided Verification (CAV’95), volume 939 of Lecture Notes in Computer Science, pages 4–15. Springer-Verlag, 1995.

    Google Scholar 

  11. A. Biere, A. Cimatti, M. Fujita, and Y. Zhu. Symbolic model checking using SAT procedures instead of BDDs. In 36th ACM/IEEE Design Automation Conference (DAC’99), 1999.

    Google Scholar 

  12. Armin Biere. Effiziente Modellprüfung des µ-Kalküls mit binären Entscheidungsdiagrammen. PhD thesis, Univ. Karlsruhe, Germany, 1997.

    Google Scholar 

  13. B. Boigelot and P. Godefroid. Symbolic verification of communication protocols with infinite state spaces using QDDs. In R. Alur and T. Henzinger, editors, 8th Workshop on Computer-Aided Verification (CAV’96), volume 1102 of Lecture Notes in Computer Science, pages 1–12. Springer-Verlag, 1996.

    Google Scholar 

  14. G. Booch, J. Rumbaugh, and I. Jacobson. Unified Modelling Language: User Guide. Addison Wesley, 1999.

    Google Scholar 

  15. M. C. Browne, E. M. Clarke, and O. Grumberg. Reasoning about networks with many identical finite-state processes. Information and Computation, 81:13–31, 1989.

    Article  MATH  MathSciNet  Google Scholar 

  16. R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677–691, 1986.

    Article  Google Scholar 

  17. R. E. Bryant. On the complexity of VLSI implementations and graph representations of boolean functions with application to integer multiplication. IEEE Trans. on Computers, 40(2):205–213, 1991.

    Article  Google Scholar 

  18. R. E. Bryant. Symbolic boolean manipulations with ordered binary decision diagrams. ACM Computing Surveys, 24(3):293–317, 1992.

    Article  Google Scholar 

  19. J. R. Büchi. On a decision method in restricted second-order arithmetics. In International Congress on Logic, Method and Philosophy of Science, pages 1–12. Stanford University Press, 1962.

    Google Scholar 

  20. J. R. Burch, E. M. Clarke, K. L. McMillan, D. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142–170, 1992.

    Article  MATH  MathSciNet  Google Scholar 

  21. O. Burkart and J. Esparza. More infinite results. Electronic Notes in Theoretical Computer Science, 6, 1997. http://www.elsevier.nl/locate/entcs/volume6.html.

  22. Dominique Cansell, Dominique Méry, and Stephan Merz. Predicate diagrams for the verification of reactive systems. In 2nd Intl. Conf. on Integrated Formal Methods (IFM 2000), Lecture Notes in Computer Science, Dagstuhl, Germany, November 2000. Springer-Verlag. To appear.

    Google Scholar 

  23. E. M. Clarke, T. Filkorn, and S. Jha. Exploiting symmetry in temporal logic model checking. In C. Courcoubetis, editor, 5th Workshop on Computer-Aided Verifi cation (CAV’93), volume 697 of Lecture Notes in Computer Science, Elounda, Crete, 1993. Springer-Verlag.

    Google Scholar 

  24. E. M. Clarke, O. Grumberg, and K. Hamaguchi. Another look at LTL model checking. Formal Methods in System Design, 10:47–71, 1997.

    Article  Google Scholar 

  25. Edmund M. Clarke and E. Allen Emerson. Synthesis of synchronization skeletons for branching time temporal logic. In Workshop on Logic of Programs, volume 131 of Lecture Notes in Computer Science, Yorktown Heights, N.Y., 1981. Springer-Verlag.

    Google Scholar 

  26. Edmund M. Clarke, Orna Grumberg, and David E. Long. Model checking and abstraction. ACM Transactions on Programming Languages and Systems, 16(5):1512–1542, September 1994.

    Article  Google Scholar 

  27. Edmund M. Clarke, Orna Grumberg, and Doron Peled. Model Checking. MIT Press, Cambridge, MA, 1999.

    Google Scholar 

  28. Edmund M. Clarke and Holger Schlingloff. Model checking. In A. Voronkov, editor, Handbook of Automated Deduction. Elsevier, 2000. To appear.

    Google Scholar 

  29. E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finitestate concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244–263, 1986.

    Article  MATH  Google Scholar 

  30. E.M. Clarke, O. Grumberg, H. Hiraishi, S. Jha, D.E. Long, K.L. McMillan, and L.A. Ness. Verification of the Futurebus+ cache coherence protocol. In D. Agnew, L. Claesen, and R. Camposano, editors, IFIP Conference on Computer Hardware Description Languages and their Applications, pages 5–20, Ottawa, Canada, 1993. Elsevier Science Publishers B.V.

    Google Scholar 

  31. R. Cleaveland and S. Sims. Generic tools for verifying concurrent systems. Science of Computer Programming, 2000. See also http://www.cs.sunysb.edu/~cwb/.

  32. R. Cleaveland and B. Steffen. A linear-time model-checking algorithm for the alternation-free modal µ-calculus. Formal Methods in System Design, 2:121–147, 1993.

    Article  MATH  Google Scholar 

  33. P. Collette. An explanatory presentation of composition rules for assumptioncommitment specifications. Information Processing Letters, 50(1):31–35, 1994.

    Article  MATH  Google Scholar 

  34. C. Courcoubetis, M. Vardi, P. Wolper, and M. Yannakakis. Memory-efficient algorithms for the verification of temporal properties. Formal methods in system design, 1:275–288, 1992.

    Article  Google Scholar 

  35. Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In 4th ACM Symposium on Principles of Programming Languages, pages 238–252, lLos Angeles, California, 1977. ACM Press.

    Google Scholar 

  36. J.-M. Couvreur. On-the-fly verification of linear temporal logic. In J.M. Wing, J. Woodcock, and J. Davies, editors, FM’99-Formal Methods, volume 1708 of Lecture Notes in Computer Science, pages 253–271, Toulouse, France, 1999. Springer-Verlag.

    Chapter  Google Scholar 

  37. Dennis Dams, Orna Grumberg, and Rob Gerth. Abstract interpretation of reactive systems: Abstractions preserving ∀CTL*, ∃CTL* and CTL*. In Ernst-Rüdiger Olderog, editor, Programming Concepts, Methods, and Calculi (PROCOMET’ 94), pages 561–581, Amsterdam, 1994. North Holland/Elsevier.

    Google Scholar 

  38. M. Daniele, F. Giunchiglia, and M. Vardi. Improved automata generation for linear temporal logic. In Computer Aided Verification (CAV’99), volume 1633 of Lecture Notes in Computer Science, pages 249–260, Trento, Italy, 1999. Springer-Verlag.

    Google Scholar 

  39. Luca de Alfaro, Zohar Manna, Henny B. Sipma, and Tomás Uribe. Visual verification of reactive systems. In Ed Brinksma, editor, Tools and Algorithms for the Construction and Analysis of Systems (TACAS’97), volume 1217 of Lecture Notes in Computer Science, pages 334–350. Springer-Verlag, 1997.

    Google Scholar 

  40. W.-P. de Roever, H. Langmaack, and A. Pnueli, editors. Compositionality: The Significant Difference, volume 1536 of Lecture Notes in Computer Science. Springer-Verlag, 1998.

    Google Scholar 

  41. E. A. Emerson and J. Y. Halpern. “sometimes” and “not never” revisited: on branching time vs. linear time. Journal of the ACM, 33:151–178, 1986.

    Article  MATH  MathSciNet  Google Scholar 

  42. E. A. Emerson, C. S. Jutla, and A. P. Sistla. On model checking for fragments of µ-calculus. In C. Courcoubetis, editor, 5th Workshop on Computer-Aided Verification (CAV’93), volume 697 of Lecture Notes in Computer Science. Springer-Verlag, 1993.

    Google Scholar 

  43. E. A. Emerson and C. L. Lei. Modalities for model checking: Branching time strikes back. In 12th Symp. on Principles of Programming Languages (POPL’85), New Orleans, 1985. ACM Press.

    Google Scholar 

  44. E. A. Emerson and C. L. Lei. Efficient model checking in fragments of the propositional µ-calculus. In 1st Symp. on Logic in Computer Science, lBoston, Mass., 1986. IEEE Press.

    Google Scholar 

  45. E. Allen Emerson. Handbook of theoretical computer science, chapter Temporal and modal logic, pages 997–1071. Elsevier Science Publishers B.V., 1990.

    Google Scholar 

  46. E. Allen Emerson and Kedar S. Namjoshi. Automatic verification of parameterized synchronous systems. In R. Alur and T. Henzinger, editors, 8th International Conference on Computer Aided Verification (CAV’96), Lecture Notes in Computer Science. Springer-Verlag, 1996.

    Google Scholar 

  47. R. Enders, T. Filkorn, and D. Taubner. Generating BDDs for symbolic model checking. Distributed Computing, 6:155–164, 1993.

    Article  MATH  Google Scholar 

  48. J. Esparza. Model checking using net unfoldings. Science of Computer Programming, 23:151–195, 1994.

    Article  MATH  MathSciNet  Google Scholar 

  49. J. Esparza. Decidability of model-checking for infinite-state concurrent systems. Acta Informatica, 34:85–107, 1997.

    Article  MathSciNet  Google Scholar 

  50. J. Esparza, A. Finkel, and R. Mayr. On the verification of broadcast protocols. In 14th IEEE Symposium on Logic in Computer Science, pages 352–359, Trento, Italy, 1999. IEEE Press.

    Google Scholar 

  51. E. Felt, G. York, R. Brayton, and A. S. Vincentelli. Dynamic variable reordering for BDD minimization. In European Design Automation Conference, pages 130–135, 1993.

    Google Scholar 

  52. T. Firley, U. Goltz, M. Huhn, K. Diethers, and T. Gehrke. Timed sequence diagrams and tool-based analysis-a case study. In R. France and B. Rumpe, editors, 2nd Intl. Conference on the Unified Modelling Language (UML’99), volume 1723 of Lecture Notes in Computer Science, pages 645–660. Springer-Verlag, 1999.

    Google Scholar 

  53. H. Fuji, G. Oomoto, and C. Hori. Interleaving based variable ordering methods for binary decision diagrams. In Intl. Conf. on Computer Aided Design (ICCAD’93). IEEE Press, 1993.

    Google Scholar 

  54. D. Gabbay, I. Hodkinson, and M. Reynolds. Temporal Logic: Mathematical Foundations and Computational Aspects, volume 1. Clarendon Press, Oxford, UK, 1994.

    MATH  Google Scholar 

  55. S. M. German and A. P. Sistla. Reasoning about systems with many processes. Journal of the ACM, 39:675–735, 1992.

    Article  MATH  MathSciNet  Google Scholar 

  56. R. Gerth, D. Peled, M. Vardi, and P. Wolper. Simple on-the-fly automatic Verifi cation of linear temporal logic. In Protocol Specification, Testing, and Verification, pages 3–18, Warsaw, Poland, 1995. Chapman & Hall.

    Google Scholar 

  57. P. Godefroid and D. E. Long. Symbolic protocol verification with queue BDDs. In 11th Ann. IEEE Symp. on Logic in Computer Science (LICS’96), New Brunswick, NJ, 1996. IEEE Press.

    Google Scholar 

  58. P. Godefroid and P. Wolper. A partial approach to model checking. Information and Computation, 110(2):305–326, 1994.

    Article  MATH  MathSciNet  Google Scholar 

  59. Orna Grumberg and David E. Long. Model checking and modular verification. ACM Transactions on Programming Languages and Systems, 16(3):843–871, May 1994.

    Article  Google Scholar 

  60. David Harel and Amir Pnueli. On the development of reactive systems. In K. R. Apt, editor, Logics and Models of Concurrent Systems, volume F13 of NATO ASI Series, pages 477–498. Springer-Verlag, 1985.

    Google Scholar 

  61. T. A. Henzinger, P.-H. Ho, and H. Wong-Toi. HyTech: A model checker for hybrid systems. Software Tools for Technology Transfer, 1:110–122, 1997.

    Article  MATH  Google Scholar 

  62. T. A. Henzinger, Z. Manna, and A. Pnueli. Temporal proof methodologies for timed transition systems. Information and Computation, 112:273–337, 1994.

    Article  MATH  MathSciNet  Google Scholar 

  63. Thomas A. Henzinger, Orna Kupferman, and Moshe Y. Vardi. A space-efficient on-the-fly algorithm for real-time model checking. In 7th International Conference on Concurrency Theory (CONCUR 1996), volume 1119 of Lecture Notes in Computer Science, pages 514–529. Springer-Verlag, 1996.

    Google Scholar 

  64. Thomas A. Henzinger, Xavier Nicollin, Joseph Sifakis, and Sergio Yovin. Symbolic model checking for real-time systems. Information and Computation, 111:193–244, 1994.

    Article  MATH  MathSciNet  Google Scholar 

  65. Gerard Holzmann. The Spin model checker. IEEE Trans. on Software Engineering, 23(5):279–295, may 1997.

    Article  MathSciNet  Google Scholar 

  66. Gerard Holzmann. An analysis of bitstate hashing. Formal Methods in System Design, November 1998.

    Google Scholar 

  67. Gerard Holzmann and Doron Peled. An improvement in formal verification. In IFIP WG 6.1 Conference on Formal Description Techniques, pages 197–214, Bern, Switzerland, 1994. Chapman & Hall.

    Google Scholar 

  68. John E. Hopcroft and Jeffrey D. Ullman. Introduction to automata theory, languages, and computation. Addison-Wesley, Reading, Mass., 1979.

    Google Scholar 

  69. Michael Huth and Mark D. Ryan. Logic in Computer Science. Cambridge University Press, Cambridge, U.K., 2000.

    MATH  Google Scholar 

  70. C. N. Ip and D. Dill. Better verification through symmetry. In 11th Intl. Symp. on Computer Hardware Description Languages and their Applications, pages 87–100. North Holland, 1993.

    Google Scholar 

  71. C. N. Ip and D. Dill. Verifying systems with replicated components in Murphi. In Intl. Conference on Computer-Aided Verification (CAV’96), Lecture Notes in Computer Science. Springer-Verlag, 1996.

    Google Scholar 

  72. Bernhard Josko. Verifying the correctness of AADL modules using model checking. In J. W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness, volume 430 of Lecture Notes in Computer Science, pages 386–400. Springer-Verlag, Berlin, 1989.

    Google Scholar 

  73. Bernhard Josko. Modular Specification and Verification of Reactive Systems. PhD thesis, Univ. Oldenburg, Fachbereich Informatik, April 1993.

    Google Scholar 

  74. H. W. Kamp. Tense Logic and the Theory of Linear Order. PhD thesis, Univ. of California at Los Angeles, 1968.

    Google Scholar 

  75. Yonit Kesten and Amir Pnueli. Verifying liveness by augmented abstraction. In Annual Conference of the European Association for Computer Science Logic (CSL’99), Lecture Notes in Computer Science, Madrid, 1999. Springer-Verlag.

    Google Scholar 

  76. Nils Klarlund. Mona & Fido: The logic-automaton connection in practice. In Computer Science Logic, CSL’ 97, volume 1414 of LNCS, pages 311–326, Aarhus, Denmark, 1998.

    Google Scholar 

  77. Dexter Kozen. Results on the propositional mu-calculus. Theoretical Computer Science, 27:333–354, 1983.

    Article  MATH  MathSciNet  Google Scholar 

  78. Saul A. Kripke. Semantical considerations on modal logic. Acta Philosophica Fennica, 16:83–94, 1963.

    MATH  MathSciNet  Google Scholar 

  79. Fred Kröger. Temporal Logic of Programs, volume 8 of EATCS Monographs on Theoretical Computer Science. Springer-Verlag, Berlin, 1987.

    MATH  Google Scholar 

  80. O. Kupferman, M. Vardi, and P. Wolper. An automata-theoretic approach to branching-time model checking. In 6th Intl. Conf. on Computer-Aided Verification (CAV’94), Lecture Notes in Computer Science. Springer-Verlag, 1994. Full version (1999) available at http://www.cs.rice.edu/~vardi/papers/.

    Google Scholar 

  81. O. Kupferman and M. Y. Vardi. Verification of fair transition systems. In R. Alur and T. Henzinger, editors, 8th Workshop on Computer-Aided Verification (CAV’96), volume 1102 of Lecture Notes in Computer Science, pages 372–382. Springer-Verlag, 1996.

    Google Scholar 

  82. Orna Kupferman and Moshe Y. Vardi. Weak alternating automata are not so weak. In 5th Israeli Symposium on Theory of Computing and Systems, pages 147–158. IEEE Press, 1997.

    Google Scholar 

  83. R. P. Kurshan and K. L. McMillan. A structural induction theorem for processes. In 8th Ann. ACM Symp. on Principles of Distributed Computing. ACM Press, 1989.

    Google Scholar 

  84. Leslie Lamport. ’sometime’ is sometimes’ not never’. In Proc. 7th Ann. Symp. on Princ. of Prog. Lang. (POPL’80), pages 174–185. ACM SIGACT-SIGPLAN, January 1980.

    Google Scholar 

  85. M. Lange, M. Leucker, T. Noll, and S. Tobies. Truth-a verification platform for concurrent systems. In Tool Support for System Specification, Development, and Verification, Advances in Computing Science. Springer-Verlag Wien New York, 1999.

    Google Scholar 

  86. K. Larsen, P. Petterson, and W. Yi. Uppaal in a nutshell. Software Tools for Technology Transfer, 1, 1997.

    Google Scholar 

  87. Orna Lichtenstein, Amir Pnueli, and Lenore Zuck. The glory of the past. In Rohit Parikh, editor, Logics of Programs, volume 193 of Lecture Notes in Computer Science, pages 196–218, Berlin, June 1985. Springer-Verlag.

    Google Scholar 

  88. J. Lilius and I. P. Paltor. Formalising UML state machines for model checking. In R. France and B. Rumpe, editors, UML’99-Beyond the Standard, volume 1723 of Lecture Notes in Computer Science. Springer-Verlag, 1999.

    Google Scholar 

  89. Claire Loiseaux, Susanne Graf, Joseph Sifakis, Ahmed Bouajjani, and Saddek Bensalem. Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design, 6:11–44, 1995. A preliminary version appeared as Spectre technical report RTC40, Grenoble, France, 1993.

    Article  Google Scholar 

  90. D. E. Long. Model checking, Abstraction and Compositional Verification. PhD thesis, CMU School of Computer Science, 1993. CMU-CS-93-178.

    Google Scholar 

  91. Gavin Lowe. Breaking and fixing the Needham-Schroeder public key protocol using FDR. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS’96), volume 1055 of Lecture Notes in Computer Science, pages 147–166. Springer-Verlag, 1996.

    Google Scholar 

  92. Z. Manna, A. Browne, H.B. Sipma, and T.E. Uribe. Visual abstractions for temporal verification. In A. Haeberer, editor, AMAST’98, volume 1548 of Lecture Notes in Computer Science, pages 28–41. Springer-Verlag, 1998.

    Google Scholar 

  93. Zohar Manna and Amir Pnueli. A hierarchy of temporal properties. In 9th. ACM Symposium on Principles of Distributed Computing, pages 377–408. ACM, 1990.

    Google Scholar 

  94. Zohar Manna and Amir Pnueli. The temporal logic of reactive and concurrent systems-Specification. Springer-Verlag, New York, 1992.

    Google Scholar 

  95. Zohar Manna and Amir Pnueli. The temporal logic of reactive and concurrent systems-Safety properties. Springer-Verlag, New York, 1995.

    Google Scholar 

  96. Kenneth L. McMillan. A compositional rule for hardware design refinement. In O. Grumberg, editor, 9th International Conference on Computer Aided Verification (CAV’97), volume 1254 of Lecture Notes in Computer Science, pages 24–35, Haifa, Israel, 1997. Springer-Verlag.

    Google Scholar 

  97. K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.

    Google Scholar 

  98. R. McNaughton and S. Papert. Counter-Free Automata. MIT Press, Cambridge, Mass., 1971.

    MATH  Google Scholar 

  99. Stephan Merz. Rules for abstraction. In R. K. Shyamasundar and K. Ueda, editors, Advances in Computing Science-ASIAN’97, volume 1345 of Lecture Notes in Computer Science, pages 32–45, Kathmandu, Nepal, December 1997. Springer-Verlag.

    Google Scholar 

  100. Faron Moller. Infinite results. In U. Montanari and V. Sassone, editors, 7th International Conference on Concurrency Theory (CONCUR’96), volume 1119 of Lecture Notes in Computer Science, pages 195–216, Pisa, Italy, 1996. Springer-Verlag.

    Google Scholar 

  101. D. E. Muller. Infinite sequences and finite machines. In Switching Circuit Theory and Logical Design: Fourth Annual Symposium, pages 3–16, New York, 1963. IEEE Press.

    Google Scholar 

  102. D. E. Muller, A. Saoudi, and P. E. Schupp. Alternating automata, the weak monadic theory of the tree and its complexity. In 13th ICALP, volume 226 of Lecture Notes in Computer Science, pages 275–283. Springer-Verlag, 1986.

    Google Scholar 

  103. D.E. Muller, A. Saoudi, and P.E. Schupp. Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time. In 3rd IEEE Symposium on Logic in Computer Science, pages 422–427. IEEE Press, 1988.

    Google Scholar 

  104. Roger Needham and Michael Schroeder. Using encryption for authentication in large networks of computers. Communications of the ACM, 21(12):993–999, 1978.

    Article  MATH  Google Scholar 

  105. D. M. Park. Finiteness is mu-ineffable. Theory of Computation Report 3, University of Warwick, 1974.

    Google Scholar 

  106. Lawrence C. Paulson. Proving security protocols correct. In 14th IEEE Symposium on Logic in Computer Science, pages 370–383, Trento, Italy, 1999. IEEE Press.

    Google Scholar 

  107. D. Peled. Combining partial order reductions with on-the-fly model-checking. Formal Methods in System Design, 8(1):39–64, 1996.

    Article  Google Scholar 

  108. W. Penczek, R. Gerth, and R. Kuiper. Partial order reductions preserving simulations. Submitted for publication, 1999.

    Google Scholar 

  109. Amir Pnueli. In transition from global to modular temporal reasoning about programs. In K. R. Apt, editor, Logics and Models of Concurrent Systems, volume F13 of ASI, pages 123–144. Springer-Verlag, Berlin, 1985.

    Google Scholar 

  110. M. O. Rabin. Decidability of second-order theories and automata on infinite trees. Transactions of the American Mathematical Society, 141:1–35, 1969.

    Article  MATH  MathSciNet  Google Scholar 

  111. Shmuel Safra. On the complexity of ω-automata. In 29th IEEE Symposium on Foundations of Computer Science, pages 319–327. IEEE Press, 1988.

    Google Scholar 

  112. Klaus Schneider. Yet another look at LTL model checking. In IFIP Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME’99), Lecture Notes in Computer Science, Bad Herrenalb, Germany, 1999.

    Google Scholar 

  113. H.B. Sipma, T.E. Uribe, and Z. Manna. Deductive model checking. In 8th International Conference on Computer-Aided Verification, volume 1102 of Lecture Notes in Computer Science, pages 208–219, New Brunswick, N.J., 1996. Springer-Verlag.

    Google Scholar 

  114. A.P. Sistla and E.M. Clarke. The complexity of propositional linear temporal logic. Journal of the ACM, 32:733–749, 1985.

    Article  MATH  MathSciNet  Google Scholar 

  115. G. Stålmarck. A system for determining propositional logic theorems by applying values and rules to triplets that are generated from a formula. Swedish Patent No. 467076 (1992), US Patent No. 5 276 897 (1994), European Patent No. 0404 454 (1995).

    Google Scholar 

  116. P. H. Starke. Reachability analysis of Petri nets using symmetries. Syst. Anal. Model. Simul., 8:293–303, 1991.

    MathSciNet  Google Scholar 

  117. Colin Stirling. Handbook of Logic in Computer Science, volume 2, chapter Modal and temporal logics, pages 477–563. Oxford Science Publications, Clarendon Press, Oxford, 1992.

    Google Scholar 

  118. Colin Stirling. Bisimulation, model checking, and other games. Mathfit instructional meeting on games and computation, 1997. Available at http://www.dcs. ed.ac.uk/home/cps/.

  119. R. E. Tarjan. Depth first search and linear graph algorithms. SIAM Journal of Computing, 1:146–160, 1972.

    Article  MATH  MathSciNet  Google Scholar 

  120. Wolfgang Thomas. Automata on infinite objects. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, pages 133–194. Elsevier, Amsterdam, 1990.

    Google Scholar 

  121. Wolfgang Thomas. Languages, automata, and logic. In G. Rozenberg and A. Salomaa, editors, Handbook of Formal Language Theory, volume III, pages 389–455. Springer-Verlag, New York, 1997.

    Google Scholar 

  122. Wolfgang Thomas. Complementation of Büchi automata revisited. In J. Karhumäki, editor, Jewels are Forever, Contributions on Theoretical Computer Science in Honor of Arto Salomaa, pages 109–122. Springer-Verlag, 2000.

    Google Scholar 

  123. A. Valmari. A stubborn attack on state explosion. In 2nd International Workshop on Computer Aided Verification, volume 531 of Lecture Notes in Computer Science, pages 156–165, Rutgers, June 1990. Springer-Verlag.

    Google Scholar 

  124. A. Valmari. The state explosion problem. In Lectures on Petri Nets I: Basic Models, volume 1491 of Lecture Notes in Computer Science, pages 429–528. Springer-Verlag, 1998.

    Google Scholar 

  125. Moshe Y. Vardi. Alternating automata and program verification. In Computer Science Today, volume 1000 of Lecture Notes in Computer Science, pages 471–485. Springer-Verlag, 1995.

    Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  127. P. Wolper and V. Lovinfosse. Verifying properties of large sets of processes with network invariants. In J. Sifakis, editor, Intl. Workshop on Automatic Verification Methods for Finite State Systems, volume 407 of Lecture Notes in Computer Science. Springer-Verlag, 1989.

    Google Scholar 

  128. Pierre Wolper. Temporal logic can be more expressive. Information and Control, 56:72–93, 1983.

    Article  MATH  MathSciNet  Google Scholar 

  129. S. Yovine. Kronos: A verification tool for real-time systems. Software Tools for Technology Transfer, 1, 1997.

    Google Scholar 

  130. H. Zhang. Sato: An efficient propositional prover. In Intl. Conf. on Automated Deduction (CADE’97), number 1249 in Lecture Notes in Computer Science, pages 272–275. Springer-Verlag, 1997.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Universität München, Germany

    Stephan Merz

Authors
  1. Stephan Merz
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. IRCCyN, CNRS, 1 rue de la Noe, 44321, Nantes Cedex 3, France

    Franck Cassez

  2. IRISA, CNRS, Campus de Beaulieu, 35042, Rennes, France

    Claude Jard

  3. Laboratoire de Recherche en Informatique, Université de Paris XI, Bâtiment 490, 91405, Orsay Cedex, France

    Brigitte Rozoy

  4. School of Computer Science, University of Birmingham, Edgbaston, Birmingham, B15 2TT, UK

    Mark Dermot Ryan

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Merz, S. (2001). Model Checking: A Tutorial Overview. In: Cassez, F., Jard, C., Rozoy, B., Ryan, M.D. (eds) Modeling and Verification of Parallel Processes. MOVEP 2000. Lecture Notes in Computer Science, vol 2067. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45510-8_1

Download citation

  • DOI: https://doi.org/10.1007/3-540-45510-8_1

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-42787-2

  • Online ISBN: 978-3-540-45510-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation