Showing 1–18 of 18 results for author: Bednarczyk, B

Data Complexity in Expressive Description Logics With Path Expressions

Authors: Bartosz Bednarczyk

Abstract: We investigate the data complexity of the satisfiability problem for the very expressive description logic ZOIQ (a.k.a. ALCHb Self reg OIQ) over quasi-forests and establish its NP-completeness. This completes the data complexity landscape for decidable fragments of ZOIQ, and reproves known results on decidable fragments of OWL2 (SR family). Using the same technique, we establish coNEXPTIME-complet… ▽ More We investigate the data complexity of the satisfiability problem for the very expressive description logic ZOIQ (a.k.a. ALCHb Self reg OIQ) over quasi-forests and establish its NP-completeness. This completes the data complexity landscape for decidable fragments of ZOIQ, and reproves known results on decidable fragments of OWL2 (SR family). Using the same technique, we establish coNEXPTIME-completeness (w.r.t. the combined complexity) of the entailment problem of rooted queries in ZIQ. △ Less

Submitted 11 June, 2024; originally announced June 2024.

Comments: Accepted to IJCAI 2024. A version with the appendix will appear soon

Exploring Non-Regular Extensions of Propositional Dynamic Logic with Description-Logics Features

Authors: Bartosz Bednarczyk

Abstract: We investigate the impact of non-regular path expressions on the decidability of satisfiability checking and querying in description logics extending ALC. Our primary objects of interest are ALCreg and ALCvpl, the extensions of with path expressions employing, respectively, regular and visibly-pushdown languages. The first one, ALCreg, is a notational variant of the well-known Propositional Dynami… ▽ More We investigate the impact of non-regular path expressions on the decidability of satisfiability checking and querying in description logics extending ALC. Our primary objects of interest are ALCreg and ALCvpl, the extensions of with path expressions employing, respectively, regular and visibly-pushdown languages. The first one, ALCreg, is a notational variant of the well-known Propositional Dynamic Logic of Fischer and Ladner. The second one, ALCvpl, was introduced and investigated by Loding and Serre in 2007. The logic ALCvpl generalises many known decidable non-regular extensions of ALCreg. We provide a series of undecidability results. First, we show that decidability of the concept satisfiability problem for ALCvpl is lost upon adding the seemingly innocent Self operator. Second, we establish undecidability for the concept satisfiability problem for ALCvpl extended with nominals. Interestingly, our undecidability proof relies only on one single non-regular (visibly-pushdown) language, namely on r#s# := { r^n s^n | n in N } for fixed role names r and s. Finally, in contrast to the classical database setting, we establish undecidability of query entailment for queries involving non-regular atoms from r#s#, already in the case of ALC-TBoxes. △ Less

Submitted 13 May, 2024; v1 submitted 19 July, 2023; originally announced July 2023.

On the Limits of Decision: the Adjacent Fragment of First-Order Logic

Authors: Bartosz Bednarczyk, Daumantas Kojelis, Ian Pratt-Hartmann

Abstract: We define the adjacent fragment AF of first-order logic, obtained by restricting the sequences of variables occurring as arguments in atomic formulas. The adjacent fragment generalizes (after a routine renaming) two-variable logic as well as the fluted fragment. We show that the adjacent fragment has the finite model property, and that its satisfiability problem is no harder than for the fluted fr… ▽ More We define the adjacent fragment AF of first-order logic, obtained by restricting the sequences of variables occurring as arguments in atomic formulas. The adjacent fragment generalizes (after a routine renaming) two-variable logic as well as the fluted fragment. We show that the adjacent fragment has the finite model property, and that its satisfiability problem is no harder than for the fluted fragment (and hence is Tower-complete). We further show that any relaxation of the adjacency condition on the allowed order of variables in argument sequences yields a logic whose satisfiability and finite satisfiability problems are undecidable. Finally, we study the effect of the adjacency requirement on the well-known guarded fragment (GF) of first-order logic. We show that the satisfiability problem for the guarded adjacent fragment (GA) remains 2ExpTime-hard, thus strengthening the known lower bound for GF. △ Less

Submitted 15 June, 2023; v1 submitted 4 May, 2023; originally announced May 2023.

Comments: Full version of our ICALP 2023 paper

About the Expressive Power and Complexity of Order-Invariance with Two Variables

Authors: Bartosz Bednarczyk, Julien Grange

Abstract: Order-invariant first-order logic is an extension of first-order logic (FO) where formulae can make use of a linear order on the structures, under the proviso that they are order-invariant, i.e. that their truth value is the same for all linear orders. We continue the study of the two-variable fragment of order-invariant first-order logic initiated by Zeume and Harwath, and study its complexity an… ▽ More Order-invariant first-order logic is an extension of first-order logic (FO) where formulae can make use of a linear order on the structures, under the proviso that they are order-invariant, i.e. that their truth value is the same for all linear orders. We continue the study of the two-variable fragment of order-invariant first-order logic initiated by Zeume and Harwath, and study its complexity and expressive power. We first establish coNExpTime-completeness for the problem of deciding if a given two-variable formula is order-invariant, which tightens and significantly simplifies the coN2ExpTime proof by Zeume and Harwath. Second, we address the question of whether every property expressible in order-invariant two-variable logic is also expressible in first-order logic without the use of a linear order. While we were not able to provide a satisfactory answer to the question, we suspect that the answer is ``no''. To justify our claim, we present a class of finite tree-like structures (of unbounded degree) in which a relaxed variant of order-invariant two-variable FO expresses properties that are not definable in plain FO. On the other hand, we show that if one restricts their attention to classes of structures of bounded degree, then the expressive power of order-invariant two-variable FO is contained within FO. △ Less

Submitted 12 February, 2024; v1 submitted 17 April, 2023; originally announced April 2023.

Comments: arXiv admin note: substantial text overlap with arXiv:2207.04986

Order-Invariance of Two-Variable Logic is coNExpTime-complete

Authors: Bartosz Bednarczyk

Abstract: We establish coNExpTime-completeness of the problem of deciding order-invariance of a given two variable first-order formula, improving and significantly simplifying coTwoNExpTime bound by Zeume and Harwath. We establish coNExpTime-completeness of the problem of deciding order-invariance of a given two variable first-order formula, improving and significantly simplifying coTwoNExpTime bound by Zeume and Harwath. △ Less

Submitted 16 August, 2022; originally announced August 2022.

Towards a Model Theory of Ordered Logics: Expressivity and Interpolation (Extended version)

Authors: Bartosz Bednarczyk, Reijo Jaakkola

Abstract: We consider the family of guarded and unguarded ordered logics, that constitute a recently rediscovered family of decidable fragments of first-order logic (FO), in which the order of quantification of variables coincides with the order in which those variables appear as arguments of predicates. While the complexities of their satisfiability problems are now well-established, their model theory,… ▽ More We consider the family of guarded and unguarded ordered logics, that constitute a recently rediscovered family of decidable fragments of first-order logic (FO), in which the order of quantification of variables coincides with the order in which those variables appear as arguments of predicates. While the complexities of their satisfiability problems are now well-established, their model theory, however, is poorly understood. Our paper aims to provide some insight into it. We start by providing suitable notions of bisimulation for ordered logics. We next employ bisimulations to compare the relative expressive power of ordered logics, and to characterise our logics as bisimulation-invariant fragments of FO a la van Benthem. Afterwards, we study the Craig Interpolation Property~(CIP). We refute yet another claim from the infamous work by Purdy, by showing that the fluted and forward fragments do not enjoy CIP. We complement this result by showing that the ordered fragment and the guarded ordered logics enjoy CIP. These positive results rely on novel and quite intricate model constructions, which take full advantage of the "forwardness" of our logics. △ Less

Submitted 23 June, 2022; originally announced June 2022.

Comments: Accepted to the 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)

Lutz's Spoiler Technique Revisited: A Unified Approach to Worst-Case Optimal Entailment of Unions of Conjunctive Queries in Locally-Forward Description Logics

Authors: Bartosz Bednarczyk

Abstract: We present a unified approach to (both finite and unrestricted) worst-case optimal entailment of (unions of) conjunctive queries (U)CQs in the wide class of "locally-forward" description logics. The main technique that we employ is a generalisation of Lutz's spoiler technique, originally developed for CQ entailment in ALCHQ. Our result closes numerous gaps present in the literature, most notably i… ▽ More We present a unified approach to (both finite and unrestricted) worst-case optimal entailment of (unions of) conjunctive queries (U)CQs in the wide class of "locally-forward" description logics. The main technique that we employ is a generalisation of Lutz's spoiler technique, originally developed for CQ entailment in ALCHQ. Our result closes numerous gaps present in the literature, most notably implying ExpTime-completeness of (U)CQ-querying for any superlogic of ALC contained in ALCHbregQ, and, as we believe, is abstract enough to be employed as a black-box in many new scenarios. △ Less

Submitted 12 August, 2021; originally announced August 2021.

On Classical Decidable Logics extended with Percentage Quantifiers and Arithmetics

Authors: Bartosz Bednarczyk, Maja Orłowska, Anna Pacanowska, Tony Tan

Abstract: During the last decades, a lot of effort was put into identifying decidable fragments of first-order logic. Such efforts gave birth, among the others, to the two-variable fragment and the guarded fragment, depending on the type of restriction imposed on formulae from the language. Despite the success of the mentioned logics in areas like formal verification and knowledge representation, such first… ▽ More During the last decades, a lot of effort was put into identifying decidable fragments of first-order logic. Such efforts gave birth, among the others, to the two-variable fragment and the guarded fragment, depending on the type of restriction imposed on formulae from the language. Despite the success of the mentioned logics in areas like formal verification and knowledge representation, such first-order fragments are too weak to express even the simplest statistical constraints, required for modelling of influence networks or in statistical reasoning. In this work we investigate the extensions of these classical decidable logics with percentage quantifiers, specifying how frequently a formula is satisfied in the indented model. We show, surprisingly, that all the mentioned decidable fragments become undecidable under such extension, sharpening the existing results in the literature. Our negative results are supplemented by decidability of the two-variable guarded fragment with even more expressive counting, namely Presburger constraints. Our results can be applied to infer decidability of various modal and description logics, e.g. Presburger Modal Logics with Converse or ALCI, with expressive cardinality constraints. △ Less

Submitted 3 October, 2021; v1 submitted 29 June, 2021; originally announced June 2021.

Comments: To appear in FSTTCS 2021

The Price of Selfishness: Conjunctive Query Entailment for ALCSelf is 2ExpTime-hard

Authors: Bartosz Bednarczyk, Sebastian Rudolph

Abstract: In logic-based knowledge representation, query answering has essentially replaced mere satisfiability checking as the inferencing problem of primary interest. For knowledge bases in the basic description logic ALC, the computational complexity of conjunctive query (CQ) answering is well known to be ExpTime-complete and hence not harder than satisfiability. This does not change when the logic is ex… ▽ More In logic-based knowledge representation, query answering has essentially replaced mere satisfiability checking as the inferencing problem of primary interest. For knowledge bases in the basic description logic ALC, the computational complexity of conjunctive query (CQ) answering is well known to be ExpTime-complete and hence not harder than satisfiability. This does not change when the logic is extended by certain features (such as counting or role hierarchies), whereas adding others (inverses, nominals or transitivity together with role-hierarchies) turns CQ answering exponentially harder. We contribute to this line of results by showing the surprising fact that even extending ALC by just the Self operator - which proved innocuous in many other contexts - increases the complexity of CQ entailment to 2ExpTime. As common for this type of problem, our proof establishes a reduction from alternating Turing machines running in exponential space, but several novel ideas and encoding tricks are required to make the approach work in that specific, restricted setting. △ Less

Submitted 15 August, 2021; v1 submitted 29 June, 2021; originally announced June 2021.

Comments: Minor stylistic improvements comparing to the 1st version

Why Does Propositional Quantification Make Modal and Temporal Logics on Trees Robustly Hard?

Authors: Bartosz Bednarczyk, Stéphane Demri

Abstract: Adding propositional quantification to the modal logics K, T or S4 is known to lead to undecidability but CTL with propositional quantification under the tree semantics (tQCTL) admits a non-elementary Tower-complete satisfiability problem. We investigate the complexity of strict fragments of tQCTL as well as of the modal logic K with propositional quantification under the tree semantics. More spec… ▽ More Adding propositional quantification to the modal logics K, T or S4 is known to lead to undecidability but CTL with propositional quantification under the tree semantics (tQCTL) admits a non-elementary Tower-complete satisfiability problem. We investigate the complexity of strict fragments of tQCTL as well as of the modal logic K with propositional quantification under the tree semantics. More specifically, we show that tQCTL restricted to the temporal operator EX is already Tower-hard, which is unexpected as EX can only enforce local properties. When tQCTL 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 consequences of our proof method, we prove Tower-hardness of tQCTL restricted to EF or to EXEF and of the well-known modal logics such as K, KD, GL, K4 and S4 with propositional quantification under a semantics based on classes of trees. △ Less

Submitted 4 August, 2022; v1 submitted 27 April, 2021; originally announced April 2021.

Journal ref: Logical Methods in Computer Science, Volume 18, Issue 3 (July 28, 2022) lmcs:7409

Modal Logics with Composition on Finite Forests: Expressivity and Complexity (Extra Material)

Authors: Bartosz Bednarczyk, Stéphane Demri, Raul Fervari, Alessio Mansutti

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(|) i… ▽ More 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. △ Less

Submitted 16 July, 2020; originally announced July 2020.

Comments: Extra material for our LICS 2020 paper published under the same title

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

Authors: Bartosz Bednarczyk, Jakub Michaliszyn

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 pas… ▽ More 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. △ Less

Submitted 3 January, 2021; v1 submitted 2 July, 2020; originally announced July 2020.

Comments: Full version of FOSSACS 2021 paper

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

Authors: Franz Baader, Bartosz Bednarczyk, Sebastian Rudolph

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. On the one hand, we prove that this does not increase the complexity of satisfiability checking and other standard inference problems. On the other hand, the satisfiability problem becomes undecidable if inverse roles are add… ▽ More 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. On the one hand, we prove that this does not increase the complexity of satisfiability checking and other standard inference problems. On the other hand, the satisfiability problem becomes undecidable if inverse roles are added to the languages. In addition, even without inverse roles, 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. The latter result is based on a locally-acyclic model construction, and it reduces query entailment to ABox consistency in the restricted setting, i.e., to ABox consistency w.r.t. restricted cardinality constraints in ALCSCC, for which we can show an ExpTime upper bound. △ Less

Submitted 14 February, 2020; originally announced February 2020.

Comments: Technical report for the paper of the same title accepted to ECAI 2020

Statistical EL is ExpTime-complete

Authors: Bartosz Bednarczyk

Abstract: We show that the consistency problem for Statistical EL ontologies, defined by Pe{ñ}aloza and Potyka, 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. We show that the consistency problem for Statistical EL ontologies, defined by Pe{ñ}aloza and Potyka, 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. △ Less

Submitted 5 March, 2021; v1 submitted 2 November, 2019; originally announced November 2019.

Comments: Major revision of the previous version, extra lemma provided, a few grammar corrections. Under submission to IPL

Completing the Picture: Complexity of Graded Modal Logics with Converse

Authors: Bartosz Bednarczyk, Emanuel Kieroński, Piotr Witkowski

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… ▽ More 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. △ Less

Submitted 4 March, 2021; v1 submitted 11 December, 2018; originally announced December 2018.

Comments: This is an extended version of our JELIA 2019 paper, under consideration in Theory and Practice of Logic Programming (TPLP)

ACM Class: F.4.1; I.2.4

Journal ref: Theory and Practice of Logic Programming 21 (2021) 493-520

One-Variable Logic Meets Presburger Arithmetic

Authors: Bartosz Bednarczyk

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 prob… ▽ More 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. △ Less

Submitted 16 September, 2019; v1 submitted 25 October, 2018; originally announced October 2018.

Comments: A short note accepted to TCS

Modulo Counting on Words and Trees

Authors: Bartosz Bednarczyk, Witold Charatonik

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 2EX… ▽ More 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. △ Less

Submitted 16 October, 2017; originally announced October 2017.

Comments: Full version of a paper published in proceedings of FSTTCS 2017 conference

Extending Two-Variable Logic on Trees

Authors: Bartosz Bednarczyk, Witold Charatonik, Emanuel Kieroński

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 addin… ▽ More 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. △ Less

Submitted 24 November, 2016; v1 submitted 7 November, 2016; originally announced November 2016.