Name
Abstract | ||
|---|---|---|
Concurrent Kleene Algebra (CKA) extends basic Kleene algebra with a parallel composition operator, which enables reasoning about concurrent programs. However, CKA fundamentally misses tests, which are needed to model standard programming constructs such as conditionals and $\mathsf{while}$-loops. It turns out that integrating tests in CKA is subtle, due to their interaction with parallelism. In this paper we provide a solution in the form of Concurrent Kleene Algebra with Observations (CKAO). Our main contribution is a completeness theorem for CKAO. Our result resorts on a more general study of CKA "with hypotheses", of which CKAO turns out to be an instance: this analysis is of independent interest, as it can be applied to extensions of CKA other than CKAO. |
Year | DOI | Venue |
|---|---|---|
2020 | 10.1007/978-3-030-45231-5_20 | FoSSaCS |
DocType | Citations | PageRank |
Conference | 0 | 0.34 |
References | Authors | |
0 | 5 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Kappé Tobias | 1 | 0 | 0.34 |
| Brunet Paul | 2 | 0 | 0.34 |
| Alexandra Silva | 3 | 31 | 9.71 |
| Wagemaker Jana | 4 | 0 | 0.34 |
| Fabio Zanasi | 5 | 110 | 13.89 |