Guarded Negation Transitive Closure Logic
For logicians and computer scientists studying the complexity of logics with transitive closure, this establishes tight complexity bounds for GNTC and its fragments, settling open questions.
The paper proves that the satisfiability problem for guarded negation transitive closure logic (GNTC) is 2ExpTime-complete, and the model checking problem is P^{NP[O(log^2 n)]}-complete, resolving open problems for related logics.
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.