Partially Observable Concurrent Kleene Algebra

TL;DR

This paper introduces POCKA, an algebraic framework for reasoning about concurrent programs with control structures and partial observations, providing soundness, completeness, and sequential consistency validation.

Contribution

The paper presents POCKA, a novel algebraic system that models partial observations in concurrent programs with control flow, extending previous algebraic frameworks.

Findings

POCKA is sound and complete for its model.

The semantics of POCKA passes sequential consistency checks.

Concrete examples demonstrate POCKA's applicability.

Abstract

We introduce partially observable concurrent Kleene algebra (POCKA), an algebraic framework to reason about concurrent programs with control structures, such as conditionals and loops. POCKA enables reasoning about programs that can access variables and values, which we illustrate through concrete examples. We prove that POCKA is a sound and complete axiomatisation of a model of partial observations, and show the semantics passes an important check for sequential consistency.