Guarded Negation Transitive Closure Logic is 2-EXPTIME-complete

TL;DR

This work studies the satisfiability problem for guarded negation transitive closure logic (GNTC) and proves it is $2$-EXPTIME-complete, improving on prior non-elementary upper bounds. The authors develop a sound and complete local model checker on tree decompositions and show how its closure properties yield a reduction to non-emptiness for 2-way alternating parity tree automata (2APTA) with a single exponential blow-up, thereby achieving the tight complexity bound. They extend the framework to GNFO and GNFP-UP fragments and compare GNTC with related logics such as GNFP-UP, GNF(TC), UNTC, and CPDL+, including implications for finite satisfiability and containment problems. Overall, the paper provides a unified automata-theoretic approach to guarded logics with transitive closure and lays groundwork for further extensions and optimizations in guarded reasoning with transitive relations.

Abstract

We consider guarded negation transitive closure logic (GNTC). In this paper, we show that the satisfiability problem for GNTC is in 2-EXPTIME (hence, 2-EXPTIME-complete from existing lower bound results), which improves the previously known non-elementary time upper bound. This extends previously known 2-EXPTIME upper bound results, e.g., for the guarded negation fragment of first-order logic, the unary negation fragment of first-order logic with regular path expressions, propositional dynamic logic (PDL) with intersection and converse, and CPDL+ (an extension of PDL with conjunctive queries) of bounded treewidth. To this end, we present a sound and complete local model checker on tree decompositions. This system has a closure property of size single exponential, and it induces a reduction from the satisfiability problem for GNTC into the non-emptiness problem for 2-way (weak) alternating parity tree automata in single exponential time. Additionally, we investigate the complexity of satisfiability and model checking for fragments of GNTC, such as guarded (quantification) fragments, unary negation fragments, and existential positive fragments.

Figures (12)

• Figure 1: Illustration of directions from $g$ and the operator $\diamond$.
• Figure 2: Example of the gluing operator $\odot \bar{ \mathfrak A }$.
• Figure 3: Illustration for the abstraction map on bag $11$ where $\bar{ \mathfrak A }$ is the tree given in \ref{['figure: gluing']}.
• Figure 4: The transition rules in the local model checker (\ref{['section: model checker GNFO']}) for GNFO.
• Figure 5: Illustration of the rule \ref{['rule: split']}.

Theorems & Definitions (127)

• Proposition 1: vardiReasoningTwowayAutomata1998
• Remark 2
• Proposition 3: see also \ref{['section: GNFP-UP']}
• Proposition 4
• proof
• Definition 5
• Proposition 6
• proof
• Example 7
• Proposition 8