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 technique developed to this end allows us to establish a Kleene Theorem for CKA, extending an earlier Kleene Theorem for a fragment of CKA. |
Year | DOI | Venue |
---|---|---|
2018 | 10.1007/978-3-319-89884-1_30 | ESOP |
DocType | Volume | Citations |
Conference | abs/1710.02787 | 1 |
PageRank | References | Authors |
0.36 | 11 | 4 |
Name | Order | Citations | PageRank |
---|---|---|---|
Tobias Kappé | 1 | 3 | 3.11 |
Paul Brunet | 2 | 4 | 3.81 |
Alexandra Silva | 3 | 37 | 4.17 |
Fabio Zanasi | 4 | 110 | 13.89 |