Abstract
Standard abstract model checking relies on abstract Kripke structures which approximate the concrete model by gluing together indistinguishable states. Strong preservation for a specification language \(\mathcal{L}\) encodes the equivalence of concrete and abstract model checking of formulas in \(\mathcal{L}\). Abstract interpretation allows to design abstract models which are more general than abstract Kripke structures. In this paper we show how abstract interpretation-based models can be exploited in order to specify a general strongly preserving abstract model checking framework. This is shown in particular for specification languages including standard temporal operators which admit a characterization as least/greatest fixpoints, as e.g. standard “Finally”, “Globally”, “Until” and “Release” modalities.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Progress on the state explosion problem in model checking. In: Wilhelm, R. (ed.) Informatics: 10 Years Back, 10 Years Ahead. LNCS, vol. 2000, pp. 176–194. Springer, Heidelberg (2001)
Clarke, E.M., Grumberg, O., Long, D.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512–1542 (1994)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. 4\(^{\mathit{th}}\) ACM POPL, pp. 238–252 (1977)
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proc. 6\(^{\mathit{th}}\) ACM POPL, pp. 269–282 (1979)
Cousot, P., Cousot, R.: Refining model checking by abstract interpretation. Automated Software Engineering Journal 6(1), 69–95 (1999)
Cousot, P., Cousot, R.: Temporal abstract interpretation. In: Proc. 27\(^{\mathit{th}}\) ACM POPL, pp. 12–25 (2000)
Dams, D.: Abstract Interpretation and Partition Refinement for Model Checking. PhD Thesis, Eindhoven Univ (1996)
Dams, D.: Flat fragments of CTL and CTL*: separating the expressive and distinguishing powers. Logic J. of the IGPL 7(1), 55–78 (1999)
Dams, D., Grumberg, O., Gerth, R.: Abstract interpretation of reactive systems. ACM Trans. Program. Lang. Syst. 16(5), 1512–1542 (1997)
Giacobazzi, R., Quintarelli, E.: Incompleteness, counterexamples and refinements in abstract model checking. In: Cousot, P. (ed.) SAS 2001. LNCS, vol. 2126, pp. 356–373. Springer, Heidelberg (2001)
Giacobazzi, R., Ranzato, F., Scozzari, F.: Making abstract interpretations complete. J. ACM 47(2), 361–416 (2000)
Grumberg, O., Long, D.E.: Model checking and modular verification. ACM Trans. Program. Lang. Syst. 16(3), 843–871 (1994)
Henzinger, M.R., Henzinger, T.A., Kopke, P.W.: Computing simulations on finite and infinite graphs. In: Proc. 36\(^{\mathit{th}}\) FOCS, pp. 453–462 (1995)
Loiseaux, C., Graf, S., Sifakis, J., Bouajjani, A., Bensalem, S.: Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design 6, 1–36 (1995)
Massé, D.: Semantics for abstract interpretation-based static analyzes of temporal properties. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 428–443. Springer, Heidelberg (2002)
Ranzato, F., Tapparo, F.: Strong preservation as completeness in abstract interpretation. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 18–32. Springer, Heidelberg (2004)
Ranzato, F., Tapparo, F.: An abstract interpretation-based refinement algorithm for strong preservation. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 140–156. Springer, Heidelberg (2005)
Schmidt, D.A.: Closed and logical relations for over- and under-approximation of powersets. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 22–37. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ranzato, F., Tapparo, F. (2005). Strong Preservation of Temporal Fixpoint-Based Operators by Abstract Interpretation. In: Emerson, E.A., Namjoshi, K.S. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2006. Lecture Notes in Computer Science, vol 3855. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11609773_22
Download citation
DOI: https://doi.org/10.1007/11609773_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-31139-3
Online ISBN: 978-3-540-31622-0
eBook Packages: Computer ScienceComputer Science (R0)