Satisfiability versus Finite Satisfiability in Elementary Modal Logics

• Autorzy: Michaliszyn J. , Otop J. , Witkowski P.

Identyfikatory

DOI

10.3233/FI-2018-1736

• Języki publikacji: EN

Abstrakty

EN

We study variants of the satisfiability problem of elementary modal logics, i.e., modal logic considered over first-order definable classes of frames. The standard semantics of modal logic allows infinite structures, but often practical applications require to restrict our attention to finite structures. A number of decidability and undecidability results for the elementary modal logics were proved separately for general satisfiability and finite satisfiability. In this paper we justify that the results for both kinds of the satisfiability problem must be shown separately – we prove that there is a universal first-order formula that defines an elementary modal logic with decidable general satisfiability problem, but undecidable finite satisfiability problem, and, the other way round, that there is a universal first-order formula that defines an elementary modal logic with decidable finite satisfiability problem, but undecidable general satisfiability problem.

Słowa kluczowe

EN

modality; satisfiability; computer science; logic; mathematics

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2018
• Tom: Vol. 163, nr 2
• Strony: 165--188
• Opis fizyczny: Bibliogr. 28 poz., rys., tab.

Twórcy

autor

Michaliszyn J.

• University of Wrocław, Faculty of Mathematics and Computer Science, Institute of Computer Science, F. Joliot-Curie 15, 50-383 Wrocław, Poland

autor

Otop J.

• University of Wrocław, Faculty of Mathematics and Computer Science, Institute of Computer Science, F. Joliot-Curie 15, 50-383 Wrocław, Poland

autor

Witkowski P.

• University of Wrocław, Faculty of Mathematics and Computer Science, Institute of Computer Science, F. Joliot-Curie 15, 50-383 Wrocław, Poland

Bibliografia

• [1] Sahlqvist H. Completeness and correspondence in the first and second order semantics for modal logic. Proceedings of the Third Scandinavian Logic Symposium. 1973; doi:10.1016/S0049-237X(08)70728-6.
• [2] Blackburn P, van Benthem JF, Wolter F. Handbook of modal logic. vol. 3. Elsevier; 2006. ISBN:9780444516909.
• [3] Mortimer M. On languages with two variables. Mathematical Logic Quarterly. 1975;21(1):135-140. doi:10.1002/malq.19750210118.
• [4] Otto M. Two Variable First-Order Logic over Ordered Domains. Journal of Symbolic Logic. 1998; 66:685-702. doi:10.2307/2695037.
• [5] Kieroński E, Michaliszyn J, Pratt-Hartmann I, Tendera L. Two-variable first-order logic with equivalence closure. In: LICS ’12: Proceedings of the 29th IEEE symposium on Logic in Computer Science; 2012. p. 431-440. doi:10.1109/LICS.2012.53.
• [6] Hemaspaandra E. The Price of Universality. Notre Dame Journal of Formal Logic. 1996;37(2):174-203. doi:10.1305/ndjfl/1040046086.
• [7] Hemaspaandra E, Schnoor H. A Universally Defined Undecidable Unimodal Logic. In: MFCS. vol. 6907 of LNCS. Springer; 2011. p. 364-375. doi:10.1007/978-3-642-22993-0_34.
• [8] Kieroński E, Michaliszyn J, Otop J. Modal Logics Definable by Universal Three-Variable Formulas. In: FSTTCS. vol. 13 of LIPIcs; 2011. p. 264-275. doi:10.4230/LIPIcs.FSTTCS.2011.264.
• [9] Grädel E. On the restraining power of guards. J Symbolic Logic. 1999;64(4):1719-1742. URL https://doi.org/10.2307/2586808.
• [10] Grädel E, Walukiewicz I. Guarded fixed point logic. In: Fourteenth Annual IEEE Symposium on Logic in Computer Science; 1999. p. 45-54. doi:10.1109/LICS.1999.782585.
• [11] Michaliszyn J. Decidability of the Guarded Fragment with the Transitive Closure. In: ICALP (2). vol. 5556 of LNCS. Springer; 2009. p. 261-272. doi:10.1007/978-3-642-02930-1_22.
• [12] Bárány V, Bojańczyk M. Finite satisfiability for guarded fixpoint logic. Inf Process Lett. 2012;112(10):371-375. doi:10.1016/j.ipl.2012.02.005.
• [13] Kieroński E, Tendera L. On Finite Satisfiability of the Guarded Fragment with Equivalence or Transitive Guards. In: LPAR. vol. 4790 of LNCS. Springer; 2007. p. 318-332. doi:10.1007/978-3-540-75560-9_24.
• [14] Hemaspaandra E, Schnoor H. On the Complexity of Elementary Modal Logics. In: STACS. vol. 1 of LIPIcs; 2008. p. 349-360. doi:10.4230/LIPIcs.STACS.2008.1356.
• [15] Michaliszyn J, Otop J. Decidable Elementary Modal Logics. In: Proceedings of the 29th IEEE symposium on Logic in Computer Science, LICS; 2012. p. 491-500. doi:10.1109/LICS.2012.59.
• [16] Vardi MY. Why is modal logic so robustly decidable? DIMACS Series in Discrete Mathematics and Theoretical Computer Science,. 1997;31:149-184.
• [17] Kieroński E, Michaliszyn J. Two-variable Universal Logic with Transitive Closure. In: Proceedings of Computer Science Logic 2012; 2012. p. 396-410. doi:10.4230/LIPIcs.CSL.2012.396.
• [18] Gorbunov I. A decidable modal logic that is finitely undecidable. In: Advances in Modal Logic 6, papers from the sixth conference on ”Advances in Modal Logic,” held in Noosa, Queensland, Australia, on 25-28 September 2006. College Publications; 2006. p. 247-258.
• [19] Blackburn P, de Rijke M, Venema Y. Modal Logic. vol. 53 of Cambridge Tracts in Theoretical Comp. Sc. Cambridge: Cambridge University Press; 2001. doi:10.1017/CBO9781107050884.
• [20] Montanari A, Puppis G, Sala P. Maximal Decidable Fragments of Halpern and Shoham’s Modal Logic of Intervals. In: ICALP (2). vol. 6199 of LNCS. Springer; 2010. p. 345-356. doi:10.1007/978-3-642-14162-1_29.
• [21] Michaliszyn J, Otop J, Witkowski P. Satisfiability vs. Finite Satisfiability in Elementary Modal Logics. In: Faella M, Murano A, editors. GandALF. vol. 96 of EPTCS; 2012. p. 141-154. doi:10.4204/EPTCS.96.11.
• [22] Berardi D, Calvanese D, De Giacomo G. Reasoning on UML class diagrams. Artif Intell. 2005;168(1-2):70-118. URL http://dx.doi.org/10.1016/j.artint.2005.05.003.
• [23] Zhao C, Heilili N, Liu S, Lin Z. Representation and Reasoning on RBAC: A Description Logic Approach. In: Theoretical Aspects of Computing - ICTAC 2005, Second International Colloquium, Hanoi, Vietnam, October 17-21, 2005, Proceedings; 2005. p. 381-393. URL http://dx.doi.org/10.1007/11560647\_25.
• [24] Berger R. The undecidability of the domino problem. Mem Amer Math Soc. 1966;66:72pp.
• [25] Börger E, Grädel E, Gurevich Y. The Classical Decision Problem. Perspectives in Mathematical Logic. Springer; 1997. ISBN-978-3-540-42324-9.
• [26] Szpilrajn E. Sur l’extension de l’ordre partiel. Fundamenta Mathematicae. 1930;16(1):386-389. URL http://eudml.org/doc/212499.
• [27] Michaliszyn J, Otop J. Elementary Modal Logics over Transitive Structures. In: Rocca SRD, editor. CSL. vol. 23 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik; 2013. p. 563-577. doi:10.4230/LIPIcs.CSL.2013.563.
• [28] Chandra AK, Kozen D, Stockmeyer LJ. Alternation. J ACM. 1981;28(1):114-133. URL http://doi.acm.org/10.1145/322234.322243.