Filter by type:

Sort by year

Completing the Picture: Complexity of Graded Modal Logics with Converse

Bartosz Bednarczyk, Emanuel Kieroński, Piotr Witkowski
Journal Papers Theory and Practice of Logic Programming

Abstract

A complete classification of the complexity of the local and global satisfiability problems for graded modal language over traditional classes of frames have 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.

Statistical EL is ExpTime-complete

Bartosz Bednarczyk
Journal Papers Information Processing Letters

Abstract

We show that the consistency problem for Statistical EL ontologies, defined by Penaloza and Potyka in SUM 2017, is ExpTime-hard. Together with existing ExpTime upper bounds, we conclude ExpTime-completeness of the logic. Our proof goes via a reduction from the consistency problem for EL extended with negation of atomic concepts.

Exploiting forwardness: Satisfiability and Query-Entailment in Forward Guarded Fragment

Bartosz Bednarczyk
Conference Papers [Best student paper award] Proceedings of the 17th Edition of the European Conference on Logics in Artificial Intelligence (JELIA 2021)

Abstract

We study the complexity of two standard reasoning problems for Forward Guarded Logic (FGF), obtained as a restriction of the Guarded Fragment in which variables appear in atoms only in the order of their quantification. We show that FGF enjoys the higher-arity-forest- model property, which results in ExpTime-completeness of its (finite and unrestricted) knowledge-base satisfiability problem. Moreover, we show that FGF is well-suited for knowledge representation. By employing a generalisation of Lutz’s spoiler technique, we prove that the conjunctive query entailment problem for FGF remains in ExpTime. We find that our results are quite unusual as FGF is, up to our knowledge, the first decidable fragment of First-Order Logic, extending standard description logics like ALC, that offers unboundedly many variables and higher-arity relations while keeping its complexity surprisingly low.

"Most of" leads to undecidability: Failure of adding frequencies to LTL

Bartosz Bednarczyk, Jakub Michaliszyn
Conference Papers Proceedings of the 24th International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2021).

Abstract

Linear Temporal Logic (LTL) interpreted on finite traces is a robust specification framework popular in formal verification. However, despite the high interest in the logic in recent years, the topic of their quantitative extensions is not yet fully explored. The main goal of this work is to study the effect of adding weak forms of percentage constraints (e.g. that most of the positions in the past satisfy a given condition, or that sigma is the most-frequent letter occurring in the past) to fragments of LTL. Such extensions could potentially be used for the verification of influence networks or statistical reasoning. Unfortunately, as we prove in the paper, it turns out that percentage extensions of even tiny fragments of LTL have undecidable satisfiability and model-checking problems. Our undecidability proofs not only sharpen most of the undecidability results on logics with arithmetics interpreted on words known from the literature, but also are fairly simple. We also show that the undecidability can be avoided by restricting the allowed usage of the negation, and briefly discuss how the undecidability results transfer to first-order logic on words.

A note on C2 interpreted over finite data-words

Bartosz Bednarczyk, Piotr Witkowski
Conference Papers Proceedings of the 27th International Symposium on Temporal Representation and Reasoning (TIME 2020).

Abstract

We consider the satisfiability problem for the two-variable fragment of first-order logic extended with counting quantifiers, interpreted over finite words with data, denoted here with C2[≤,succ,∼,πbin]. In our scenario, we allow for using arbitrary many uninterpreted binary predicates from ,πbin, two navigational predicates ≤ and succ over word positions as well as a data-equality predicate ~. We prove that the obtained logic is undecidable, which contrasts with the decidability of the logic without counting by Montanari, Pazzaglia and Sala [MontanariPS16]. We supplement our results with decidability for several sub-fragments of C2[≤,succ,∼,πbin], e.g., without binary predicates, without successor succ, or under the assumption that the total number of positions carrying the same data value in a data-word is bounded by an a priori given constant.

All-Instances Oblivious Chase Termination is Undecidable for Single-Head Binary TGDs

Bartosz Bednarczyk, Robert Ferens, Piotr Ostropolski-Nalewaja
Conference Papers Proceedings of the 29th International Joint Conference on Artificial Intelligence and the 17th Pacific Rim International Conference on Artificial Intelligence (IJCAI 2020).

Abstract

The chase is a famous algorithmic procedure in database theory with numerous applications in ontology-mediated query answering. We consider static analysis of the chase termination problem, which asks, given set of TGDs, whether the chase terminates on all input databases. The problem was recently shown to be undecidable by Gogacz et al. for sets of rules containing only ternary predicates. In this work, we show that undecidability occurs already for sets of single-head TGD over binary vocabularies. This question is relevant since many real-world ontologies, e.g., those from the Horn fragment of the popular OWL, are of this shape.

A Framework for Reasoning about Dynamic Axioms in Description Logics

Bartosz Bednarczyk, Stephane Demri, Alessio Mansutti
Conference Papers Proceedings of the 29th International Joint Conference on Artificial Intelligence and the 17th Pacific Rim International Conference on Artificial Intelligence (IJCAI 2020).

Abstract

Description logics are well-known logical formalisms for knowledge representation. We propose to enrich knowledge bases (KBs) with dynamic axioms that specify how the satisfaction of statements from the KBs evolves when the interpretation is decomposed or recomposed, providing a natural means to predict the evolution of interpretations. Our dynamic axioms borrow logical connectives from separation logics, well-known specification languages to verify programs with dynamic data structures. In the paper, we focus on ALC and EL augmented with dynamic axioms, or to their subclass of positive dynamic axioms. The knowledge base consistency problem in the presence of dynamic axioms is investigated, leading to interesting complexity results, among which the problem for EL with positive dynamic axioms is tractable, whereas EL with dynamic axioms is undecidable.

Modal Logics with Composition on Finite Forests: Expressivity and Complexity

Bartosz Bednarczyk, Stephane Demri, Raul Fervari, Alessio Mansutti
Conference Papers Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2020

Abstract

We investigate the expressivity and computational complexity of two modal logics on finite forests equipped with operators to reason on submodels. The logic ML(|) extends the basic modal logic ML with the composition operator | from static ambient logic, whereas ML(∗) contains the separating conjunction ∗ from separation logic. Though both operators are second-order in nature, we show that ML(|) is as expressive as the graded modal logic GML (on finite trees) whereas ML(∗) lies strictly between ML and GML. Moreover, we establish that the satisfiability problem for ML(∗) is Tower-complete, whereas for ML(|) is (only) AExpPol-complete.As a by-product, we solve several open problems related to sister logics, such as static ambient logic, modal separation logic, and second-order modal logic on finite trees.s

Satisfiability and Query Answering in Description Logics with Global and Local Cardinality Constraints

Franz Baader, Bartosz Bednarczyk, Sebastian Rudolph
Conference Papers Proceedings of the 24th European Conference on Artificial Intelligence (ECAI 2020).

Abstract

Abstract. We introduce and investigate the expressive description logic (DL) ALCSCC++, in which the global and local cardinality constraints introduced in previous papers can be mixed. We prove that the added expressivity does not increase the complexity of satisfiability checking and other standard inference problems. However, reasoning in ALCSCC++ becomes undecidable if inverse roles are added or conjunctive query entailment is considered. We prove that decidability of querying can be regained if global and local constraints are not mixed and the global constraints are appropriately restricted. In this setting, query entailment can be shown to be EXPTIME-complete and hence not harder than reasoning in ALC.

One-Variable Logic Meets Presburger Arithmetic

Bartosz Bednarczyk
Journal Papers Theoretical Computer Science

Abstract

We consider the one-variable fragment of first-order logic extended with Presburger constraints. The logic is designed in such a way that it subsumes the previously-known fragments extended with counting, modulo counting or cardinality comparison and combines their expressive powers. We prove NP-completeness of the logic by presenting an optimal algorithm for solving its finite satisfiability problem.

Worst-Case Optimal Querying of Very Expressive Description Logics with Path Expressions and Succinct Counting

Bartosz Bednarczyk, Sebastian Rudolph
Conference Papers Proceedings of the 28th International Joint Conference on Artificial Intelligence, IJCAI 2019

Abstract

Among the most expressive knowledge representation formalisms are the description logics of the Z family. For well-behaved fragments of ZOIQ, entailment of positive two-way regular path queries is well known to be 2EXPTIMEcomplete under the proviso of unary encoding of numbers in cardinality constraints. We show that this assumption can be dropped without an increase in complexity and EXPTIME-completeness can be achieved when bounding the number of query atoms, using a novel reduction from query entailment to knowledge base satisfiability. These findings allow to strengthen other results regarding query entailment and query containment problems in very expressive description logics. Our results also carry over to GC2 , the two-variable guarded fragment of firstorder logic with counting quantifiers, for which hitherto only conjunctive query entailment has been investigated.

Worst-Case Optimal Querying of Very Expressive Description Logics with Path Expressions and Succinct Counting

Bartosz Bednarczyk, Sebastian Rudolph
Workshop Papers Description Logics Workshop 2019

Abstract

Among the most expressive knowledge representation formalisms are the description logics of the Z family. For well-behaved fragments of ZOIQ, entailment of positive two-way regular path queries is well known to be 2EXPTIMEcomplete under the proviso of unary encoding of numbers in cardinality constraints. We show that this assumption can be dropped without an increase in complexity and EXPTIME-completeness can be achieved when bounding the number of query atoms, using a novel reduction from query entailment to knowledge base satisfiability. These findings allow to strengthen other results regarding query entailment and query containment problems in very expressive description logics. Our results also carry over to GC2 , the two-variable guarded fragment of firstorder logic with counting quantifiers, for which hitherto only conjunctive query entailment has been investigated.

Satisfiability Checking and Conjunctive Query Answering in Description Logics with Global and Local Cardinality Constraints

Franz Baader, Bartosz Bednarczyk, Sebastian Rudolph
Workshop Papers Description Logics Workshop 2019

Abstract

We consider an expressive description logic (DL) in which the global and local cardinality constraints introduced in previous papers can be mixed. On the one hand, we show that this does not increase the complexity of satisfiability checking and other standard inference problems. On the other hand, conjunctive query entailment in this DL turns out to be undecidable. We prove that decidability of querying can be regained if global and local constraints are not mixed and the global constraints are appropriately restricted.

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.