Top

Published in:

2017 | OriginalPaper | Chapter

Complete Abstractions and Subclassical Modal Logics

Authors : Vijay D’Silva, Marcelo Sousa

Published in: Verification, Model Checking, and Abstract Interpretation

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Independence Abstractions and Models of Concurrency

next chapter Using Abstract Interpretation to Correct Synchronization Faults

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)MathSciNetCrossRefMATH

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)MathSciNetCrossRefMATH

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 CrossRef

Cousot, P., Cousot, R.: Abstract interpretation and application to logic programs. J. Logic Program. 13(2–3), 103–179 (1992)MathSciNetCrossRefMATH

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)MATH

10.

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)

11.

Dunn, J.M.: Positive modal logic. Stud. Logica 55(2), 301–317 (1995)MathSciNetCrossRefMATH

12.

Dunn, J.M., Gehrke, M., Palmigiano, A.: Canonical extensions and relational completeness of some substructural logics. J. Symbolic Logic 70(3), 713–740 (2005)MathSciNetCrossRefMATH

13.

Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere!. Theor. Comput. Sci. 256(1–2), 63–92 (2001)MathSciNetCrossRefMATH

14.

Gehrke, M.: Generalized Kripke frames. Stud. Logica. 84(2), 241–275 (2006)MathSciNetCrossRefMATH

15.

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 CrossRef

16.

Giacobazzi, R., Ranzato, F.: Optimal domains for disjunctive abstract interpretation. Sci. Comput. Program. 32(1–3), 177–210 (1998)MathSciNetCrossRefMATH

17.

Giacobazzi, R., Ranzato, F., Scozzari, F.: Making abstract interpretations complete. J. ACM 47(2), 361–416 (2000)MathSciNetCrossRefMATH

18.

Jónsson, B., Tarski, A.: Boolean algebras with operators. Am. J. Math. 74(1), 127–162 (1952)MathSciNetCrossRefMATH

19.

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)

20.

Kripke, S.: A completeness theorem in modal logic. J. Symbolic Logic 24(1), 1–14 (1959)MathSciNetCrossRefMATH

21.

Lemmon, E.J.: Algebraic semantics for modal logics I. J. Symbolic Logic 31(1), 46–65 (1966)MathSciNetCrossRefMATH

22.

Lemmon, E.J.: Algebraic semantics for modal logics II. J. Symbolic Logic 31(2), 191–218 (1966)MathSciNetCrossRefMATH

23.

Libkin, L., Martens, W., Vrgoč, D.: Querying graphs with data. J. ACM 63(2), 14:1–14:53 (2016)MathSciNetCrossRef

24.

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)CrossRefMATH

25.

McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Norwell (1993)CrossRefMATH

26.

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)

27.

Pratt, V.: Chu spaces. Course notes for the School in Category Theory and Applications, July 1999

28.

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 CrossRef

29.

Ranzato, F., Tapparo, F.: Generalized strong preservation by abstract interpretation. J. Logic Comput. 17(1), 157–197 (2007)MathSciNetCrossRefMATH

30.

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 CrossRef

31.

Schmidt, D.A.: Inverse-limit and topological aspects of abstract interpretation. Theor. Comput. Sci. 430, 23–42 (2012)MathSciNetCrossRefMATH

32.

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 CrossRef

Title: Complete Abstractions and Subclassical Modal Logics
Authors: Vijay D’Silva
Marcelo Sousa
Publisher: Springer International Publishing
Book: Verification, Model Checking, and Abstract Interpretation
Print ISBN: 978-3-319-52233-3

Electronic ISBN: 978-3-319-52234-0

Copyright Year: 2017
DOI: https://doi.org/10.1007/978-3-319-52234-0_10

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner