Abstract
This paper describes a framework, based on Abstract Interpretation, for creating abstractions for model-checking. Specifically, we study how to abstract models of μ-calculus and systematically derive abstractions that are constructive, sound, and precise, and apply them to abstracting Kripke structures. The overall approach is based on the use of bilattices to represent partial and inconsistent information.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Ball, T., Levin, V., Xie, F.: Automatic Creation of Environment Models via Training. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 93–107. Springer, Heidelberg (2004)
Ball, T., Rajamani, S.: “The SLAM Toolkit”. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 260–264. Springer, Heidelberg (2001)
Belnap, N.D.: A Useful Four-Valued Logic. In: Dunn, Epstein (eds.) Modern Uses of Multiple-Valued Logic, Reidel, pp. 30–56 (1977)
Chechik, M., Devereux, B., Easterbrook, S., Gurfinkel, A.: Multi-Valued Symbolic Model-Checking. ACM TOSEM 12(4), 1–38 (2003)
Clarke, E.M., Grumberg, O., Long, D.E.: Model Checking and Abstraction. ACM TOPLAS 16(5), 1512–1542 (1994)
Corbett, J., Dwyer, M., Hatcliff, J., Laubach, S., Pasareanu, C., Robby, Zheng, H.: Bandera: Extracting Finite-state Models from Java Source Code. In: ICSE 2000, pp. 439–448 (2000)
Cousot, P., Cousot, R.: Abstract Interpretation Frameworks. Journal of Logic and Computation 2(4), 511–547 (1992)
Dams, D., Gerth, R., Grumberg, O.: Abstract Interpretation of Reactive Systems. ACM TOPLAS 2(19), 253–291 (1997)
Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order. Cambridge University Press, Cambridge (1990)
de Alfaro, L., Faella, M., Henzinger, T.A., Majumdar, R., Stoelinga, M.: “Model Checking Discounted Temporal Properties”. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 77–92. Springer, Heidelberg (2004)
de Alfaro, L., Godefroid, P., Jagadeesan, R.: Three-Valued Abstractions of Games: Uncertainty, but with Precision. In: LICS 2004, pp. 170–179 (2004)
Emerson, E.A., Sistla, A.P.: Symmetry and Model Checking. FMSD 9(1-2), 105–131 (1996)
Emerson, E.A., Wahl, T.: Dynamic Symmetry Reduction. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 382–396. Springer, Heidelberg (2005)
Fitting, M.: Bilattices are Nice Things. In: Conference on Self-Reference (2002)
Ginsberg, M.L.: Multivalued Logics: A Uniform Approach to Reasoning in Artificial Intelligence. Computational Intelligence 4(3), 265–316 (1988)
Godefroid, P., Huth, M., Jagadeesan, R.: Abstraction-based Model Checking using Modal Transition Systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 426–440. Springer, Heidelberg (2001)
Graf, S., Saïdi, H.: Construction of Abstract State Graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)
Gurfinkel, A., Chechik, M.: Yasm: Model-Checking Software with Belnap Logic. Technical Report 533, University of Toronto (April 2005)
Gurfinkel: A., Wei, O., Chechik, M.: Logical Abstract Interpretation. Technical Report 532, University of Toronto (September 2005)
Kozen, D.: Results on the Propositional μ-calculus. Theoretical Computer Science 27, 334–354 (1983)
Larsen, K.G., Thomsen, B.: A Modal Process Logic. In: LICS 1988, pp. 203–210 (1988)
Loiseaux, C., Graf, S., Sifakis, J., Bouajjani, A., Bensalem, S.: Property Preserving Abstractions for the Verification of Concurrent Systems. FMSD 6, 1–35 (1995)
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)
Shoham, S., Grumberg, O.: Monotonic Abstraction-Refinement for CTL. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 546–560. Springer, Heidelberg (2004)
Wei, O., Gurfinkel, A., Chechik, M.: Identification and Counter Abstraction for Full Virtual Symmetry. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 285–300. Springer, Heidelberg (2005)
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
Gurfinkel, A., Wei, O., Chechik, M. (2005). Systematic Construction of Abstractions for Model-Checking. 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_25
Download citation
DOI: https://doi.org/10.1007/11609773_25
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)