Document Open Access Logo

Brzozowski Goes Concurrent - A Kleene Theorem for Pomset Languages

Authors Tobias Kappé, Paul Brunet, Bas Luttik, Alexandra Silva, Fabio Zanasi

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2017.25.pdf
  • Filesize: 0.56 MB
  • 16 pages

Document Identifiers

Author Details

Tobias Kappé
Paul Brunet
Bas Luttik
Alexandra Silva
Fabio Zanasi

Cite AsGet BibTex

Tobias Kappé, Paul Brunet, Bas Luttik, Alexandra Silva, and Fabio Zanasi. Brzozowski Goes Concurrent - A Kleene Theorem for Pomset Languages. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 25:1-25:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.CONCUR.2017.25

Abstract

Concurrent Kleene Algebra (CKA) is a mathematical formalism to study programs that exhibit concurrent behaviour. As with previous extensions of Kleene Algebra, characterizing the free model is crucial in order to develop the foundations of the theory and potential applications. For CKA, this has been an open question for a few years and this paper makes an important step towards an answer. We present a new automaton model and a Kleene-like theorem that relates a relaxed version of CKA to series-parallel pomset languages, which are a natural candidate for the free model. There are two substantial differences with previous work: from expressions to automata, we use Brzozowski derivatives, which enable a direct construction of the automaton; from automata to expressions, we provide a syntactic characterization of the automata that denote valid CKA behaviours.
Keywords
  • Kleene theorem
  • Series-rational expressions
  • Automata
  • Brzozowski derivatives
  • Concurrency
  • Pomsets

Metrics

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

References

  1. Carolyn Jane Anderson, Nate Foster, Arjun Guha, Jean-Baptiste Jeannin, Dexter Kozen, Cole Schlesinger, and David Walker. NetKAT: semantic foundations for networks. In Proc. Principles of Programming Languages (POPL), pages 113-126, 2014. URL: http://dx.doi.org/10.1145/2535838.2535862.
  2. Sabine Broda, Sílvia Cavadas, Miguel Ferreira, and Nelma Moreira. Deciding synchronous Kleene algebra with derivatives. In Proc. Implementation and Application of Automata (CIAA), pages 49-62, 2015. URL: http://dx.doi.org/10.1007/978-3-319-22360-5_5.
  3. Janusz A. Brzozowski. Derivatives of regular expressions. J. ACM, 11(4):481-494, 1964. URL: http://dx.doi.org/10.1145/321239.321249.
  4. Jay L. Gischer. The equational theory of pomsets. Theor. Comput. Sci., 61:199-224, 1988. URL: http://dx.doi.org/10.1016/0304-3975(88)90124-7.
  5. C. A. R. Hoare, Bernhard Möller, Georg Struth, and Ian Wehrman. Concurrent Kleene Algebra. In Proc. Concurrency Theory (CONCUR), pages 399-414, 2009. URL: http://dx.doi.org/10.1007/978-3-642-04081-8_27.
  6. Tony Hoare, Stephan van Staden, Bernhard Möller, Georg Struth, and Huibiao Zhu. Developments in Concurrent Kleene Algebra. J. Log. Algebr. Meth. Program., 85(4):617-636, 2016. URL: http://dx.doi.org/10.1016/j.jlamp.2015.09.012.
  7. Peter Jipsen. Concurrent Kleene Algebra with tests. In Proc. Relational and Algebraic Methods in Computer Science (RAMiCS) 2014, pages 37-48, 2014. URL: http://dx.doi.org/10.1007/978-3-319-06251-8_3.
  8. Peter Jipsen and M. Andrew Moshier. Concurrent Kleene Algebra with tests and branching automata. J. Log. Algebr. Meth. Program., 85(4):637-652, 2016. URL: http://dx.doi.org/10.1016/j.jlamp.2015.12.005.
  9. Tobias Kappé, Paul Brunet, Bas Luttik, Alexandra Silva, and Fabio Zanasi. Brzozowski goes concurrent - a Kleene theorem for pomset languages. CoRR, abs/1704.07199, 2017. URL: http://arxiv.org/abs/1704.07199.
  10. Stephen C. Kleene. Representation of events in nerve nets and finite automata. Automata Studies, pages 3-41, 1956. Google Scholar
  11. Dexter Kozen. A completeness theorem for Kleene Algebras and the algebra of regular events. Inf. Comput., 110(2):366-390, 1994. URL: http://dx.doi.org/10.1006/inco.1994.1037.
  12. Dexter Kozen. Automata and computability. Undergraduate texts in computer science. Springer, 1997. Google Scholar
  13. Dexter Kozen. Kleene Algebra with tests. ACM Trans. Program. Lang. Syst., 19(3):427-443, 1997. URL: http://dx.doi.org/10.1145/256167.256195.
  14. Michael R. Laurence and Georg Struth. Completeness theorems for Bi-Kleene Algebras and series-parallel rational pomset languages. In Proc. Relational and Algebraic Methods in Computer Science (RAMiCS), pages 65-82, 2014. URL: http://dx.doi.org/10.1007/978-3-319-06251-8_5.
  15. Kamal Lodaya and Pascal Weil. Series-parallel posets: Algebra, automata and languages. In Proc. Annual Symposium on Theoretical Aspects of Computer Science (STACS), pages 555-565, 1998. URL: http://dx.doi.org/10.1007/BFb0028590.
  16. 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.
  17. Cristian Prisacariu. Synchronous Kleene algebra. J. Log. Algebr. Program., 79(7):608-635, 2010. URL: http://dx.doi.org/10.1016/j.jlap.2010.07.009.
  18. Jurriaan Rot, Marcello M. Bonsangue, and Jan J. M. M. Rutten. Coalgebraic bisimulation-up-to. In Proc. Current Trends in Theory and Practice of Computer Science (SOFSEM), pages 369-381, 2013. URL: http://dx.doi.org/10.1007/978-3-642-35843-2_32.
  19. Ken Thompson. Regular expression search algorithm. Commun. ACM, 11(6):419-422, 1968. URL: http://dx.doi.org/10.1145/363347.363387.
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 Imprint Privacy Contact