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 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.
Cite
CITATION STYLE
Kappé, T., Brunet, P., Silva, A., Wagemaker, J., & Zanasi, F. (2020). Concurrent Kleene Algebra with Observations: From Hypotheses to Completeness. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 12077 LNCS, pp. 381–400). Springer. https://doi.org/10.1007/978-3-030-45231-5_20
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
