Completeness for Identity-free Kleene Lattices

Authors Amina Doumane, Damien Pous

Thumbnail PDF


  • Filesize: 0.56 MB
  • 17 pages

Document Identifiers

Author Details

Amina Doumane
  • Univ Lyon, CNRS, ENS de Lyon, UCB Lyon 1, LIP, Lyon, France
Damien Pous
  • Univ Lyon, CNRS, ENS de Lyon, UCB Lyon 1, LIP, Lyon, France

Cite AsGet BibTex

Amina Doumane and Damien Pous. Completeness for Identity-free Kleene Lattices. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 18:1-18:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


We provide a finite set of axioms for identity-free Kleene lattices, which we prove sound and complete for the equational theory of their relational models. Our proof builds on the completeness theorem for Kleene algebra, and on a novel automata construction that makes it possible to extract axiomatic proofs using a Kleene-like algorithm.

Subject Classification

ACM Subject Classification
  • Theory of computation → Regular languages
  • Kleene algebra
  • Graph languages
  • Petri Automata
  • Kleene theorem


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


  1. C. J. Anderson, N. Foster, A. Guha, J.-B. Jeannin, D. Kozen, C. Schlesinger, and D. Walker. Netkat: semantic foundations for networks. In POPL, pages 113-126. ACM, 2014. URL:
  2. H. Andréka, S. Mikulás, and I. Németi. The equational theory of Kleene lattices. Theoretical Computer Science, 412(52):7099-7108, 2011. URL:
  3. H. Andréka and Sz. Mikulás. Axiomatizability of positive algebras of binary relations. Algebra Universalis, 66(1):7-34, 2011. URL:
  4. H. Andréka. Representation of distributive lattice-ordered semigroups with binary relations. Algebra Universalis, 28:12-25, 1991. Google Scholar
  5. H. Andréka and D.A. Bredikhin. The equational theory of union-free algebras of relations. Algebra Universalis, 33(4):516-532, 1995. URL:
  6. A. Angus and D. Kozen. Kleene algebra with tests and program schematology. Technical Report TR2001-1844, CS Dpt., Cornell University, July 2001. URL:
  7. A. Armstrong, G. Struth, and T. Weber. Programming and automating mathematics in the Tarski-Kleene hierarchy. Journal of Logical and Algebraic Methods in Programming, 83(2):87-102, 2014. URL:
  8. Maurice Boffa. Une condition impliquant toutes les identités rationnelles. Informatique Théorique et Applications, 29(6):515-518, 1995. URL:
  9. Thomas Braibant and Damien Pous. Deciding Kleene algebras in Coq. Logical Methods in Computer Science, 8(1):1-16, 2012. URL:
  10. Paul Brunet and Damien Pous. Petri automata for Kleene allegories. In LICS, pages 68-79. ACM, 2015. URL:
  11. Paul Brunet and Damien Pous. Petri automata. Logical Methods in Computer Science, Volume 13, Issue 3, 2017. URL:
  12. J. H. Conway. Regular algebra and finite machines. Chapman and Hall, 1971. Google Scholar
  13. Amina Doumane and Damien Pous. Completeness for identity-free kleene lattices. Full version of this extended abstract, available at, 2018.
  14. S. Foster, G. Struth, and T. Weber. Automated engineering of relational and algebraic methods in Isabelle/HOL - (invited tutorial). In RAMiCS, volume 6663 of LNCS, pages 52-67. Springer, 2011. URL:
  15. P.J. Freyd and A. Scedrov. Categories, Allegories. North Holland. Elsevier, 1990. Google Scholar
  16. C. A. R. Hoare, B. Möller, G. Struth, and I. Wehrman. Concurrent Kleene algebra. In CONCUR, volume 5710 of LNCS, pages 399-414. Springer, 2009. URL:
  17. P. Höfner and G. Struth. On automating the calculus of relations. In IJCAR, volume 5195 of LNCS, pages 50-66. Springer, 2008. URL:
  18. Tobias Kappé, Paul Brunet, Alexandra Silva, and Fabio Zanasi. Concurrent kleene algebra: Free model and completeness. In ESOP, volume 10801 of LNCS, pages 856-882. Springer, 2018. URL:
  19. D. Kozen. A completeness theorem for Kleene algebras and the algebra of regular events. Information and Computation, 110(2):366-390, 1994. URL:
  20. D. Kozen. Kleene algebra with tests. Transactions on Programming Languages and Systems, 19(3):427-443, May 1997. URL:
  21. D. Kozen. On Hoare logic and Kleene algebra with tests. ACM Trans. Comput. Log., 1(1):60-76, 2000. URL:
  22. D. Kozen and M.-C. Patron. Certification of compiler optimizations using Kleene algebra with tests. In CL2000, volume 1861 of Lecture Notes in Artificial Intelligence, pages 568-582. Springer, 2000. URL:
  23. Dexter Kozen. Typed Kleene algebra. Technical Report TR98-1669, CS Dpt., Cornell University, 1998. URL:
  24. Dexter Kozen, Konstantinos Mamouras, and Alexandra Silva. Completeness and incompleteness in nominal kleene algebra. J. Log. Algebr. Meth. Program., 91:17-32, 2017. URL:
  25. A. Krauss and T. Nipkow. Proof pearl: Regular expression equivalence and relation algebra. Journal of Algebraic Reasoning, 49(1):95-106, 2012. URL:
  26. D. Krob. Complete systems of B-rational identities. Theoretical Computer Science, 89(2):207-343, 1991. URL:
  27. Michael R. Laurence and Georg Struth. Completeness theorems for pomset languages and concurrent kleene algebras. CoRR, abs/1705.05896, 2017. URL:
  28. Damien Pous. Kleene Algebra with Tests and Coq tools for while programs. In ITP, volume 7998 of LNCS, pages 180-196. Springer, 2013. URL:
  29. V. R. Pratt. Dynamic algebras and the nature of induction. In STOC, pages 22-28. ACM, 1980. URL:
  30. Volodimir Nikiforovych Redko. On defining relations for the algebra of regular events. Ukrainskii Matematicheskii Zhurnal, 16:120-126, 1964. Google Scholar
  31. Jacobo Valdes, Robert E. Tarjan, and Eugene L. Lawler. The recognition of series parallel digraphs. In STOC, pages 1-12. ACM, 1979. URL:
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail