Concurrent Kleene Algebra: Free Model and Completeness
arXiv:1710.02787 · doi:10.1007/978-3-319-89884-1_30
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.
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
References in corpus (2)
Cited by in corpus (12)
- Concurrent Kleene Algebra: Free Model and Completeness
- On Series-Parallel Pomset Languages: Rationality, Context-Freeness and Automata
- Learning Pomset Automata
- Deconstructing the Calculus of Relations with Tape Diagrams
- Partially Observable Concurrent Kleene Algebra
- Concurrent NetKAT: Modeling and analyzing stateful, concurrent networks
- A Finite Axiomatisation of Finite-State Automata Using String Diagrams
- Concurrent Kleene Algebra with Observations: from Hypotheses to Completeness
- Completeness and Incompleteness of Synchronous Kleene Algebra
- On Star Expressions and Coalgebraic Completeness Theorems
- Equivalence checking for weak bi-Kleene algebra
- How to write a coequation