Brzozowski goes concurrent: A Kleene Theorem for pomset languages

T. Kappé, P. Brunet, Bas Luttik, A. Silva, F. Zanasi

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

4 Citations (Scopus)
45 Downloads (Pure)


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.
Original languageEnglish
Title of host publication28th International Conference on Concurrency Theory (CONCUR 2017)
EditorsRoland Meyer, Uwe Nestmann
Place of PublicationDagstuhl
PublisherSchloss Dagstuhl - Leibniz-Zentrum für Informatik
Number of pages16
ISBN (Electronic)9783959770484
Publication statusPublished - 1 Aug 2017
Event28th International Conference on Concurrency Theory, CONCUR 2017 - Berlin, Germany
Duration: 5 Sept 20178 Sept 2017

Publication series

NameLeibniz International Proceedings in Informatics (LIPIcs)
PublisherSchloss Dagstuhl--Leibniz-Zentrum fuer Informatik


Conference28th International Conference on Concurrency Theory, CONCUR 2017


  • Automata
  • Brzozowski derivatives
  • Concurrency
  • Kleene theorem
  • Pomsets
  • Series-rational expressions


Dive into the research topics of 'Brzozowski goes concurrent: A Kleene Theorem for pomset languages'. Together they form a unique fingerprint.

Cite this