Concurrent Kleene Algebra with Observations: from Hypotheses to Completeness
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 -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
@article{arxiv.2002.09682,
title = {Concurrent Kleene Algebra with Observations: from Hypotheses to Completeness},
author = {Tobias Kappé and Paul Brunet and Alexandra Silva and Jana Wagemaker and Fabio Zanasi},
journal= {arXiv preprint arXiv:2002.09682},
year = {2023}
}