Guarded Fragments Meet Dynamic Logic: The Story of Regular Guards (Extended Abstract)

Abstract

The Guarded Fragment (GF) of first-order logic ( FO), introduced by Andréka et al. [1], generalizes modal and description logics (DLs) to higher-arity relational vocabularies. Over the past 25 years, GF has become the canonical first-order fragment that balances expressive power with attractive model-theoretic properties, such as the finite model property [ 2], preservation theorems [3], and robust decidability under various extensions involving fixed-point operators [ 4] or query languages [5]. Since classical (polyadic) multi-modal and description logic formulae embed naturally into GF via standard translations, this fragment serves as a versatile logical framework central to both theoretical studies and applications in KR and databases. However, not all widely-used families of modal and description logics (DLs) are expressible within the scope of GF, as it cannot express properties such as transitivity or equivalence of relations. Consequently, translating transitive description logics like those from the family of DLs or modal logics interpreted over equivalence frames including S5, into the guarded fragment is not directly possible. To overcome this limitation, Ganzinger et al. [6] initiated the study of semantically-constrained guards, an extension of GF allowing certain relations-confined to guards-to be interpreted with additional semantic constraints, notably transitivity or equivalence. This direction spurred intensive research, yielding several positive results, notably the 2ExpTime-completeness of GF extended with (conjunctions of) transitive guards (consult the works of Szwast&Tendera [7], Kazakov [8] and Kieroński&Rudolph [9]), as well as the two-variable fragment of GF augmented by transitive or equivalence closures of binary guards, established by Michaliszyn and his co-authors [10, 11]. Check Tendera's survey [12] for a comprehensive overview. On the negative side, natural extensions of GF with equality (GF≈ ), intended to capture popular description logics from the ℛ family, turned out to be undecidable. Examples include GF≈ with exponentiation (regular expressions that are compositions of the same letter) [13] or associative compositional axioms [8]. The decidability status of these logics without equality ≈ is still open. Consequently, there is no known decidable extension of GF with semantically-constrained guards captures propositional dynamic logic (PDL) and its generalizations such as the family [14] of DLs, PDL with intersection and converse (ICPDL) [15], or its higher-arity extensions of DLs like ℒℛ [16].

1. Introduction

2. Our Contributions

We introduce and study a novel logic called RGF, which extends (equality- and constant-free) GF by allowing ICPDL-programs as guards (cf. Def. 1). Our main result establishes that Sat(RGF) is 2ExpTime-complete, matching the complexity of plain GF and ICPDL. This also lifts decidability to several logics where it was previously known only in their two-variable case. Our proof employs a fusion technique, reducing Sat(RGF) to instances of the satisfiability problem in plain GF or two-variable RGF, which is in turn solvable via an encoding to ICPDL.

Theorem 1. The satisfiability problem for RGF is 2ExpTime-complete. ◀

We further address two questions: (i) Is the query entailment problem decidable for RGF? (ii) Is there an expressive fragment of RGF of complexity lower than 2ExpTime? We answer question (i) negatively, showing undecidability of conjunctive query entailment even for two-variable fluted GF with a single transitive guard, substantially strengthening prior results of Gottlob et al. [17, Thm. 1] on entailment of unions of conjunctive queries over GF2 with transitive guards in three ways: our logic is more restricted (belongs to the so-called fluted fragment), our queries do not use disjunction (we use conjunctive queries rather than the unions thereof), and our proof is also applicable to the finite-model scenario (which remained open).

Theorem 2. Both finite and general CQ entailment problems are undecidable for RGF, already for its lfuted two-variable fragment with a single transitive guard. ◀

By fluted formulae we mean index-normal formulae (on any branch of its syntax tree, the -th quantifier bounds precisely ) where any atom (¯) in the scope of a quantifier bounding (but not +1), the sequence ¯ is a sufix of the sequence 1, 2, . . . , . Our undecidability transfers to ℒ extended with unqualified existential restrictions with intersection of the form ∃(r ∩ s).⊤, inclusion axioms of the form r ⊆ s ∪ t, and a single transitivity statement.

For (ii) we conduct a thorough case analysis, pinpointing when subfragments of RGF admit lower complexity than 2ExpTime. We conclude that a novel forward variant of GF extended with transitive closure is the largest (in a natural sense) ExpSpace-complete fragment of RGF.

Theorem 3 (Simplified statement) . The satisfiability problem for the forward subfragment RGF with the set of operators restricted to {· +, · * , ?} is ExpSpace-complete. The inclusion of other operators makes already the fluted two-variable fragment of RGF 2ExpTime-hard. ◀

3. Our Motivations

We explain our motivations behind the study of the GF with regular guards in the form of a Q&A. ¬ Why the guarded fragment (GF)? Because GF is the canonical extension of modal and description logics to the setting of higher-arity relations [18], heavily investigated in the last 25 years. GF is not only well-behaved both computationally [ 2 ] and model-theoretically [19], but is also robust under extensions like fixed points [ 4 ] or semanticallyconstrained guards [12]. It was studied also in the setting of knowledge representation in multiple recent papers [20, 21, 22, 23, 24]. ¬ Do we generalize any previously studied logics? Yes, many of them. First, as GF encodes (via the standard translation, see e.g. Section 2.6.1 of Baader’s textbook 2017) multi-modal and description logics [18], our logic also encodes (via an analogous translation) ICPDL and its subfragments such as ℒreg or ℛℐ (Horrocks et al. 2006). There also exists a natural translation from (counting-free fragment of) ℒℛreg (Calvanese et al. 2008) to RGF. Second, there is a long tradition of studying GF extended with semantically-constrained guards [12], i.e. distinguished relations (available only as guards) interpreted as transitive (Ganzinger et al. 1999) or equivalence [27] relations, or as transitive [ 10 ] or equivalence (Kieroński et al. 2017) closures of another relation (that may also appear only as a guard). As one can simulate transitive or equivalence relation R with S+ and (S ∪ S− )* for a fresh relation S, our logic strictly extends all of the mentioned logics. Moreover, the mentioned papers concerning transitive and equivalence closures only focused on the extensions of GF2 (two-variable GF), and hence our logic lifts them (without ≈ ) to the case of full GF and provides the tight complexity bound. Other ideas concern GF with exponentiation (regular expressions that are composition of the same letter) [13] or associative compositional axioms [ 8 ] (i.e. axioms R ∘ S ⊆ T where R, S, T occurring only in guards). Both of them can be easily simulated in our framework. Finally, GF with conjunctions of transitive relations in guards [ 8 ] can be expressed in RGF by employing ∩ operator. All of this makes RGF a desirable object of study. ¬ Are there any closely related but incomparable logics? The closest logic is the Unary Negation Fragment [28] with regular-path expressions [29] UNreg, together with its very recent generalizations with transitive closure operators [30] and guarded negation [31]. All of these logics share 2ExpTime complexity of their (formula) satisfiability problem, but their expressive powers are incomparable. Indeed, RGF is not able to express conjunctive queries, while the other logics cannot express that R* -reachable elements are B-connected. Yet another related logic is GNFPup by Benedikt et al. 2016, which extends the guarded (negation) fragment [33] with fixed-point operators with unguarded parameters. The syntax of GNFPup is complicated, but the logic seems to embed ICPDL. Unfortunately, according to our understanding, such an encoding leads to a non-constant “pdepth” of the resulting formulae, leading to a non-elementary fragment of the logic. The expressive powers of GNFPup and RGF are again incomparable and the separating examples are as before.

4. Our Logic

we define both RGF-programs and RGF-formulae.

We work with structures over a fixed countably-infinite equality- and constant-free relational signature Σ := ΣFO ∪· ΣR , where all predicates in ΣR , called regular predicates, are binary. By mutual induction, Definition 1 (RGF). RGF-programs are given by the grammar: , ::= B | B¯ | ∘ | ∪ | ∩ | * | + | ?, where B ∈ ΣR and is an RGF-formula with a sole free variable. An RGF-guard for a formula is either an atom over ΣFO or () for some RGF-program , such that free variables of include all free variables of . The set RGF of RGF-formulae is defined with the grammar:

, ′ ::= A(¯) | ¬ | ∧ ′ | ∃ () | ∃¯( ∧ ), where A ∈ ΣFO and is an RGF-guard for . The semantics of RGF-programs is:

Name Test / Predicate Converse operator Concatenation Kleene star/plus Union / Intersection ∪ / ∩

* / + Syntax of ? / B

¯ ∘

Semantics A of in a structure A {(a, a) | A |= [a]} / Binary relation

{(b, a) | (a, b) ∈ A} {(a, c) | ∃b.(a, b) ∈ A ∧ (b, c) ∈ A

} where 0 := ⊤? and +1 := ( ) ∘ .

A

∪ A / A ⋃︀∞=0( )A / ⋃︀∞ =1

∩ A ( )A, ◀

Why are constant symbols excluded from Σ? ¬ ¬ Our logic generalizes a plethora of extensions of GF with semantically-constrained guards (consult transitive guards, is a fragment of RGF. We explain our design choices. the introduction). For instance, transitive and equivalence relations in guards can be simulated in RGF using R+ and (R ∪ R¯ )* for a fresh binary relation R. Hence, GF+TG, the extension of GF with ¬ Why is the signature separated, i.e. Σ := ΣFO ∪· ΣR ? To ensure that binary predicates from ΣR appear only in guards; otherwise, even the two-variable guarded fragment with transitivity is undecidable [6, Th. 2].

Why is the equality symbol ≈

excluded from Σ? Its inclusion makes our logic undecidable, already for GF2 with compositional axioms [8, Th. 5.3.1], conjunctions of transitive guards [8, Th. 5.3.2], or exponentiation [13, Th. 3.1].

They are expected to preserve decidability, especially given that the key theorem of 2ExpTimecompleteness of ICPDL [34, Th. 3.28] extends to Hybrid ICPDL.

5. Future Work

Future work may proceed along two directions. One promising path is to extend the ICPDL-based guards to more expressive formalisms, such as linear Datalog or non-binary transitive closure operators. This would help eliminate the asymmetry between the binary nature of regular guards and the higher-arity relations allowed in GF. The alternative path is to tackle the finite satisfiability problem for RGF. This problem is very challenging—even for minimal fragments of ICPDL like LoopPDL—and has resisted resolution for over 40 years, indicating that significant breakthroughs and new techniques will be required. A more pragmatic direction is to study fragments of RGF with the FMP (the finite model property). While formulae like ∀1∃2R(12) combined with either ¬∃1R+(11) or ∀12(R+(11) → B(12) ∧ ¬B(21)) destroy the FMP by enforcing infinite, non-loopable R-chains, one may hope that fluted RGF retains it. With similar counter-examples we show: Lemma 1. For the set of allowed operators Op being either {· +, ?}, {· +, · * }, {· +, ¯·}, or {· +, ∘} we have that the fluted RGF with the operators in programs restricted to these from Op does not have the finite model property. ◀ We can already prove that FRGF[· +] has the FMP and we are currently trying to extend our approach to FRGF[· +, ∩, ∪]. More details are coming soon!

Acknowledgements

This work was supported by NCN grants 2024/53/N/ST6/01390 (Bartosz Bednarczyk) and 2021/41/B/ST6/00996 (Emanuel Kieroński). This paper is an extended abstract of our paper recently accepted to KR 2025. Its extended version will be publicly available on arXiv soon.

Declaration on Generative AI

During the preparation of this work, the authors used GPT-4 and Grammarly in order to: Grammar and spelling check, Improve writing style, and Paraphrase and reword. After using these tools, the authors reviewed and edited the content as needed and take full responsibility for the publication’s content. [11] E. Kieroński, I. Pratt-Hartmann, L. Tendera, Equivalence Closure in the Two-Variable Guarded

Fragment, Journal of Logic and Computation 27 (2017) 999–1021. [12] L. Tendera, Finite Model Reasoning in Expressive Fragments of First-Order Logic, in: M4M at

ICLA, 2017. [13] J. Michaliszyn, Konstrukcje PDL w Logice ze Strażnikami, Master’s thesis, University of Wrocław, 2008. Available (in polish) at https://ii.uni.wroc.pl/~jmi/papers/magisterka.PDF. [14] D. Calvanese, T. Eiter, M. Ortiz, Regular Path Queries in Expressive Description Logics with

Nominals, in: C. Boutilier (Ed.), IJCAI, 2009. [15] S. Göller, M. Lohrey, C. Lutz, PDL with Intersection and Converse: Satisfiability and Infinite-State

Model Checking, Journal of Symbolic Logic 74 (2009) 279–314. [16] D. Calvanese, G. D. Giacomo, M. Lenzerini, Conjunctive Query Containment and Answering Under

Description Logic Constraints, ACM Transactions on Computational Logic 9 (2008) 22:1–22:31. [17] G. Gottlob, A. Pieris, L. Tendera, Querying the Guarded Fragment with Transitivity, in: ICALP, 2013. [18] E. Grädel, Description Logics and Guarded Fragments of First Order Logic, in: DL, 1998. [19] E. Grädel, M. Otto, The Freedoms of (Guarded) Bisimulation, in: Johan van Benthem on Logic and

Information Dynamics, Springer, 2014, pp. 3–31. [20] C. Lutz, Q. Manière, Adding Circumscription to Decidable Fragments of First-Order Logic: A

Complexity Rollercoaster, in: KR, 2024. [21] J. C. Jung, C. Lutz, H. Pulcini, F. Wolter, Separating Data Examples by Description Logic Concepts with Restricted Signatures, in: KR, 2021. [22] D. Figueira, S. Figueira, E. Pin Baque, Finite Controllability for Ontology-Mediated Query Answering of CRPQ, in: KR, 2020. [23] S. Zheng, R. Schmidt, Deciding the Loosely Guarded Fragment and Querying Its Horn Fragment

Using Resolution, in: AAAI, 2020. [24] P. Bourhis, M. Morak, A. Pieris, Making Cross Products and Guarded Ontology Languages

Compatible, in: IJCAI, 2017. [25] F. Baader, I. Horrocks, C. Lutz, U. Sattler, An Introduction to Description Logic, Cambridge

University Press, 2017. [26] I. Horrocks, O. Kutz, U. Sattler, The Even More Irresistible SROIQ, in: KR, 2006. [27] E. Kieroński, Results on the Guarded Fragment with Equivalence or Transitive Relations, in: CSL, 2005. [28] L. Segoufin, B. ten Cate, Unary Negation, Logical Methods in Computer Science 9 (2013). [29] J. C. Jung, C. Lutz, M. Martel, T. Schneider, Querying the Unary Negation Fragment with Regular

Path Expressions, in: ICDT, 2018. [30] D. Figueira, S. Figueira, A Common Ancestor of PDL, Conjunctive Queries, and Unary Negation

First-order, ArXiV (version 1) (2025). [31] Y. Nakamura, Guarded Negation Transitive Closure Logic is 2-EXPTIME-complete, ArXiV (version 2) (2025). [32] M. Benedikt, P. Bourhis, M. Vanden Boom, A Step Up in Expressiveness of Decidable Fixpoint

Logics, in: LICS, 2016. [33] V. Bárány, B. ten Cate, L. Segoufin, Guarded Negation, Journal of the ACM 62 (2015) 22:1–22:26. [34] S. Göller, Computational Complexity of Propositional Dynamic Logics, Ph.D. thesis, University of Leipzig, 2008. URL: http://www.lsv.fr/Publis/PAPERS/PDF/goeller-phd14.pdf.

References

[1] H. Andréka , I. Németi , J. van Benthem , Modal Languages and Bounded Fragments of Predicate Logic, Journal of Philosophical Logic 27 ( 1998 ) 217 - 274 .

[2] E. Grädel , On The Restraining Power of Guards, Journal of Symbolic Logic 64 ( 1999 ) 1719 - 1742 .

[3] M. Otto , Highly Acyclic Groups, Hypergraph Covers, and the Guarded Fragment , Journal of the ACM 59 ( 2012 ) 5: 1 - 5 : 40 .

[4] E. Grädel , I. Walukiewicz , Guarded Fixed Point Logic, in: LICS, 1999 .

[5] V. Bárány , G. Gottlob, M. Otto , Querying the Guarded Fragment, Logical Methods in Computer Science 10 ( 2014 ).

[6] H. Ganzinger , C. Meyer, M. Veanes, The Two-Variable Guarded Fragment with Transitive Relations , in: LICS, 1999 .

[7] W. Szwast , L. Tendera , The Guarded Fragment with Transitive Guards , Annals of Pure and Applied Logic 128 ( 2004 ) 227 - 276 .

[8] Y. Kazakov , Saturation-Based Decision Procedures For Extensions Of The Guarded Fragment , Ph.D. thesis, Universität des Saarlandes , 2006 .

[9] E. Kieroński , S. Rudolph , Finite Model Theory of the Triguarded Fragment and Related Logics , in: LICS, 2021 .

[10] J. Michaliszyn , Decidability of the Guarded Fragment with the Transitive Closure , in: ICALP, 2009 .