Guarded Negation Transitive Closure Logic

2025/01/25 by Diego Figueira, Santiago Figueira, Nakamura, Yoshiki +1 · 1 citation
#cs.LO #cs.DB

paper · pdf · doi:10.48550/arxiv.2501.15303

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 P^{NP[O(log2 n)]}-complete in combined complexity. Our result implies P^{NP[O(log2 n)]}-completeness for both UNTC and UNFO^reg, which were left open in previous works.

Citations

• Propositional dynamic logic of regular programs
• Derivatives of Regular Expressions

Cited by

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

Related

• Unary negation fragment with equivalence relations has the finite model\n property
• Satisfiability and Model Checking of CTL* with Graded Path Modalities
• Finite Satisfiability of Unary Negation Fragment with Transitivity
• A Decision Procedure for Guarded Separation Logic: Complete Entailment Checking for Separation Logic with Inductive Definitions
• On the Complexity of Team Logic and its Two-Variable Fragment