Document Open Access Logo

Finite Relational Semantics for Language Kleene Algebra with Complement

Author Yoshiki Nakamura

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2025.37.pdf
  • Filesize: 1.02 MB
  • 23 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Equational logic and rewriting
  • Theory of computation → Logic and verification
  • Theory of computation → Formal languages and automata theory
Keywords
  • Kleene algebra
  • Language model
  • Relational model
  • Complexity

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

We study the equational theory of Kleene algebra (KA) w.r.t. languages (here, meaning the equational theory of regular expressions where each letter maps to any language) by extending the algebraic signature with the language complement. This extension significantly enhances the expressive power of KA. In this paper, we present a finite relational semantics completely characterizing the equational theory w.r.t. languages, which extends the relational characterizations known for KA and for KA with top. Based on this relational semantics, we show that the equational theory w.r.t. languages is Π⁰₁-complete for KA with complement (with or without Kleene-star) and is PSPACE-complete if the complement only applies to variables or constants.

Cite As Get BibTex

Yoshiki Nakamura. Finite Relational Semantics for Language Kleene Algebra with Complement. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 37:1-37:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CSL.2025.37

Author Details

Yoshiki Nakamura
  • Institute of Science Tokyo, Japan

Funding

This work was supported by JSPS KAKENHI Grant Number JP21K13828.

Acknowledgements

We thank anonymous reviewers for useful comments.

References

  1. Hajnal Andréka and D. A. Bredikhin. The equational theory of union-free algebras of relations. Algebra Universalis, 33(4):516-532, 1995. URL: https://doi.org/10.1007/BF01225472.
  2. 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.
  3. S. L. Bloom, Z. Ésik, and Gh. Stefanescu. Notes on equational theories of relations. algebra universalis, 33(1):98-126, 1995. URL: https://doi.org/10.1007/BF01190768.
  4. Paul Brunet. Reversible Kleene lattices. In MFCS, volume 83 of LIPIcs, pages 66:1-66:14. Schloss Dagstuhl, 2017. URL: https://doi.org/10.4230/LIPICS.MFCS.2017.66.
  5. Paul Brunet. A complete axiomatisation of a fragment of language algebra. In CSL, volume 152 of LIPIcs, pages 11:1-11:15. Schloss Dagstuhl, 2020. URL: https://doi.org/10.4230/LIPIcs.CSL.2020.11.
  6. Paul Brunet and Damien Pous. Petri automata for Kleene allegories. In LICS, pages 68-79. IEEE, 2015. URL: https://doi.org/10.1109/LICS.2015.17.
  7. 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.
  8. Wojciech Buszkowski. On the complexity of the equational theory of relational action algebras. In RAMICS, volume 4136 of LNTCS, pages 106-119. Springer, 2006. URL: https://doi.org/10.1007/11828563_7.
  9. Ernie Cohen. Hypotheses in Kleene algebra. Unpublished manuscript, 1994. Google Scholar
  10. Rina S. Cohen and J. A. Brzozowski. Dot-depth of star-free events. Journal of Computer and System Sciences, 5(1):1-16, 1971. URL: https://doi.org/10.1016/S0022-0000(71)80003-X.
  11. John H. Conway. Regular Algebra and Finite Machines. Chapman and Hall, 1971. Google Scholar
  12. Isabel F. Cruz, Alberto O. Mendelzon, and Peter T. Wood. A graphical query language supporting recursion. ACM SIGMOD Record, 16(3):323-330, 1987. URL: https://doi.org/10.1145/38714.38749.
  13. 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.
  14. Amina Doumane, Denis Kuperberg, Damien Pous, and Pierre Pradic. Kleene algebra with hypotheses. In FoSSaCS, volume 11425 of LNTCS, pages 207-223. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17127-8_12.
  15. Heinz-Dieter Ebbinghaus and Jörg Flum. Finite Model Theory. Springer, 1995. URL: https://doi.org/10.1007/3-540-28788-4.
  16. Andrzej Ehrenfeucht. An application of games to the completeness problem for formalized theories. Fundamenta Mathematicae, 49(2):129-141, 1961. URL: https://doi.org/10.4064/fm-49-2-129-141.
  17. Roland Fraïssé. Sur les classifications des systems de relations. Publ. Sci. Univ. Alger I., 1954. Google Scholar
  18. Martin Fürer. The complexity of the inequivalence problem for regular expressions with intersection. In ICALP, volume 85 of LNCS, pages 234-245. Springer, 1980. URL: https://doi.org/10.1007/3-540-10003-2_74.
  19. Steven Givant. The calculus of relations. In Introduction to Relation Algebras, volume 1, pages 1-34. Springer International Publishing, 2017. URL: https://doi.org/10.1007/978-3-319-65235-1_1.
  20. 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.
  21. Jelle Hellings, Catherine L. Pilachowski, Dirk Van Gucht, Marc Gyssens, and Yuqing Wu. From relation algebra to semi-join algebra: An approach to graph query optimization. The Computer Journal, 64(5):789-811, 2021. URL: https://doi.org/10.1093/comjnl/bxaa031.
  22. Robin Hirsch and Ian Hodkinson. Relation Algebras by Games, volume 147 of Studies in logic and the foundations of mathematics. Elsevier, 1 edition, 2002. Google Scholar
  23. Tony Hoare, Bernhard Möller, Georg Struth, and Ian Wehrman. Concurrent Kleene algebra and its foundations. The Journal of Logic and Algebraic Programming, 80(6):266-296, 2011. URL: https://doi.org/10.1016/j.jlap.2011.04.005.
  24. Stephen C. Kleene. Representation of events in nerve nets and finite automata. In Automata Studies. (AM-34), pages 3-42. Princeton University Press, 1956. URL: https://doi.org/10.1515/9781400882618-002.
  25. Dexter Kozen. A completeness theorem for Kleene algebras and the algebra of regular events. In LICS, pages 214-225. IEEE, 1991. URL: https://doi.org/10.1109/LICS.1991.151646.
  26. Dexter Kozen. On Hoare logic and Kleene algebra with tests. ACM Transactions on Computational Logic, 1(1):60-76, 2000. URL: https://doi.org/10.1145/343369.343378.
  27. Dexter Kozen. On the complexity of reasoning in Kleene algebra. Information and Computation, 179(2):152-162, 2002. URL: https://doi.org/10.1006/INCO.2001.2960.
  28. Dexter Kozen and Konstantinos Mamouras. Kleene algebra with equations. In ICALP, volume 8573 of LNCS, pages 280-292. Springer, 2014. URL: https://doi.org/10.1007/978-3-662-43951-7_24.
  29. Dexter Kozen and Frederick Smith. Kleene algebra with tests: Completeness and decidability. In CSL, volume 1258 of LNCS, pages 244-259. Springer, 1996. URL: https://doi.org/10.1007/3-540-63172-0_43.
  30. F. W. Levi. On semigroups. Bulletin of the Calcutta Mathematical Society, 36(36):141-146, 1944. Google Scholar
  31. A. R. Meyer and L. J. Stockmeyer. The equivalence problem for regular expressions with squaring requires exponential space. In SWAT, pages 125-129. IEEE, 1972. URL: https://doi.org/10.1109/SWAT.1972.29.
  32. Yoshiki Nakamura. Partial derivatives on graphs for Kleene allegories. In LICS, pages 1-12. IEEE, 2017. URL: https://doi.org/10.1109/LICS.2017.8005132.
  33. Yoshiki Nakamura. Expressive power and succinctness of the positive calculus of binary relations. Journal of Logical and Algebraic Methods in Programming, 127:100760, 2022. URL: https://doi.org/10.1016/j.jlamp.2022.100760.
  34. Yoshiki Nakamura. Existential calculi of relations with transitive closure: Complexity and edge saturations. In LICS, pages 1-13. IEEE, 2023. URL: https://doi.org/10.1109/LICS56636.2023.10175811.
  35. Yoshiki Nakamura. Finite relational semantics for language Kleene algebra with complement, 2024. URL: https://hal.science/hal-04455882.
  36. Yoshiki Nakamura. Undecidability of the positive calculus of relations with transitive closure and difference: Hypothesis elimination using graph loops. In RAMICS, volume 14787 of LNTCS, pages 207-224. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-68279-7_13.
  37. Yoshiki Nakamura. Derivatives on graphs for the positive calculus of relations with transitive closure, 2024 (submitted, journal version of [Nakamura, 2017]). URL: https://doi.org/10.48550/arXiv.2408.08236.
  38. Yoshiki Nakamura and Ryoma Sin'ya. Words-to-letters valuations for language Kleene algebras with variable complements. In AFL, volume 386 of EPTCS, pages 185-199. EPTCS, 2023. URL: https://doi.org/10.4204/EPTCS.386.15.
  39. Yoshiki Nakamura and Ryoma Sin'ya. Words-to-letters valuations for language Kleene algebras with variable and constant complements, 2024 (accepted, journal version of [Nakamura and Sin'ya, 2023]). URL: https://arxiv.org/abs/2309.02760.
  40. Kan Ching Ng. Relation algebras with transitive closure. PhD thesis, University of California, 1984. Google Scholar
  41. 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.
  42. Jean-Éric Pin. The dot-depth hierarchy, 45 years later. In The Role of Theory in Computer Science, pages 177-201. WORLD SCIENTIFIC, 2016. URL: https://doi.org/10.1142/9789813148208_0008.
  43. Damien Pous. On the positive calculus of relations with transitive closure. In STACS, volume 96 of LIPIcs, pages 3:1-3:16. Schloss Dagstuhl, 2018. URL: https://doi.org/10.4230/LIPICS.STACS.2018.3.
  44. Damien Pous, Jurriaan Rot, and Jana Wagemaker. On tools for completeness of kleene algebra with hypotheses. Logical Methods in Computer Science, Volume 20, Issue 2, 2024. URL: https://doi.org/10.46298/lmcs-20(2:8)2024.
  45. Damien Pous and Jana Wagemaker. Completeness theorems for Kleene algebra with top. In CONCUR, volume 243 of LIPIcs, pages 26:1-26:18. Schloss Dagstuhl, 2022. URL: https://doi.org/10.4230/LIPICS.CONCUR.2022.26.
  46. V. R. Pratt. Dynamic algebras and the nature of induction. In STOC, pages 22-28. ACM, 1980. URL: https://doi.org/10.1145/800141.804649.
  47. Sylvain Schmitz. Complexity hierarchies beyond elementary. ACM Transactions on Computation Theory, 8(1):1-36, 2016. URL: https://doi.org/10.1145/2858784.
  48. Steffen Smolka, Nate Foster, Justin Hsu, Tobias Kappé, Dexter Kozen, and Alexandra Silva. Guarded Kleene algebra with tests: verification of uninterpreted programs in nearly linear time. Proceedings of the ACM on Programming Languages, 4(POPL):61:1-61:28, 2019. URL: https://doi.org/10.1145/3371129.
  49. Larry J. Stockmeyer. The Complexity of Decision Problems in Automata Theory and Logic. PhD thesis, Massachusetts Institute of Technology, 1974. URL: https://doi.org/1721.1/15540.
  50. Alfred Tarski. On the calculus of relations. The Journal of Symbolic Logic, 6(3):73-89, 1941. URL: https://doi.org/10.2307/2268577.
  51. Wolfgang Thomas. A concatenation game and the dot-depth hierarchy. In Computation Theory and Logic, number 270 in LNCS, pages 415-426. Springer, 1987. URL: https://doi.org/10.1007/3-540-18170-9_183.
  52. B. A. Trakhtenbrot. The impossibility of an algorithm for the decision problem in finite classes. Doklady Akademii Nauk SSSR, 70(4):569-572, 1950. Google Scholar
  53. Cheng Zhang, Arthur Azevedo de Amorim, and Marco Gaboardi. On incorrectness logic and Kleene algebra with top and tests. Proceedings of the ACM on Programming Languages, 6(POPL):29:1-29:30, 2022. URL: https://doi.org/10.1145/3498690.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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