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 conditional and while-loops. It turns out integrating tests in CKA is subtle, due to their interaction with parallel threads. 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.
@inproceedings{kbswz20,
title = "Concurrent Kleene Algebra with Observations: From Hypotheses to Completeness",
author = "{Paul Brunet}, {Tobias Kappé}, {Alexandra Silva}, {Fabio Zanasi}, {Jana Wagemaker}",
year = 2020,
booktitle = "FoSSaCS",
doi = "10.1007/978-3-030-45231-5_20"
}
