On the Completeness of Model Checking

  • Francesco Ranzato
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2028)


In POPL’00, Cousot and Cousot introduced and studied a novel general temporal specification language, called Open image in new window , in particular featuring a natural and rich time-symmetric trace-based semantics. The classical state-based model checking of the µ Open image in new window is an abstract interpretation of its trace-based semantics, which, surprisingly, turns out to be incomplete, even for finite systems. Cousot and Cousot identified the temporal connectives causing such incompleteness. In this paper, we first characterize the least, i.e. least informative, refinements of the state-based model checking abstraction which are complete relatively to any incomplete temporal connective. On the basis of this analysis, we show that the least refinement of the state-based model checking semantics of (a slight and natural monotone restriction of) the Open image in new window which is complete w.r.t. the trace-based semantics does exist, and it is essentially the trace-based semantics itself. This result can be read as stating that any model checking algorithm for the Open image in new window abstracting away from sets of traces will be necessarily incomplete.


  1. 1.
    E.M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In Proc. CAV’00, LNCS 1855, pp. 154–169, 2000.Google Scholar
  2. 2.
    E.M. Clarke, O. Grumberg and D. Long. Model checking and abstraction. ACM TOPLAS, 16(5):1512–1542, 1994.CrossRefGoogle Scholar
  3. 3.
    E.M. Clarke, O. Grumberg and D.A. Peled. Model checking. The MIT Press, 1999.Google Scholar
  4. 4.
    P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proc. 4th ACM POPL, pp. 238–252, 1977.Google Scholar
  5. 5.
    P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Proc. 6th ACM POPL, pp. 269–282, 1979.Google Scholar
  6. 6.
    P. Cousot and R. Cousot. Temporal abstract interpretation. In Proc. 27th ACM POPL, pp. 12–25, 2000.Google Scholar
  7. 7.
    D. Dams, O. Grumberg, and R. Gerth. Abstract interpretation of reactive systems. ACM TOPLAS, 16(5):1512–1542, 1997.Google Scholar
  8. 8.
    R. Giacobazzi, F. Ranzato, and F. Scozzari. Making abstract interpretations complete. J. ACM, 47(2):361–416, 2000.CrossRefMathSciNetzbMATHGoogle Scholar
  9. 9.
    D. Kozen. Results on the propositional μ-calculus. TCS, 27:333–354, 1983.zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, and S. Bensalem. Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design, 6:1–36, 1995.CrossRefGoogle Scholar
  11. 11.
    Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems Specification. Springer-Verlag, 1992.Google Scholar
  12. 12.
    M. Müller-Olm, D. Schmidt, and B. Steffen. Model-checking: a tutorial introduction. In Proc. SAS’99, LNCS 1694, pp. 330–354, 1999.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Francesco Ranzato
    • 1
  1. 1.Dipartimento di Matematica Pura ed ApplicataUniversità di PadovaPadovaItaly

Personalised recommendations