Document Open Access Logo

Completeness for Identity-free Kleene Lattices

Authors Amina Doumane, Damien Pous

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2018.18.pdf
  • Filesize: 0.56 MB
  • 17 pages

Document Identifiers

Related Versions

Subject Classification

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

Metrics

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

Abstract

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.

Cite As Get 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) https://doi.org/10.4230/LIPIcs.CONCUR.2018.18

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

Funding

This work has been funded by the European Research Council (ERC) under the European Union’s Horizon 2020 programme (CoVeCe, grant agreement No 678157). This work was supported by the LABEX MILYON (ANR-10-LABX-0070) of Université de Lyon, within the program "Investissements d'Avenir" (ANR-11-IDEX-0007) operated by the French National Research Agency (ANR).

References

  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: http://dx.doi.org/10.1145/2535838.2535862.
  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: http://dx.doi.org/10.1016/j.tcs.2011.09.024.
  3. H. Andréka and Sz. Mikulás. Axiomatizability of positive algebras of binary relations. Algebra Universalis, 66(1):7-34, 2011. URL: http://dx.doi.org/10.1007/s00012-011-0142-3.
  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: http://dx.doi.org/10.1007/BF01225472.
  6. A. Angus and D. Kozen. Kleene algebra with tests and program schematology. Technical Report TR2001-1844, CS Dpt., Cornell University, July 2001. URL: http://hdl.handle.net/1813/5831.
  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: http://dx.doi.org/10.1016/j.jlap.2014.02.001.
  8. Maurice Boffa. Une condition impliquant toutes les identités rationnelles. Informatique Théorique et Applications, 29(6):515-518, 1995. URL: http://archive.numdam.org/.../ITA_1995__29_6_515_0.pdf.
  9. Thomas Braibant and Damien Pous. Deciding Kleene algebras in Coq. Logical Methods in Computer Science, 8(1):1-16, 2012. URL: http://dx.doi.org/10.2168/LMCS-8(1:16)2012.
  10. Paul Brunet and Damien Pous. Petri automata for Kleene allegories. In LICS, pages 68-79. ACM, 2015. URL: http://dx.doi.org/10.1109/LICS.2015.17.
  11. Paul Brunet and Damien Pous. Petri automata. Logical Methods in Computer Science, Volume 13, Issue 3, 2017. URL: http://dx.doi.org/10.23638/LMCS-13(3:33)2017.
  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 https://hal.archives-ouvertes.fr/hal-01780845, 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: http://dx.doi.org/10.1007/978-3-642-21070-9_5.
  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: http://dx.doi.org/10.1007/978-3-642-04081-8_27.
  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: http://dx.doi.org/10.1007/978-3-540-71070-7_5.
  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: http://dx.doi.org/10.1007/978-3-319-89884-1_30.
  19. D. Kozen. A completeness theorem for Kleene algebras and the algebra of regular events. Information and Computation, 110(2):366-390, 1994. URL: http://dx.doi.org/10.1006/inco.1994.1037.
  20. D. Kozen. Kleene algebra with tests. Transactions on Programming Languages and Systems, 19(3):427-443, May 1997. URL: http://dx.doi.org/10.1145/256167.256195.
  21. D. Kozen. On Hoare logic and Kleene algebra with tests. ACM Trans. Comput. Log., 1(1):60-76, 2000. URL: http://dx.doi.org/10.1145/343369.343378.
  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: http://dx.doi.org/10.1007/3-540-44957-4_38.
  23. Dexter Kozen. Typed Kleene algebra. Technical Report TR98-1669, CS Dpt., Cornell University, 1998. URL: http://www.cs.cornell.edu/~kozen/papers/typed.pdf.
  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: http://dx.doi.org/10.1016/j.jlamp.2017.06.002.
  25. A. Krauss and T. Nipkow. Proof pearl: Regular expression equivalence and relation algebra. Journal of Algebraic Reasoning, 49(1):95-106, 2012. URL: http://dx.doi.org/10.1007/s10817-011-9223-4.
  26. D. Krob. Complete systems of B-rational identities. Theoretical Computer Science, 89(2):207-343, 1991. URL: http://dx.doi.org/10.1016/0304-3975(91)90395-I.
  27. Michael R. Laurence and Georg Struth. Completeness theorems for pomset languages and concurrent kleene algebras. CoRR, abs/1705.05896, 2017. URL: http://arxiv.org/abs/1705.05896.
  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: http://dx.doi.org/10.1007/978-3-642-39634-2_15.
  29. V. R. Pratt. Dynamic algebras and the nature of induction. In STOC, pages 22-28. ACM, 1980. URL: http://dx.doi.org/10.1145/800141.804649.
  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: http://dx.doi.org/10.1145/800135.804393.
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