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.

翻译：本文研究守护否定传递闭包逻辑（GNTC）。我们证明GNTC的满足性问题属于2-EXPTIME（结合已有下界结果，即证其为2-EXPTIME完全），该结论将先前已知的非初等时间上界提升至2-EXPTIME。这一结果扩展了多个已知的2-EXPTIME上界结论，包括：一阶逻辑的守护否定片段、带正则路径表达式的一阶逻辑一元否定片段、带交集与逆运算的命题动态逻辑（PDL），以及有界树宽的CPDL+（支持合取查询的PDL扩展系统）。为实现该证明，我们提出了一种基于树分解的可靠且完备的局部模型检测系统。该系统具有单指数规模的闭包性质，并能在单指数时间内将GNTC的满足性问题归约为双向（弱）交替奇偶树自动机的非空性问题。此外，我们还研究了GNTC若干片段（如守护量化片段、一元否定片段、存在正片段）的满足性问题与模型检测问题的计算复杂度。