Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Finite Satisfiability of the Two-Variable Guarded Fragment with Transitive Guards and Related Variants

Emanuel Kieronski, Lidia Tendera

TL;DR

This work analyzes the finite satisfiability problem for GF2 extended with special guards that enforce transitive, equivalence, pre-order, or partial-order interpretations. The authors establish that only GF2+{eG} without equality has the exponential finite-model property, while the others admit only doubly exponential minimal models; they then precisely determine the complexity: GF2+{eG} without equality is in $\mathrm{NExpTime}$ (and with equality remains $\mathrm{NExpTime}$-complete), and GF2+{tG} achieves $\mathrm{2ExpTime}$-hardness and a $\mathrm{2ExpTime}$ upper bound. A core technique is a ramified-model construction built from multidimensional grids on a cylinder, combined with counting-types and a reduction to linear/integer programming to bound model size. These methods yield tight complexity bounds and illuminate the role of guard-structure on decidability and finite-model properties in two-variable guarded logics. The results have implications for description and temporal logics, where guarded fragments with transitive or equivalence-related guards are common.

Abstract

We consider extensions of the two-variable guarded fragment, GF2, where distinguished binary predicates that occur only in guards are required to be interpreted in a special way (as transitive relations, equivalence relations, pre-orders or partial orders). We prove that the only fragment that retains the finite (exponential) model property is GF2 with equivalence guards without equality. For remaining fragments we show that the size of a minimal finite model is at most doubly exponential. To obtain the result we invent a strategy of building finite models that are formed from a number of multidimensional grids placed over a cylindrical surface. The construction yields a 2NExpTime-upper bound on the complexity of the finite satisfiability problem for these fragments. We improve the bounds and obtain optimal ones for all the fragments considered, in particular NExpTime for GF2 with equivalence guards, and 2ExpTime for GF2 with transitive guards. To obtain our results we essentially use some results from integer programming.

Finite Satisfiability of the Two-Variable Guarded Fragment with Transitive Guards and Related Variants

TL;DR

This work analyzes the finite satisfiability problem for GF2 extended with special guards that enforce transitive, equivalence, pre-order, or partial-order interpretations. The authors establish that only GF2+{eG} without equality has the exponential finite-model property, while the others admit only doubly exponential minimal models; they then precisely determine the complexity: GF2+{eG} without equality is in (and with equality remains -complete), and GF2+{tG} achieves -hardness and a upper bound. A core technique is a ramified-model construction built from multidimensional grids on a cylinder, combined with counting-types and a reduction to linear/integer programming to bound model size. These methods yield tight complexity bounds and illuminate the role of guard-structure on decidability and finite-model properties in two-variable guarded logics. The results have implications for description and temporal logics, where guarded fragments with transitive or equivalence-related guards are common.

Abstract

We consider extensions of the two-variable guarded fragment, GF2, where distinguished binary predicates that occur only in guards are required to be interpreted in a special way (as transitive relations, equivalence relations, pre-orders or partial orders). We prove that the only fragment that retains the finite (exponential) model property is GF2 with equivalence guards without equality. For remaining fragments we show that the size of a minimal finite model is at most doubly exponential. To obtain the result we invent a strategy of building finite models that are formed from a number of multidimensional grids placed over a cylindrical surface. The construction yields a 2NExpTime-upper bound on the complexity of the finite satisfiability problem for these fragments. We improve the bounds and obtain optimal ones for all the fragments considered, in particular NExpTime for GF2 with equivalence guards, and 2ExpTime for GF2 with transitive guards. To obtain our results we essentially use some results from integer programming.

Paper Structure

This paper contains 16 sections, 16 theorems, 21 equations, 4 figures, 1 table.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Special Guards
  4. Examples
  5. Normal forms
  6. Types and Counting types
  7. Equivalence guards. The case without equality
  8. Equivalence Guards. The case with equality
  9. Systems of linear inequalities
  10. Neat model construction
  11. Transitive Guards
  12. Basic notions and outline of the bounded size model construction
  13. Certificates of finite satisfiability
  14. Construction of a bounded size model
  15. Complexity
  16. ...and 1 more sections

Key Result

Lemma 2.1

There is a linear time reduction transforming any $\hbox{\rm GF}^2{+}{\textsc{tG}}$ sentence $\varphi$ over a signature $\sigma$ into a $\hbox{\rm GF}^2{+}{\textsc{trG}}$-sentence $\varphi'$ over a signature $\sigma'$ such that $\varphi$ and $\varphi'$ are satisfiable over the same domains and $\sig

Figures (4)

  • Figure 1: An infinite model of $\lambda$.
  • Figure 2: Doubly exponential $E_2$-class: thin lines correspond to $E_1$ connections, thick lines---to $E_2$; grey regions depict $E_2$-classes.
  • Figure 3: An alternating chain of $T$-cliques
  • Figure 4: Arrangement of elements on the two-dimensional grid and an illustrative division into classes. $E_1$-classes are dark grey, $E_2$-classes are light grey.

Theorems & Definitions (48)

  • Lemma 2.1
  • proof
  • Example 2.2: Enforcing infinite models in $\hbox{\rm GF}^2{+}{\textsc{eG}}$ with equality
  • Example 2.3: Enforcing large finite models in $\hbox{\rm GF}^2{+}{\textsc{eG}}$ with equality
  • Example 2.4: Enforcing infinite models in $\hbox{\rm GF}^2{+}{\textsc{tG}}$ or $\hbox{\rm GF}^2{+}{\textsc{trG}}$ without equality
  • Example 2.5: Enforcing large finite models in $\hbox{\rm GF}^2{+}{\textsc{tG}}$ or in $\hbox{\rm GF}^2{+}{\textsc{trG}}$, without equality
  • Lemma 2.6
  • Definition 2.7
  • Definition 3.1
  • Definition 3.2
  • ...and 38 more