We take as starting point Kleene’s well-known theorem establishing a correspondence between regular expressions and finite automata: every language denoted by a regular expression is accepted by a finite automaton, and every language accepted by a finite automaton is denoted by a regular expression. We extend regular expressions with a parallel construct and finite automata with a fork construction and establish a Kleene correspondence between the two in pomset language semantics.

This may be considered as a first step towards a Kleene theorem for Concurrent Kleene Algebra (CKA), an extension of Kleene Algebra with a parallel construct, that was proposed by Hoare, Möller, Struth and Wehrman as a suitable formal framework for the study of concurrent programs. CKA does require a different semantics satisfying the so-called exchange law between sequential and parallel composition.

The talk is based on joint work with Tobias Kappé, Paul Brunet, Alexandra Silva and Fabio Zanasi, all from UCL.