Document Open Access Logo

Reversible Kleene lattices

Author Paul Brunet

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2017.66.pdf
  • Filesize: 0.57 MB
  • 14 pages

Document Identifiers

Author Details

Paul Brunet

Cite As Get BibTex

Paul Brunet. Reversible Kleene lattices. In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 66:1-66:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.MFCS.2017.66

Abstract

We investigate the equational theory of reversible Kleene lattices, that is algebras of languages with the regular operations (union, composition and Kleene star), together with intersection and mirror image. Building on results by Andréka, Mikulás and Németi from 2011, we construct the free representation of this algebra. We then provide an automaton model to compare representations. These automata are adapted from Petri automata, which we introduced with Pous in 2015 to tackle a similar problem for algebras of binary relations. This allows us to show that testing the validity of 
equations in this algebra is decidable, and in fact ExpSpace-complete.

Subject Classification

Keywords
  • Kleene algebra
  • Automata
  • Petri nets
  • Decidability
  • Complexity
  • Formal languages
  • Lattice

Metrics

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

References

  1. Hajnal Andréka, Szabolcs Mikulás, and István Németi. The equational theory of Kleene lattices. TCS, 412(52):7099-7108, 2011. URL: http://dx.doi.org/10.1016/j.tcs.2011.09.024.
  2. Hajnal Andréka and Dmitry A. Bredikhin. The equational theory of union-free algebras of relations. Alg. Univ., 33(4):516-532, 1995. URL: http://dx.doi.org/10.1007/BF01225472.
  3. Stephen L. Bloom, Zoltán Ésik, and Gheorghe Stefanescu. Notes on equational theories of relations. Alg. Univ., 33(1):98-126, 1995. URL: http://dx.doi.org/10.1007/BF01190768.
  4. Paul Brunet. Algebras of Relations: From algorithms to formal proofs. PhD thesis, Université de Lyon, 2016. URL: https://tel.archives-ouvertes.fr/tel-01455083v1.
  5. Paul Brunet. Reversible Kleene lattices. extended abstract, 2017. URL: https://hal.archives-ouvertes.fr/hal-01474911.
  6. Paul Brunet and Damien Pous. Petri Automata for Kleene Allegories. In Proc. LICS, pages 68-79, July 2015. URL: http://dx.doi.org/10.1109/LICS.2015.17.
  7. Paul Brunet and Damien Pous. A formal exploration of Nominal Kleene Algebra. In Proc. MFCS, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.MFCS.2016.22.
  8. Paul Brunet and Damien Pous. Petri automata. Logical Methods in Computer Science, 2017. submitted. URL: http://arxiv.org/abs/1702.01804.
  9. John H. Conway. Regular algebra and finite machines. Chapman and Hall Mathematics Series, 1971. Google Scholar
  10. Zoltán Ésik and Laszlo Bernátsky. Equational properties of Kleene algebras of relations with conversion. TCS, 137(2):237-251, 1995. URL: http://dx.doi.org/10.1016/0304-3975(94)00041-G.
  11. Peter J. Freyd and Andre Scedrov. Categories, Allegories. NH, 1990. Google Scholar
  12. Martin Fürer. The complexity of the inequivalence problem for regular expressions with intersection. In Proc. ICALP, pages 234-245, 1980. URL: http://dx.doi.org/10.1007/3-540-10003-2_74.
  13. Murdoch J. Gabbay and Vincenzo Ciancia. Freshness and name-restriction in sets of traces with names. In Proc. FoSSaCS, pages 365-380. Springer, 2011. URL: http://dx.doi.org/10.1007/978-3-642-19805-2_25.
  14. Stephen C. Kleene. Representation of Events in Nerve Nets and Finite Automata. Memorandum. Rand Corporation, 1951. Google Scholar
  15. Dexter Kozen. A completeness theorem for Kleene Algebras and the algebra of regular events. In Proc. LICS, pages 214-225. IEEE Computer Society, 1991. URL: http://dx.doi.org/10.1109/LICS.1991.151646.
  16. Dexter Kozen. Kleene algebra with tests. Transactions on Programming Languages and Systems, 19(3):427-443, 1997. URL: http://dx.doi.org/10.1145/256167.256195.
  17. Dexter Kozen, Konstantinos Mamouras, Daniela Petrisan, and Alexandra Silva. Nominal Kleene coalgebra. In Proc. ICALP, pages 286-298. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-662-47666-6_23.
  18. Dexter Kozen, Konstantinos Mamouras, and Alexandra Silva. Completeness and incompleteness in nominal Kleene algebra. In Proc. RAMiCS, pages 51-66, 2015. URL: http://dx.doi.org/10.1007/978-3-319-24704-5_4.
  19. Albert R. Meyer and Larry J. Stockmeyer. The equivalence problem for regular expressions with squaring requires exponential space. In Proc. SWAT, pages 125-129, 1972. URL: http://dx.doi.org/10.1109/SWAT.1972.29.
  20. Volodimir N. Redko. On defining relations for the algebra of regular events. Ukrainskii Matematicheskii Zhurnal, pages 120-126, 1964. Google Scholar
  21. Arto Salomaa. Two complete axiom systems for the algebra of regular events. J. ACM, 13(1):158-169, 1966. URL: http://dx.doi.org/10.1145/321312.321326.
  22. Walter J. Savitch. Relationships between nondeterministic and deterministic tape complexities. Journal of computer and system sciences, 4(2):177-192, 1970. URL: http://dx.doi.org/10.1016/S0022-0000(70)80006-X.
  23. Jacobo Valdes, Robert E. Tarjan, and Eugene L. Lawler. The recognition of series parallel digraphs. In Proc. STOC, STOC '79, 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-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact