Concurrent Kleene Algebra: Free Model and Completeness
Tobias Kapp\'e, Paul Brunet, Alexandra Silva, Fabio Zanasi
TL;DR
This paper proves the completeness of the axioms for Concurrent Kleene Algebra with bounded parallelism, establishing the semantics as the free model and introducing pomset automata as an operational model.
Contribution
It demonstrates the completeness of CKA axioms with bounded parallelism and introduces pomset automata as an operational semantics.
Findings
CKA axioms are complete for the bounded parallelism fragment
Semantics are proven to be the free model for this fragment
Pomset automata are established as an operational model
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.