Document Open Access Logo

The Equational Theory of Relational Kleene Algebra with Graph Loop is PSPACE-Complete

Author Yoshiki Nakamura

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2026.25.pdf
  • Filesize: 1.65 MB
  • 19 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
  • Theory of computation → Formal languages and automata theory
  • Theory of computation → Logic and databases
  • Theory of computation → Programming logic
Keywords
  • Kleene algebra
  • Graph loop
  • Domain

Metrics

Abstract

In this paper, we show that the equational theory of relational Kleene algebra with the graph loop operator (a.k.a. fixset) is PSpace-complete. Here, the graph loop is the unary operator that restricts a binary relation to the identity relation. We further show that this PSpace-completeness still holds by extending the terms with top, tests, converse, and nominals, over relational models. Notably, for Kleene algebra with tests (KAT), while the equational theory of relational KAT with antidomain is ExpTime-complete, we show that the equational theory of relational KAT with domain is PSpace-complete, thereby resolving a problem left open in previous works.
To this end, we introduce a novel automaton model on relational structures (graphs), called loop-automata. Loop-automata extend nondeterministic finite automata with a transition type that tests whether the current vertex has a loop. Using this model, we can give a polynomial-time reduction from the equational theories above to the language inclusion problem for 2-way alternating automata.

Cite As Get BibTex

Yoshiki Nakamura. The Equational Theory of Relational Kleene Algebra with Graph Loop is PSPACE-Complete. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 25:1-25:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.FSCD.2026.25

Author Details

Yoshiki Nakamura
  • Chiba University, Japan

Acknowledgements

This work was supported by JSPS KAKENHI Grant Numbers JP21K13828 and JP25K14985.

References

  1. Hajnal Andréka, Szabolcs Mikulás, and István Németi. The equational theory of Kleene lattices. Theoretical Computer Science, 412(52):7099-7108, 2011. URL: https://doi.org/10.1016/J.TCS.2011.09.024.
  2. Carlos Areces and Balder ten Cate. Hybrid logics. In Handbook of Modal Logic, volume 3 of Studies in Logic and Practical Reasoning, pages 821-868. Elsevier, 2007. URL: https://doi.org/10.1016/S1570-2464(07)80017-6.
  3. Paul Brunet and Damien Pous. Kleene algebra with converse. In International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS), volume 8428 of LNCS, pages 101-118. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-06251-8_7.
  4. Paul Brunet and Damien Pous. Petri automata. Logical Methods in Computer Science, 13(3), 2017. URL: https://doi.org/10.23638/LMCS-13(3:33)2017.
  5. Diego Calvanese, Giuseppe De Giacomo, Maurizio Lenzerini, and Moshe Y. Vardi. Rewriting of regular expressions and regular path queries. In ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems (PODS), pages 194-204. ACM, 1999. URL: https://doi.org/10.1145/303976.303996.
  6. 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.
  7. 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.
  8. Jules Desharnais, Bernhard Möller, and Georg Struth. Kleene algebra with domain. ACM Transactions on Computational Logic, 7(4):798-833, 2006. URL: https://doi.org/10.1145/1183278.1183285.
  9. Jules Desharnais and Georg Struth. Modal semirings revisited. In Mathematics of Program Construction (MPC), volume 5133 of LNTCS, pages 360-387. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-70594-9_19.
  10. Jules Desharnais and Georg Struth. Internal axioms for domain semirings. Science of Computer Programming, 76(3):181-203, 2011. URL: https://doi.org/10.1016/j.scico.2010.05.007.
  11. 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.
  12. Viliam Geffert and Alexander Okhotin. Transforming two-way alternating finite automata to one-way nondeterministic automata. In International Symposium on Mathematical Foundations of Computer Science (MFCS), volume 8634 of LNTCS, pages 291-302. Springer, 2014. URL: https://doi.org/10.1007/978-3-662-44522-8_25.
  13. 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.
  14. Chris Hardin and Dexter Kozen. On the complexity of the Horn theory of REL. Technical report, Cornell University, 2003. URL: https://hdl.handle.net/1813/5612.
  15. Robin Hirsch, Marcel Jackson, and Szabolcs Mikulás. The algebra of functions with antidomain and range. Journal of Pure and Applied Algebra, 220(6):2214-2239, 2016. URL: https://doi.org/10.1016/j.jpaa.2015.11.003.
  16. Neil Immerman. Descriptive Complexity. Texts in Computer Science. Springer, 1 edition, 1999. URL: https://doi.org/10.1007/978-1-4612-0539-5.
  17. Dexter Kozen. A completeness theorem for Kleene algebras and the algebra of regular events. Information and Computation, 110(2):366-390, 1994. URL: https://doi.org/10.1006/inco.1994.1037.
  18. Dexter Kozen. Kleene algebra with tests. ACM Transactions on Programming Languages and Systems, 19(3):427-443, 1997. URL: https://doi.org/10.1145/256167.256195.
  19. Dexter Kozen and Frederick Smith. Kleene algebra with tests: Completeness and decidability. In EACSL Annual Conference on Computer Science Logic (CSL), volume 1258 of LNCS, pages 244-259. Springer, 1996. URL: https://doi.org/10.1007/3-540-63172-0_43.
  20. Carsten Lutz and Dirk Walther. PDL with negation of atomic programs. Journal of Applied Non-Classical Logics, 15(2):189-213, 2005. URL: https://doi.org/10.3166/jancl.15.189-213.
  21. Brett McLean. Free Kleene algebras with domain. Journal of Logical and Algebraic Methods in Programming, 117:100606, 2020. URL: https://doi.org/10.1016/j.jlamp.2020.100606.
  22. Robert McNaughton and Hisao Yamada. Regular expressions and state graphs for automata. IRE Transactions on Electronic Computers, EC-9(1):39-47, 1960. URL: https://doi.org/10.1109/TEC.1960.5221603.
  23. Albert R. Meyer and Larry J. Stockmeyer. The equivalence problem for regular expressions with squaring requires exponential space. In Annual Symposium on Switching and Automata Theory (SWAT), pages 125-129. IEEE, 1972. URL: https://doi.org/10.1109/SWAT.1972.29.
  24. Yoshiki Nakamura. Partial derivatives on graphs for Kleene allegories. In Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-12. IEEE, 2017. URL: https://doi.org/10.1109/LICS.2017.8005132.
  25. Yoshiki Nakamura. Existential calculi of relations with transitive closure: Complexity and edge saturations. In Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-13. IEEE, 2023. URL: https://doi.org/10.1109/LICS56636.2023.10175811.
  26. 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.
  27. 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.
  28. Yoshiki Nakamura. Undecidability of the emptiness problem of deterministic propositional while programs with graph loop: Hypothesis elimination using loops, 2025. URL: https://arxiv.org/abs/2504.20415v1.
  29. Peter W. O'Hearn. Incorrectness logic. Proceedings of the ACM on Programming Languages, 4(POPL):10:1-10:32, 2019. URL: https://doi.org/10.1145/3371078.
  30. Damien Pous. On the positive calculus of relations with transitive closure. In 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.
  31. Damien Pous and Jana Wagemaker. Completeness theorems for Kleene algebra with tests and top. Logical Methods in Computer Science, Volume 20, Issue 3, 2024. URL: https://doi.org/10.46298/lmcs-20(3:27)2024.
  32. Jorge Pérez, Marcelo Arenas, and Claudio Gutierrez. nSPARQL: A navigational language for RDF. In International Semantic Web Conference (ISWC), volume 5318 of LNISA, pages 66-81. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-88564-1_5.
  33. Juan L. Reutter. Containment of nested regular expressions, 2013. URL: https://arxiv.org/abs/1304.2637v2.
  34. Igor Sedlár. Kleene algebra with dynamic tests: Completeness and complexity, 2023. URL: https://arxiv.org/abs/2311.06937v1.
  35. Igor Sedlár. On the complexity of Kleene algebra with domain. In International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS), volume 13896 of LNCS, pages 208-223. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-28083-2_13.
  36. Alfred Tarski. On the calculus of relations. The Journal of Symbolic Logic, 6(3):73-89, 1941. URL: https://doi.org/10.2307/2268577.
  37. Ken Thompson. Programming techniques: Regular expression search algorithm. Communications of the ACM, 11(6):419-422, 1968. URL: https://doi.org/10.1145/363347.363387.
  38. Lena Verscht and Benjamin Lucien Kaminski. A taxonomy of Hoare-like logics: Towards a holistic view using predicate transformers and Kleene algebras with top and tests. Proc. ACM Program. Lang., 9(POPL):60:1782-60:1811, 2025. URL: https://doi.org/10.1145/3704896.
  39. Cheng Zhang, Arthur Azevedo de Amorim, and Marco Gaboardi. Domain reasoning in TopKAT. In International Colloquium on Automata, Languages, and Programming (ICALP), volume 297 of LIPIcs, pages 157:1-157:18. Schloss Dagstuhl, 2024. URL: https://doi.org/10.4230/LIPIcs.ICALP.2024.157.
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