Abstract
In POPL’00, Cousot and Cousot introduced and studied a novel general temporal specification language, called , in particular featuring a natural and rich time-symmetric trace-based semantics. The classical state-based model checking of the µ 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 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 abstracting away from sets of traces will be necessarily incomplete.
Chapter PDF
Similar content being viewed by others
References
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.
E.M. Clarke, O. Grumberg and D. Long. Model checking and abstraction. ACM TOPLAS, 16(5):1512–1542, 1994.
E.M. Clarke, O. Grumberg and D.A. Peled. Model checking. The MIT Press, 1999.
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.
P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Proc. 6th ACM POPL, pp. 269–282, 1979.
P. Cousot and R. Cousot. Temporal abstract interpretation. In Proc. 27th ACM POPL, pp. 12–25, 2000.
D. Dams, O. Grumberg, and R. Gerth. Abstract interpretation of reactive systems. ACM TOPLAS, 16(5):1512–1542, 1997.
R. Giacobazzi, F. Ranzato, and F. Scozzari. Making abstract interpretations complete. J. ACM, 47(2):361–416, 2000.
D. Kozen. Results on the propositional μ-calculus. TCS, 27:333–354, 1983.
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.
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems Specification. Springer-Verlag, 1992.
M. Müller-Olm, D. Schmidt, and B. Steffen. Model-checking: a tutorial introduction. In Proc. SAS’99, LNCS 1694, pp. 330–354, 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ranzato, F. (2001). On the Completeness of Model Checking. In: Sands, D. (eds) Programming Languages and Systems. ESOP 2001. Lecture Notes in Computer Science, vol 2028. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45309-1_10
Download citation
DOI: https://doi.org/10.1007/3-540-45309-1_10
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41862-7
Online ISBN: 978-3-540-45309-3
eBook Packages: Springer Book Archive