# Concurrent Kleene Algebra with Observations: from Hypotheses to Completeness

arXiv: https://arxiv.org/abs/2002.09682 · HTML: https://mlsanity.com/paper/2002.09682/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 22 Feb 2020.

## Built on by (most cited first, 1 of 1)

- [Kleene algebra with commutativity conditions is undecidable](https://mlsanity.com/paper/2411.15979/) (2024)

## Abstract (arXiv)

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 mathsfwhile-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.