Concurrent Kleene Algebra: Free Model and Completeness
Abstract
Concurrent Kleene Algebra (CKA) was introduced by Hoare, Moeller, Struth and Wehrman in 2009 as a framework to reason about concurrent programs. We prove that the axioms for CKA with bounded parallelism are complete for the semantics proposed in the original paper; consequently, these semantics are the free model for this fragment. This result settles a conjecture of Hoare and collaborators. Moreover, the techniques developed along the way are reusable; in particular, they allow us to establish pomset automata as an operational model for CKA.
Cite
@article{arxiv.1710.02787,
title = {Concurrent Kleene Algebra: Free Model and Completeness},
author = {Tobias Kappé and Paul Brunet and Alexandra Silva and Fabio Zanasi},
journal= {arXiv preprint arXiv:1710.02787},
year = {2023}
}
Comments
Version 2 includes an overview section that outlines the completeness proof, as well as some extra discussion of the interpolation lemma. It also includes better typography and a number of minor fixes. Version 3 incorporates the changes by comments from the anonymous referees at ESOP. Among other things, these include a worked example of computing the syntactic closure by hand