States vs. Traces in Model Checking by Abstract Interpretation
In POPL’00, Cousot and Cousot showed that the classical state-based model checking of a very general temporal language called \( \mu \curvearrowleft \star \)-calculus is an incomplete abstract interpretation of its trace-based semantics. In ESOP’01, Ranzato showed that the least refinement of the state-based model checking semantics of the \( \mu \curvearrowleft \star \)-calculus which is complete w.r.t. its trace-based semantics exists, and it is essentially the trace-based semantics itself. The analogous problem in the opposite direction is solved by the present paper. First, relatively to any incomplete temporal connective of the \( \mu \curvearrowleft \star \)-calculus, we characterize the structure of the models, i.e. transition systems, for which the state-based model checking is trace-complete. On this basis, we prove that the unique abstraction of the state-based model checking semantics of the \( \mu \curvearrowleft \star \)-calculus (actually, of any fragment allowing conjunctions) which is complete w.r.t. the trace-based semantics is the straightforward semantics carrying no information at all. The following consequence can be drawn: there is no way to either refine or abstract sets of states in order to get a model checking algorithm for (any fragment allowing conjunctions of) the \( \mu \curvearrowleft \star \)-calculus which is trace-complete.
Unable to display preview. Download preview PDF.
- 1.T. Ball, A. Podelski, and S.K. Rajamani. Relative Completeness of Abstraction Refinement for Software Model Checking. In Proc. of TACAS’02, LNCS 2280, pp. 158–172, Springer, 2002.Google Scholar
- 2.C.H. Bennett. Logical reversibility of computation. IBM J. Research Dev., 21:905–940, 1981.Google Scholar
- 3.J. Chomicki. Temporal query languages: A survey. In Proc. 1st Int. Conf. on Temporal Logic, LNAI 827, pp. 506–534, Springer, 1994.Google Scholar
- 6.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, Springer, 2000.Google Scholar
- 7.E.M. Clarke, O. Grumberg, and D. Peled. Model checking, The MIT Press, 1999.Google Scholar
- 9.P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proc. ACM POPL’77, pp. 238–252. ACM Press, 1977.Google Scholar
- 10.P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Proc. ACM POPL’79, pp. 269–282. ACM Press, 1979.Google Scholar
- 11.P. Cousot and R. Cousot. Temporal abstract interpretation. In Proc. ACM POPL’00, pp. 12–25. ACM Press, 2000.Google Scholar
- 14.R. Giacobazzi and E. Quintarelli. Incompleteness, counterexamples and refinements in abstract model checking. In Proc. SAS’01, LNCS 2126, pp. 356–373, Springer, 2001.Google Scholar
- 16.M. Müller-Olm, D. Schmidt, and B. Steffen. Model checking: A tutorial introduction. In Proc. SAS’99, LNCS 1694, pp. 330–354. Springer, 1999.Google Scholar
- 17.F. Ranzato. On the completeness of model checking. In Proc. ESOP’01, LNCS 2028, pp. 137–154, Springer, 2001.Google Scholar