Filter by type:

Sort by year

Why propositional quantification makes modal logics on trees robustly hard ?

Bartosz Bednarczyk, Stephane Demri
Conference Papers Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019

Abstract

Adding propositional quantification to the modal logics K, T or S4 is known to lead to undecidability whereas CTL with propositional quantification under the tree semantics (written QCTLt) admits a non-elementary Tower-complete satisfiability problem. We investigate the complexity of strict fragments of QCTLt as well as of the modal logic K with propositional quantification under the tree semantics. More specifically, we show that QCTLt restricted to the temporal operator EX is already Tower-hard, which is unexpected as, for instance, EX can only enforce local properties. When QCTLt restricted to EX is interpreted on N-bounded trees for some N >= 2, we prove that the satisfiability problem is AExppol-complete; AExppol-hardness is established by reduction from a recently introduced tiling problem, instrumental for studying the model-checking problem for interval temporal logics. As significant consequences of our proof method, we prove Tower-hardness of QCTLt restricted to EF or to EXEF and of the well-known modal logics K, KD, GL, S4, K4 and D4, with propositional quantification under a semantics based on classes of trees.

On the Complexity of Graded Modal Logics with Converse

Bartosz Bednarczyk, Emanuel Kieroński, Piotr Witkowski
Conference Papers Proceedings of the 16th Edition of the European Conference on Logics in Artificial Intelligence (JELIA 2019)

Abstract

A complete classification of the complexity of the local and global satisfiability problems for graded modal language over traditional classes of frames has already been established. By 'traditional' classes of frames we mean those characterized by any positive combination of reflexivity, seriality, symmetry, transitivity, and the Euclidean property. In this paper we fill the gaps remaining in an analogous classification of the graded modal language with graded converse modalities. In particular we show its NExpTime-completeness over the class of Euclidean frames, demonstrating this way that over this class the considered language is harder than the language without graded modalities or without converse modalities. We also consider its variation disallowing graded converse modalities, but still admitting basic converse modalities. Our most important result for this variation is confirming an earlier conjecture that it is decidable over transitive frames. This contrasts with the undecidability of the language with graded converse modalities.

Modulo Counting on Words and Trees

Bartosz Bednarczyk, Witold Charatonik
Conference Papers Proceedings of the 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2017, December 11–15, 2017, Kanpur, India. LIPIcs 93, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik 2017, pages 12:1–12:16.

Abstract

We consider the satisfiability problem for the two-variable fragment of the first-order logic extended with modulo counting quantifiers and interpreted over finite words or trees. We prove a small-model property of this logic, which gives a technique for deciding the satisfiability problem. In the case of words this gives a new proof of EXPSPACE upper bound, and in the case of trees it gives a 2EXPTIME algorithm. This algorithm is optimal: we prove a matching lower bound by a generic reduction from alternating Turing machines working in exponential space; the reduction involves a development of a new version of tiling games.

Extending Two-Variable Logic on Trees

Bartosz Bednarczyk, Witold Charatonik, Emanuel Kieroński
Conference Papers Proceedings of the 26th EACSL Annual Conference on Computer Science Logic, CSL 2017, August 20-24, 2017, Stockholm, Sweden. LIPIcs 82, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik 2017, pages 11:1-11:20

Abstract

The finite satisfiability problem for the two-variable fragment of first-order logic interpreted over trees was recently shown to be ExpSpace-complete. We consider two extensions of this logic. We show that adding either additional binary symbols or counting quantifiers to the logic does not affect the complexity of the finite satisfiability problem. However, combining the two extensions and adding both binary symbols and counting quantifiers leads to an explosion of this complexity. We also compare the expressive power of the two-variable fragment over trees with its extension with counting quantifiers. It turns out that the two logics are equally expressive, although counting quantifiers do add expressive power in the restricted case of unordered trees.

On One Variable Fragment of First Order Logic with Modulo Counting Quantifier

Bartosz Bednarczyk
Conference Papers Proceedings of ESSLLI 2017 Student Session, 29th European Summer School in Logic, Language & Information, July 17-28, 2017, Toulouse, France, pages 7-13

Abstract

We consider the one-variable fragment of first-order logic extended with modulo counting quantifiers. We prove NPTime-completeness of such fragment by presenting an optimal algorithm for solving its finite satisfiability problem.

Satisfiability of the Two-Variable Fragment of First-Order Logic with counting quantifiers over finite trees

Bartosz Bednarczyk
Bachelor Thesis Dissertation advisor: prof. dr hab. Witold Charatonik, Date of defence: Feb. 15, 2017

Abstract

The finite satisfiability problem for the two-variable fragment of first-order logic interpreted over trees was recently shown to be ExpSpace-complete. We show that adding counting quantifiers to the logic does not affect the complexity of the finite satisfiability problem.