Document Open Access Logo

On Decidability of Concurrent Kleene Algebra

Authors Paul Brunet, Damien Pous, Georg Struth

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2017.28.pdf
  • Filesize: 0.57 MB
  • 15 pages

Document Identifiers

Subject Classification

Keywords
  • Concurrent Kleene algebra
  • series-parallel pomsets
  • Petri nets

Metrics

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

Abstract

Concurrent Kleene algebras support equational reasoning about
computing systems with concurrent behaviours. Their natural
semantics is given by series(-parallel) rational pomset languages, a
standard true concurrency semantics, which is often associated with
processes of Petri nets. We use constructions on Petri nets to
provide two decision procedures for such pomset languages motivated
by the equational and the refinement theory of concurrent Kleene
algebra. The contribution to the first problem lies in a much
simpler algorithm and an EXPSPACE complexity bound. Decidability
of the second, more interesting problem is new and, in fact,
EXPSPACE-complete.

Cite As Get BibTex

Paul Brunet, Damien Pous, and Georg Struth. On Decidability of Concurrent Kleene Algebra. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 28:1-28:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.CONCUR.2017.28

Author Details

Paul Brunet
Damien Pous
Georg Struth

References

  1. Maurice Boffa. Une remarque sur les systèmes complets d'identités rationnelles. Informatique Théorique et Applications, 24:419-428, 1990. URL: http://archive.numdam.org/article/ITA_1990__24_4_419_0.pdf.
  2. Maurice Boffa. Une condition impliquant toutes les identités rationnelles. Informatique Théorique et Applications, 29(6):515-518, 1995. Google Scholar
  3. Paul Brunet, Damien Pous, and Georg Struth. On decidability of concurrent Kleene algebra, 2017. Full version of this extended abstract, with proofs. URL: https://hal.archives-ouvertes.fr/hal-01558108/.
  4. J. H. Conway. Regular algebra and finite machines. Chapman and Hall, 1971. Google Scholar
  5. Jay L. Gischer. The equational theory of pomsets. Theoretical Computer Science, 61(2):199-224, 1988. URL: http://dx.doi.org/10.1016/0304-3975(88)90124-7.
  6. J. Grabowski. On partial languages. Fundamenta Informaticae, 4:427-498, 1981. Google Scholar
  7. Christoph Haase and Piotr Hofman. Tightening the complexity of equivalence problems for commutative grammars. In STACS, volume 47 of LIPIcs, pages 41:1-41:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. Google Scholar
  8. T. Hoare, B. Möller, G. Struth, and I. Wehrman. Concurrent Kleene algebra and its foundations. Journal of Logic and Algebraic Programming, 80(6):266-296, 2011. Google Scholar
  9. A. Horn and D. Kroening. On partial order semantics for SAT/SMT-based symbolic encodings of weak memory concurrency. In FORTE, volume 9039 of Lecture Notes in Computer Science, pages 19-34. Springer Verlag, 2015. Google Scholar
  10. Lalita Jategaonkar and Albert R. Meyer. Deciding true concurrency equivalences on safe, finite nets. Theoretical Computer Science, 154(1):107-143, 1996. URL: http://dx.doi.org/10.1016/0304-3975(95)00132-8.
  11. Dexter Kozen. A completeness theorem for Kleene algebras and the algebra of regular events. In LICS, pages 214-225. IEEE, 1991. URL: http://dx.doi.org/10.1109/LICS.1991.151646.
  12. Daniel Krob. A Complete System of B-Rational Identities. In ICALP, volume 443 of Lecture Notes in Computer Science, pages 60-73. Springer Verlag, 1990. URL: http://dx.doi.org/10.1007/BFb0032022.
  13. Michael R. Laurence and Georg Struth. Completeness theorems for bi-Kleene algebras and series-parallel rational pomset languages. In RAMiCS, volume 8428 of Lecture Notes in Computer Science, pages 65-82. Springer Verlag, 2014. URL: http://dx.doi.org/10.1007/978-3-319-06251-8_5.
  14. K. Lodaya, D. Ranganayakulu, and K. Rangarajan. Hierarchical structure of 1-safe petri nets. In ASIAN, Progamming Languages and Distributed Computation, pages 173-187. Springer Verlag, 2003. URL: http://dx.doi.org/10.1007/978-3-540-40965-6_12.
  15. Kamal Lodaya and Pascal Weil. Series–parallel languages and the bounded-width property. Theoretical Computer Science, 237(1):347-380, 2000. URL: http://dx.doi.org/10.1016/S0304-3975(00)00031-1.
  16. Alain J. Mayer and Larry J. Stockmeyer. The complexity of word problems - this time with interleaving. Information and Computation, 115(2):293-311, 1994. URL: http://dx.doi.org/10.1006/inco.1994.1098.
  17. 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: http://dx.doi.org/10.1109/SWAT.1972.29.
  18. K. Thompson. Regular expression search algorithm. Communications of the ACM, 11:419-422, 1968. URL: http://www.fing.edu.uy/inco/cursos/intropln/material/p419-thompson.pdf.
  19. 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