Completeness Theorems for Pomset Languages and Concurrent Kleene Algebras

Pomsets constitute one of the most basic models of concurrency. A pomset is a generalisation of a word over an alphabet in that letters may be partially ordered. A term $t$ using the bi-Kleene operations $0,1, +, \cdot, ,^, \parallel, ^{()}$definesalanguage$ \mathopen{[![ } t \mathclose{]!] } $ of pomsets in a natural way. We prove that every valid universal equality over pomset languages using these operations is a consequence of the equational theory of regular languages (in which parallel multiplication and iteration are undefined) plus that of the commutative-regular languages (in which sequential multiplication and iteration are undefined). We also show that the class of $\mathit{\text{rational}}$ pomset languages (that is, those languages generated from singleton pomsets using the bi-Kleene operations) is closed under all Boolean operations. An $\mathit{\text{ideal}}$ of a pomset $p$ is a pomset using the letters of $p$, but having an ordering at least as strict as $p$. A bi-Kleene term $t$ thus defines the set $\mathbf{\text{Id}}(t)$ of ideals of pomsets in $t$. We prove that if $t$ does not contain commutative iteration ${}^{(\ast )}$ (in our terminology, $t$ is bw-rational) then $$\mathbf{\text{Id}}$ (\mathopen{[![ } t \mathclose{]!] }) \cap $\mathbf{\text{Pom}}${sp}$,where$ $\mathbf{\text{Pom}}${sp}$ is the set of pomsets generated from singleton pomsets using sequential and parallel multiplication ($\cdot$ and $\parallel$) is defined by a bw-rational term, and if two such terms $t,t^{\mathrm{\prime }}$ define the same ideal language, then $t^{\mathrm{\prime }}=t$ is provable from the Kleene axioms for $0,1,+,\cdot {,}^{\ast }$ plus the commutative idempotent semiring axioms for $0,1,+,\parallel$ plus the exchange law $ (u \parallel v)\cdot ( x \parallel y) \le v \cdot y \parallel u \cdot x $.