Guarded Negation Transitive Closure Logic

TL;DR

This paper analyzes the computational complexity of the guarded negation fragment of transitive closure logic (GNTC), establishing its satisfiability and model checking problems as 2ExpTime-complete and P^NP[log^2 n]-complete respectively.

Contribution

It provides the first complexity characterizations of GNTC's satisfiability and model checking problems, including reductions to automata-based problems.

Findings

Satisfiability for GNTC is 2ExpTime-complete.

Model checking for GNTC is P^NP[log^2 n]-complete.

Results imply similar complexity bounds for UNTC and UNFO^{reg}.

Abstract

We study the guarded negation fragment of transitive closure logic (GNTC). We show that the satisfiability problem for GNTC is 2ExpTime-complete, by establishing the following reductions: (i) a polynomial-time reduction from the satisfiability problem for GNTC to the satisfiability problem for the unary negation fragment UNTC of GNTC, and (ii) a direct exponential-time reduction from the satisfiability problem for UNTC to the non-emptiness problem for 2-way alternating parity tree automata. Furthermore, we show that the model checking problem for GNTC is $\mathsf{P}^{\mathsf{NP}[\mathcal{O}(\log^2 n)]}$-complete in combined complexity. Our result implies $\mathsf{P}^{\mathsf{NP}[\mathcal{O}(\log^2 n)]}$-completeness for both UNTC and $\mathrm{UNFO}^{\mathrm{reg}}$, which were left open in previous works.