Concurrent Kleene algebras (CKA) and bi-Kleene algebras support equational reasoning about computing systems with concurrent behaviours. Their natural semantics is given by series(-parallel) rational pomset languages, a standard true concurrency semantics, which is often associated with processes of Petri nets.In the first part of the talk, I will present a recent proof of completeness, showing that two series-rational expressions are equivalent according to the laws of CKA exactly when their pomset semantics are equal. In a second part, I will use Petri nets to reduce the problem of containment of languages of pomsets to the equivalence of finite state automata. In doing so, we prove decidability as well as provide tight complexity bounds.
Joint work with Damien Pous, Georg Struth, Tobias Kappé, Alexandra Silva, and Fabio Zanasi