Document Open Access Logo

Kleene Algebra with Commutativity Conditions Is Undecidable

Authors Arthur Azevedo de Amorim , Cheng Zhang , Marco Gaboardi

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2025.36.pdf
  • Filesize: 0.78 MB
  • 25 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
  • Theory of computation → Regular languages
Keywords
  • Kleene Algebra
  • Hypotheses
  • Complexity

Metrics

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

Abstract

We prove that the equational theory of Kleene algebra with commutativity conditions on primitives (or atomic terms) is undecidable, thereby settling a longstanding open question in the theory of Kleene algebra. While this question has also been recently solved independently by Kuznetsov, our results hold even for weaker theories that do not support the induction axioms of Kleene algebra.

Cite As Get BibTex

Arthur Azevedo de Amorim, Cheng Zhang, and Marco Gaboardi. Kleene Algebra with Commutativity Conditions Is Undecidable. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 36:1-36:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CSL.2025.36

Author Details

Arthur Azevedo de Amorim
  • Rochester Institute of Technology, NY, USA
Cheng Zhang
  • University College London, UK
Marco Gaboardi
  • Boston University, MA, USA

Funding

  • Azevedo de Amorim, Arthur: National Science Foundation Grant No. 2314323.
  • Zhang, Cheng: National Science Foundation Award No. 1845803 and No. 2040249.
  • Gaboardi, Marco: National Science Foundation Award No. 1845803 and No. 2040249.

Acknowledgements

We want to thank Todd Schmid and Alexandra Silva for the valuable discussion during this work; and also acknowledge the useful feedback provided by the anonymous reviewers of CSL2025. Finally, we want to thank Stepan Kuznetsov for his detailed and valuable feedback on this work.

References

  1. Carolyn Jane Anderson, Nate Foster, Arjun Guha, Jean-Baptiste Jeannin, Dexter Kozen, Cole Schlesinger, and David Walker. Netkat: semantic foundations for networks. ACM SIGPLAN Notices, 49(1):113-126, January 2014. URL: https://doi.org/10.1145/2578855.2535862.
  2. Allegra Angus and Dexter Kozen. Kleene Algebra with Tests and Program Schematology. Technical Report, Cornell University, USA, June 2001. Google Scholar
  3. Valentin Antimirov. Partial derivatives of regular expressions and finite automaton constructions. Theoretical Computer Science, 155(2):291-319, March 1996. URL: https://doi.org/10.1016/0304-3975(95)00182-4.
  4. Timos Antonopoulos, Eric Koskinen, Ton Chanh Le, Ramana Nagasamudram, David A. Naumann, and Minh Ngo. An Algebra of Alignment for Relational Verification. Proceedings of the ACM on Programming Languages, 7(POPL):20:573-20:603, January 2023. URL: https://doi.org/10.1145/3571213.
  5. Jean Berstel. Transductions and Context-Free Languages. Vieweg+Teubner Verlag, Wiesbaden, 1979. URL: https://doi.org/10.1007/978-3-663-09367-1.
  6. Volker Diekert and Yves Métivier. Partial Commutation and Traces. In Grzegorz Rozenberg and Arto Salomaa, editors, Handbook of Formal Languages: Volume 3 Beyond Words, pages 457-533. Springer, Berlin, Heidelberg, 1997. URL: https://doi.org/10.1007/978-3-642-59126-6_8.
  7. Nate Foster, Dexter Kozen, Mae Milano, Alexandra Silva, and Laure Thompson. A coalgebraic decision procedure for netkat. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’15, pages 343-355, New York, NY, USA, January 2015. Association for Computing Machinery. URL: https://doi.org/10.1145/2676726.2677011.
  8. Alan Gibbons and Wojciech Rytter. On the decidability of some problems about rational subsets of free partially commutative monoids. Theoretical Computer Science, 48:329-337, January 1986. URL: https://doi.org/10.1016/0304-3975(86)90101-5.
  9. C. A. R. Tony Hoare, Bernhard Möller, Georg Struth, and Ian Wehrman. Concurrent Kleene Algebra. In Mario Bravetti and Gianluigi Zavattaro, editors, CONCUR 2009 - Concurrency Theory, pages 399-414, Berlin, Heidelberg, 2009. Springer. URL: https://doi.org/10.1007/978-3-642-04081-8_27.
  10. J.E. Hopcroft, R. Motwani, and J.D. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley series in computer science. Addison-Wesley, 2001. URL: https://books.google.com/books?id=omIPAQAAMAAJ.
  11. Tobias Kappé, Paul Brunet, Alexandra Silva, Jana Wagemaker, and Fabio Zanasi. Concurrent Kleene Algebra with Observations: From Hypotheses to Completeness, volume 12077 of Lecture Notes in Computer Science, pages 381-400. Springer International Publishing, Cham, 2020. URL: https://doi.org/10.1007/978-3-030-45231-5_20.
  12. Tobias Kappé, Paul Brunet, Alexandra Silva, and Fabio Zanasi. Concurrent kleene algebra: Free model and completeness. In Amal Ahmed, editor, Programming Languages and Systems, Lecture Notes in Computer Science, pages 856-882, Cham, 2018. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-89884-1_30.
  13. Dexter Kozen. On kleene algebras and closed semirings. In Branislav Rovan, editor, Mathematical Foundations of Computer Science 1990, volume 452, pages 26-47. Springer-Verlag, Berlin/Heidelberg, 1990. URL: https://doi.org/10.1007/BFb0029594.
  14. Dexter Kozen. Kleene algebra with tests and commutativity conditions, volume 1055 of Lecture Notes in Computer Science, pages 14-33. Springer Berlin Heidelberg, Berlin, Heidelberg, 1996. URL: https://doi.org/10.1007/3-540-61042-1_35.
  15. Dexter Kozen. On the complexity of reasoning in kleene algebra. In Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29 - July 2, 1997, pages 195-202. IEEE Computer Society, 1997. URL: https://doi.org/10.1109/LICS.1997.614947.
  16. Dexter Kozen and Alexandra Silva. Left-handed completeness. Theoretical Computer Science, 807:220-233, February 2020. URL: https://doi.org/10.1016/j.tcs.2019.10.040.
  17. Stepan L. Kuznetsov. On the complexity of reasoning in kleene algebra with commutativity conditions. In Erika Ábrahám, Clemens Dubslaff, and Silvia Lizeth Tapia Tarifa, editors, Theoretical Aspects of Computing - ICTAC 2023 - 20th International Colloquium, Lima, Peru, December 4-8, 2023, Proceedings, volume 14446 of Lecture Notes in Computer Science, pages 83-99. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-47963-2_7.
  18. A. K. McIver, E. Cohen, and C. C. Morgan. Using Probabilistic Kleene Algebra for Protocol Verification, volume 4136 of Lecture Notes in Computer Science, pages 296-310. Springer Berlin Heidelberg, Berlin, Heidelberg, 2006. URL: https://doi.org/10.1007/11828563_20.
  19. Annabelle McIver, Tahiry M. Rabehaja, and Georg Struth. On probabilistic kleene algebras, automata and simulations. In Proceedings of the 12th International Conference on Relational and Algebraic Methods in Computer Science, RAMICS'11, pages 264-279, Berlin, Heidelberg, May 2011. Springer-Verlag. URL: https://doi.org/10.1007/978-3-642-21070-9_20.
  20. A.M Silva. Kleene coalgebra. s.n.; UB Nijmegen host, S.l.; Nijmegen, 2010. URL: http://hdl.handle.net/2066/83205.
  21. Cheng Zhang, Arthur Azevedo de Amorim, and Marco Gaboardi. On incorrectness logic and kleene algebra with top and tests. arxiv preprint, August 2022. https://arxiv.org/abs/2108.07707, URL: https://doi.org/10.48550/arXiv.2108.07707.
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