# Brzozowski Goes Concurrent - A Kleene Theorem for Pomset Languages

## TL;DR

This paper introduces a new automaton model and a Kleene-like theorem for Concurrent Kleene Algebra, advancing the understanding of concurrent program behaviors and their formal language representations.

## Contribution

It presents a novel automaton construction using Brzozowski derivatives and characterizes automata that represent valid CKA behaviors, addressing a longstanding open problem.

## Key findings

- Automaton model for CKA behaviors established
- Kleene-like theorem relating CKA to pomset languages proved
- Syntactic characterization of automata for CKA behaviors provided

## 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.