Making Abstract Model Checking Strongly Preserving

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


Usually, abstract model checking is not strongly preserving: it may well exist a temporal specification which is not valid on the abstract model but which is instead satisfied by the concrete model. Starting from the standard notion of bisimulation, we introduce a notion of completeness for abstract models: completeness together with a so-called partitioning property for abstract models implies strong preservation for the past μ-calculus. Within a rigorous abstract interpretation framework, we show that the least refinement of a given abstract model, for a suitable ordering on abstract models, which is complete and partitioning always exists, and it can be constructively characterized as a greatest fixpoint. This provides a systematic methodology for minimally refining an abstract model checking in order to get strong preservation.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    S. Bensalem, Y. Lakhnech, S. Owre. Computing Abstractions of Infinite State Systems Compositionally and Automatically. In Proc. CAV’98, LNCS 1427, pp. 319–331, Springer, 1998.Google Scholar
  2. 2.
    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
  3. 3.
    E.M. Clarke, O. Grumberg, S. Jha, Y. Lu, H. Veith. Progress on the State Explosion Problem in Model Checking. In Informatics-10 Years Back, 10 Years Ahead. LNCS 2000, pp. 176–194, Springer, 2001.Google Scholar
  4. 4.
    E.M. Clarke, O. Grumberg, D.E. Long. Model checking and abstraction. In Proc. ACM POPL’92, pp. 342–354, 1992.Google Scholar
  5. 5.
    E.M. Clarke, O. Grumberg and D. Long. Model checking and abstraction. ACM TOPLAS, 16(5):1512–1542, 1994.CrossRefGoogle Scholar
  6. 6.
    E.M. Clarke, O. Grumberg and D.A. Peled. Model checking. The MIT Press, 1999.Google Scholar
  7. 7.
    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, 1977.Google Scholar
  8. 8.
    P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Proc. ACM POPL’79, pp. 269–282, 1979.Google Scholar
  9. 9.
    P. Cousot and R. Cousot. Temporal abstract interpretation. In Proc. ACM POPL’00, pp. 12–25, 2000.Google Scholar
  10. 10.
    D. Dams, O. Grumberg, and R. Gerth. Abstract interpretation of reactive systems. A CM TOPLAS, 16(5):1512–1542, 1997.Google Scholar
  11. 11.
    J. Dingel and T. Filkorn. Model checking for infinite state systems using data abstraction, assumption-commitment style reasoning and theorem proving. In Proc. CAV’95, LNCS 939, pp. 54–69, Springer, 1995.Google Scholar
  12. 12.
    G. Filé, R. Giacobazzi, and F. Ranzato. A unifying view of abstract domain design. A CM Comput. Surv., 28(2):333–336, 1996.CrossRefGoogle Scholar
  13. 13.
    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
  14. 14.
    R. Giacobazzi and F. Ranzato. Refining and compressing abstract domains. In Proc. ICALP’97, LNCS 1256, pp. 771–781, Springer, 1997.Google Scholar
  15. 15.
    R. Giacobazzi, F. Ranzato, and F. Scozzari. Making abstract interpretations complete. J. A CM, 47(2):361–416, 2000.zbMATHMathSciNetGoogle Scholar
  16. 16.
    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
  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.
    D.A. Schmidt. Binary relations for abstraction and refinement. In Proc. Workshop on Refinement and Abstraction, Japan 1999. To appear in Elsevier Electronic Notes in Computer Science.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Francesco Ranzato
    • 1
  • Francesco Tapparo
    • 1
    • 2
  1. 1.Dipartimento di Matematica Pura ed ApplicataUniversità di PadovaPadovaItaly
  2. 2.Dipartimento di MatematicaUniversità di MilanoMilanoItaly

Personalised recommendations