Document Open Access Logo

Guarded Negation Transitive Closure Logic

Authors Diego Figueira , Santiago Figueira , Yoshiki Nakamura

PDF

File

Thumbnail PDF
PDF
LIPIcs.LICS.2026.43.pdf
  • Filesize: 1.52 MB
  • 29 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
Keywords
  • Transitive closure logic
  • Guarded negation
  • Unary negation
  • Satisfiability
  • Model checking

Metrics

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

Cite As Get BibTex

Diego Figueira, Santiago Figueira, and Yoshiki Nakamura. Guarded Negation Transitive Closure Logic. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 43:1-43:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.LICS.2026.43

Author Details

Diego Figueira
  • Univ. Bordeaux, CNRS, Bordeaux INP, LaBRI, UMR 5800, France
Santiago Figueira
  • University of Buenos Aires, Argentina
  • CONICET, Buenos Aires, Argentina
Yoshiki Nakamura
  • Chiba University, Japan

Funding

This work was supported by JSPS KAKENHI Grant Numbers JP21K13828, JP25K14985; by ANR grants INTENDED (ANR-19-CHIA-0014) and EXPAND (ANR-25-CE23-1215); and by French-Argentinian IRP SINFIN.

Acknowledgements

We thank anonymous reviewers for their helpful and insightful comments.

References

  1. ISO/IEC JTC 1/SC 32. ISO/IEC 9075-16:2023. Information technology - Database languages SQL. Part 16: Property Graph Queries (SQL/PGQ). Technical report, ISO, 2023. URL: https://www.iso.org/standard/79473.html.
  2. ISO/IEC JTC 1/SC 32. ISO/IEC 39075:2024. Information technology - Database languages - GQL. Technical report, ISO, 2024. URL: https://www.iso.org/standard/76120.html.
  3. Hajnal Andréka, István Németi, and Johan van Benthem. Modal languages and bounded fragments of predicate logic. J. Philos. Log., 27(3):217-274, 1998. URL: https://doi.org/10.1023/A:1004275029985.
  4. Valentin Antimirov. Partial derivatives of regular expressions and finite automaton constructions. Theoretical Computer Science, 155(2):291-319, 1996. URL: https://doi.org/10.1016/0304-3975(95)00182-4.
  5. Bartosz Bednarczyk and Emanuel Kieroński. Guarded fragments meet dynamic logic: The story of regular guards. In International Conference on Principles of Knowledge Representation and Reasoning (KR), pages 89-99, 2025. URL: https://doi.org/10.24963/kr.2025/9.
  6. Michael Benedikt, Pierre Bourhis, and Michael Vanden Boom. A step up in expressiveness of decidable fixpoint logics. In Annual Symposium on Logic in Computer Science (LICS), pages 817-826. ACM, 2016. URL: https://doi.org/10.1145/2933575.2933592.
  7. Michael Benedikt, Pierre Bourhis, and Michael Vanden Boom. A step up in expressiveness of decidable fixpoint logics (extended version of [Benedikt et al., 2016]), 2016. HAL_id: hal-01413890, version: v1. URL: https://hal.science/hal-01413890v1.
  8. Mikołaj Bojańczyk. Two-way alternating automata and finite models. In International Colloquium on Automata, Languages and Programming (ICALP), volume 2380 of LNCS, pages 833-844. Springer, 2002. URL: https://doi.org/10.1007/3-540-45465-9_71.
  9. Pierre Bourhis, Markus Krötzsch, and Sebastian Rudolph. How to best nest regular path queries. In Informal Proceedings of the 27th International Workshop on Description Logics (DL), volume 1193 of CEUR Workshop Proceedings, pages 404-415. CEUR-WS.org, 2014. URL: https://ceur-ws.org/Vol-1193/paper_80.pdf.
  10. Pierre Bourhis, Markus Krötzsch, and Sebastian Rudolph. Reasonable highly expressive query languages. In International Joint Conference on Artificial Intelligence (IJCAI), pages 2826-2832. AAAI Press, 2015. URL: http://ijcai.org/Abstract/15/400.
  11. Janusz A. Brzozowski. Derivatives of regular expressions. Journal of the ACM, 11(4):481-494, 1964. URL: https://doi.org/10.1145/321239.321249.
  12. Vince Bárány and Mikołaj Bojańczyk. Finite satisfiability for guarded fixpoint logic. Information Processing Letters, 112(10):371-375, 2012. URL: https://doi.org/10.1016/j.ipl.2012.02.005.
  13. Vince Bárány, Balder ten Cate, and Luc Segoufin. Guarded negation. Journal of the ACM, 62(3):22:1-22:26, 2015. URL: https://doi.org/10.1145/2701414.
  14. Facundo Carreiro and Yde Venema. PDL inside the μ-calculus: A syntactic and an automata-theoretic characterization. In Advances in Modal Logic (AiML), pages 74-93. College Publications, 2014. URL: http://www.aiml.net/volumes/volume10/Carreiro-Venema.pdf.
  15. Mariano P. Consens and Alberto O. Mendelzon. GraphLog: a visual formalism for real life recursion. In ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems (PODS), pages 404-416. ACM, 1990. URL: https://doi.org/10.1145/298514.298591.
  16. Bruno Courcelle and Joost Engelfriet. Graph Structure and Monadic Second-Order Logic. Number 138 in Encyclopedia of Mathematics and its Applications. Cambridge University Press, 2012. URL: https://doi.org/10.1017/CBO9780511977619.
  17. Patrick Cousot and Radhia Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Annual Symposium on Principles of Programming Languages (POPL), pages 238-252. ACM, 1977. URL: https://doi.org/10.1145/512950.512973.
  18. Ryszard Danecki. Propositional dynamic logic with strong loop predicate. In International Symposium on Mathematical Foundations of Computer Science (MFCS), volume 176 of LNCS, pages 573-581. Springer, 1984. URL: https://doi.org/10.1007/BFb0030342.
  19. Daniel Danielski and Emanuel Kieroński. Finite satisfiability of unary negation fragment with transitivity. In International Symposium on Mathematical Foundations of Computer Science (MFCS), volume 138 of LIPIcs, pages 17:1-17:15. Schloss Dagstuhl, 2019. URL: https://doi.org/10.4230/LIPIcs.MFCS.2019.17.
  20. Diego Figueira and Santiago Figueira. A common ancestor of PDL, conjunctive queries, and unary negation first-order, 2025. URL: https://doi.org/10.48550/arXiv.2501.11641.
  21. Diego Figueira, Santiago Figueira, and Edwin Pin. PDL on steroids: on expressive extensions of PDL with intersection and converse. In Annual Symposium on Logic in Computer Science (LICS), pages 1-13. IEEE, 2023. URL: https://doi.org/10.1109/LICS56636.2023.10175813.
  22. Diego Figueira, Anthony W. Lin, and Liat Peterfreund. Complexity of evaluating GQL queries. In International Conference on Database Theory (ICDT), LIPIcs, pages 13:1-13:18. Schloss Dagstuhl, 2026. URL: https://doi.org/10.4230/LIPIcs.ICDT.2026.13.
  23. Michael J. Fischer and Richard E. Ladner. Propositional dynamic logic of regular programs. Journal of Computer and System Sciences, 18(2):194-211, 1979. URL: https://doi.org/10.1016/0022-0000(79)90046-1.
  24. Jörg Flum. On the (infinite) model theory of fixed-point logics. In Models, Algebras, and Proofs. CRC Press, 1998. Google Scholar
  25. Amélie Gheerbrant, Leonid Libkin, Liat Peterfreund, and Alexandra Rogova. GQL and SQL/PGQ: Theoretical models and expressive power. Proc.VLDB Endow. (VLDB), 18(6):1798-1810, 2025. URL: https://doi.org/10.14778/3725688.3725707.
  26. Erich Grädel, Martin Otto, and Eric Rosen. Undecidability results on two-variable logics. Archive for Mathematical Logic, 38(4-5):313-354, 1999. URL: https://doi.org/10.1007/s001530050130.
  27. Erich Grädel. Guarded fixed point logics and the monadic theory of countable trees. Theoretical Computer Science, 288(1):129-152, 2002. URL: https://doi.org/10.1016/S0304-3975(01)00151-7.
  28. Erich Grädel and Igor Walukiewicz. Guarded fixed point logic. In Annual Symposium on Logic in Computer Science (LICS), pages 45-54. IEEE, 1999. URL: https://doi.org/10.1109/LICS.1999.782585.
  29. Stefan Göller, Markus Lohrey, and Carsten Lutz. PDL with intersection and converse: satisfiability and infinite-state model checking. The Journal of Symbolic Logic, 74(1):279-314, 2009. URL: https://doi.org/10.2178/jsl/1231082313.
  30. Neil Immerman. Languages that capture complexity classes. SIAM Journal on Computing, 16(4):760-778, 1987. URL: https://doi.org/10.1137/0216051.
  31. Neil Immerman, Alex Rabinovich, Tom Reps, Mooly Sagiv, and Greta Yorsh. The boundary between decidability and undecidability for transitive-closure logics. In EACSL Annual Conference on Computer Science Logic (CSL), volume 3210 of LNCS, pages 160-174. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-30124-0_15.
  32. Jean Christoph Jung, Carsten Lutz, Mauricio Martel, and Thomas Schneider. Querying the unary negation fragment with regular path expressions. In International Conference on Database Theory (ICDT), volume 98 of LIPIcs. Schloss Dagstuhl, 2018. URL: https://doi.org/10.4230/LIPIcs.ICDT.2018.15.
  33. Orna Kupferman and Moshe Y. Vardi. Weak alternating automata are not that weak. ACM Trans. Comput. Logic, 2(3):408-429, 2001. URL: https://doi.org/10.1145/377978.377993.
  34. Martin Lange and Carsten Lutz. 2-ExpTime lower bounds for propositional dynamic logics with intersection. The Journal of Symbolic Logic, 70(04):1072-1086, 2005. URL: https://doi.org/10.2178/jsl/1129642115.
  35. David E. Muller, Ahmed Saoudi, and Paul E. Schupp. Alternating automata, the weak monadic theory of the tree, and its complexity. In International Colloquium on Automata, Languages, and Programming (ICALP), volume 6 of LNCS, pages 275-283. Springer, 1986. URL: https://doi.org/10.1007/3-540-16761-7_77.
  36. David E. Muller, Ahmed Saoudi, and Paul E. Schupp. Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time. In Annual Symposium on Logic in Computer Science (LICS), pages 422-427. IEEE, 1988. URL: https://doi.org/10.1109/LICS.1988.5139.
  37. Yoshiki Nakamura. Partial derivatives on graphs for Kleene allegories. In Annual Symposium on Logic in Computer Science (LICS), pages 1-12. IEEE, 2017. URL: https://doi.org/10.1109/LICS.2017.8005132.
  38. Yoshiki Nakamura. Existential calculi of relations with transitive closure: Complexity and edge saturations. In Annual Symposium on Logic in Computer Science (LICS), pages 1-13. IEEE, 2023. URL: https://doi.org/10.1109/LICS56636.2023.10175811.
  39. Yoshiki Nakamura. Undecidability of the positive calculus of relations with transitive closure and difference: Hypothesis elimination using graph loops. In International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS), volume 14787 of LNCS, pages 207-224. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-68279-7_13.
  40. Yoshiki Nakamura. Derivatives on graphs for the positive calculus of relations with transitive closure. Logical Methods in Computer Science, Volume 21, Issue 4, 2025. URL: https://doi.org/10.46298/lmcs-21(4:27)2025.
  41. Yoshiki Nakamura. Undecidability of the emptiness problem of deterministic propositional while programs with graph loop: Hypothesis elimination using loops, 2025. URL: https://doi.org/10.48550/arXiv.2504.20415.
  42. Damien Pous. On the positive calculus of relations with transitive closure. In International Symposium on Theoretical Aspects of Computer Science (STACS), volume 96 of LIPIcs, pages 3:1-3:16. Schloss Dagstuhl, 2018. URL: https://doi.org/10.4230/LIPIcs.STACS.2018.3.
  43. Juan L. Reutter, Miguel Romero, and Moshe Y. Vardi. Regular queries on graph databases. Theory of Computing Systems, 61(1):31-83, 2017. URL: https://doi.org/10.1007/s00224-016-9676-2.
  44. Neil Robertson and Paul D. Seymour. Graph minors. II. algorithmic aspects of tree-width. Journal of Algorithms, 7(3):309-322, 1986. URL: https://doi.org/10.1016/0196-6774(86)90023-4.
  45. Hadar Rotschield and Liat Peterfreund. On the expressiveness of languages for querying Property Graphs in relational databases. Proc. ACM Manag. Data (PODS), 3(5):279:1-279:18, 2025. URL: https://doi.org/10.1145/3767715.
  46. Philippe Schnoebelen. Oracle circuits for branching-time model checking. In International Colloquium on Automata, Languages and Programming (ICALP), volume 2719 of LNCS, pages 790-801. Springer, 2003. URL: https://doi.org/10.1007/3-540-45061-0_62.
  47. Luc Segoufin and Balder ten Cate. Unary negation. Logical Methods in Computer Science, Volume 9, Issue 3, 2013. URL: https://doi.org/10.2168/LMCS-9(3:25)2013.
  48. Moshe Y. Vardi. Reasoning about the past with two-way automata. In International Colloquium on Automata, Languages and Programming (ICALP), volume 1443 of LNCS, pages 628-641. Springer, 1998. URL: https://doi.org/10.1007/BFb0055090.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact