Abstract
Forwards-completeness is a concept in abstract interpretation expressing that an abstract and a concrete transformer have the same semantics with respect to an abstraction. When the set of transformers is generated by the signature of a logic, a forwards-complete abstraction of a structure is one that satisfies the same formulae in a given logic. We highlight a connection between models of positive modal logic, which are logics that lack negation and implication, and forwards-completeness. These models, which were discovered independently by researchers in modal logic, model checking, and static analysis of logic programs, correspond to Kripke structures with an order on their states. We show that forwards-completeness provides a new way to synthesize both models for positive modal logics and a notion of simulation for these models. The Kripke structures that can be synthesized using forwards-completeness satisfy a saturation condition which ensures that transition relations behave like best abstract transformers.
Supported by a Google Ph.D Fellowship.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Abdulla, P.A., Čeräns, K., Jonsson, B., Tsay, Y.K.: Algorithmic analysis of programs with well quasi-ordered domains. Inf. Comput. 160(1–2), 109–127 (2000)
Abramsky, S.: Domain Theory and the Logic of Observable Properties. Ph.d. thesis, University of London (1987)
Celani, S.A., Jansana, R.: A new semantics for positive modal logic. Notre Dame J. Formal Logic 38(1), 1–18 (1997)
Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Grumberg, O., Veith, H. (eds.) 25 Years of Model Checking. LNCS, vol. 5000, pp. 196–215. Springer, Berlin (2008). doi:10.1007/978-3-540-69850-0_12
Cousot, P., Cousot, R.: Abstract interpretation and application to logic programs. J. Logic Program. 13(2–3), 103–179 (1992)
Cousot, P.: Semantic foundations of program analysis. In: Muchnick, S., Jones, N. (eds.) Program Flow Analysis: Theory and Applications, pp. 303–342. Prentice-Hall Inc, Englewood Cliffs (1981). Chap. 10
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the Principles of Programming Languages, pp. 238–252. ACM, New York (1977)
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proceedings of the Principles of Programming Languages, pp. 269–282. ACM, New York (1979)
Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order. Cambridge University Press, Cambridge (1990)
D’Silva, V.: Generalizing simulation to abstract domains. In: D’Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013 – Concurrency Theory. LNCS, vol. 8052. Springer, Heidelberg (2013)
Dunn, J.M.: Positive modal logic. Stud. Logica 55(2), 301–317 (1995)
Dunn, J.M., Gehrke, M., Palmigiano, A.: Canonical extensions and relational completeness of some substructural logics. J. Symbolic Logic 70(3), 713–740 (2005)
Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere!. Theor. Comput. Sci. 256(1–2), 63–92 (2001)
Gehrke, M.: Generalized Kripke frames. Stud. Logica. 84(2), 241–275 (2006)
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, Berlin (2001). doi:10.1007/3-540-47764-0_20
Giacobazzi, R., Ranzato, F.: Optimal domains for disjunctive abstract interpretation. Sci. Comput. Program. 32(1–3), 177–210 (1998)
Giacobazzi, R., Ranzato, F., Scozzari, F.: Making abstract interpretations complete. J. ACM 47(2), 361–416 (2000)
Jónsson, B., Tarski, A.: Boolean algebras with operators. Am. J. Math. 74(1), 127–162 (1952)
Kildall, G.A.: A unified approach to global program optimization. In: Proceedings of the Principles of Programming Languages, pp. 194–206. ACM, New York (1973)
Kripke, S.: A completeness theorem in modal logic. J. Symbolic Logic 24(1), 1–14 (1959)
Lemmon, E.J.: Algebraic semantics for modal logics I. J. Symbolic Logic 31(1), 46–65 (1966)
Lemmon, E.J.: Algebraic semantics for modal logics II. J. Symbolic Logic 31(2), 191–218 (1966)
Libkin, L., Martens, W., Vrgoč, D.: Querying graphs with data. J. ACM 63(2), 14:1–14:53 (2016)
Loiseaux, C., Graf, S., Sifakis, J., Bouajjani, A., Bensalem, S.: Property preserving abstractions for the verification of concurrent systems. Formal Meth. Syst. Des. 6(1), 11–44 (1995)
McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Norwell (1993)
Nguyen, L.A.: On the complexity of fragments of modal logics. In: Advances in Modal Logic. vol. 5, pp. 249–268. Kings College Publications (2005)
Pratt, V.: Chu spaces. Course notes for the School in Category Theory and Applications, July 1999
Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol. 137, pp. 337–351. Springer, Heidelberg (1982). doi:10.1007/3-540-11494-7_22
Ranzato, F., Tapparo, F.: Generalized strong preservation by abstract interpretation. J. Logic Comput. 17(1), 157–197 (2007)
Schmidt, D.A.: Internal and external logics of abstract interpretations. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol. 4905, pp. 263–278. Springer, Berlin (2008). doi:10.1007/978-3-540-78163-9_23
Schmidt, D.A.: Inverse-limit and topological aspects of abstract interpretation. Theor. Comput. Sci. 430, 23–42 (2012)
Zufferey, D., Wies, T., Henzinger, T.A.: Ideal abstractions for well-structured transition systems. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 445–460. Springer, Berlin (2012). doi:10.1007/978-3-642-27940-9_29
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
D’Silva, V., Sousa, M. (2017). Complete Abstractions and Subclassical Modal Logics. In: Bouajjani, A., Monniaux, D. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2017. Lecture Notes in Computer Science(), vol 10145. Springer, Cham. https://doi.org/10.1007/978-3-319-52234-0_10
Download citation
DOI: https://doi.org/10.1007/978-3-319-52234-0_10
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-52233-3
Online ISBN: 978-3-319-52234-0
eBook Packages: Computer ScienceComputer Science (R0)