Partially Observable Concurrent Kleene Algebra
Jana Wagemaker, Brunet, Paul, Simon Docherty, Tobias Kappé, Jurriaan Rot, Alexandra Silva · arXiv (Cornell University) · 2020
We introduce partially observable concurrent Kleene algebra (POCKA), an algebraic framework to reason about concurrent programs with variables as well as control structures, such as conditionals and loops, that depend on those variables. We illustrate the use of POCKA 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.