States vs. Traces in Model Checking by Abstract Interpretation

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


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.

Unable to display preview. Download preview PDF.


  1. 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. 2.
    C.H. Bennett. Logical reversibility of computation. IBM J. Research Dev., 21:905–940, 1981.Google Scholar
  3. 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
  4. 4.
    J. Chomicki, D. Toman, and M.H. Böhlen. Quering ATSQL databases with temporal logic. A CM Trans. Database Syst., 26(2):145–1178, 2001.CrossRefzbMATHGoogle Scholar
  5. 5.
    E.M. Clarke, O. Grumberg, and D. E. Long. Model checking and abstraction. A CM Trans. Program. Lang. Syst., 19(5):1512–1542, 1994.CrossRefGoogle Scholar
  6. 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. 7.
    E.M. Clarke, O. Grumberg, and D. Peled. Model checking, The MIT Press, 1999.Google Scholar
  8. 8.
    J. Clifford, A. Croker, and A. Tuzhilin. On completeness of historical relational query languages. A CM Trans. Database Syst., 19(1):64–116, 1994.CrossRefGoogle Scholar
  9. 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. 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. 11.
    P. Cousot and R. Cousot. Temporal abstract interpretation. In Proc. ACM POPL’00, pp. 12–25. ACM Press, 2000.Google Scholar
  12. 12.
    D. Dams, R. Gerth, and O. Grumberg. Abstract interpretation of reactive systems. A CM Trans. Program. Lang. Syst., 19(2):253–291, 1997.CrossRefGoogle Scholar
  13. 13.
    R. Giacobazzi, F. Ranzato, and F. Scozzari. Making abstract interpretations complete. J. A CM, 47(2):361–416, 2000.zbMATHMathSciNetGoogle Scholar
  14. 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
  15. 15.
    C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, and S. Bensalem. Property preserving abstractions for the verification of concurrent systems. Formal Methods Syst. Des., 6:1–36, 1995.CrossRefGoogle Scholar
  16. 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. 17.
    F. Ranzato. On the completeness of model checking. In Proc. ESOP’01, LNCS 2028, pp. 137–154, Springer, 2001.Google Scholar
  18. 18.
    A.P. Sistla and O. Wolfson. Temporal triggers in active databases. IEEE Trans. Knowl. Data. Eng., 7(3):471–486, 1995.CrossRefGoogle Scholar
  19. 19.
    A.U. Tansel. Adding time dimension to relational model and extending relational algebra. Information Systems, 11(4):343–355, 1986.zbMATHCrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Roberto Giacobazzi
    • 1
  • Francesco Ranzato
    • 2
  1. 1.Dipartimento di InformaticaUniversità di VeronaVeronaItaly
  2. 2.Dipartimento di Matematica Pura ed ApplicataUniversità di PadovaPadovaItaly

Personalised recommendations