Partially Observable Concurrent Kleene Algebra
Logic in Computer Science
2023-02-06 v2 Formal Languages and Automata Theory
Programming Languages
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.
Cite
@article{arxiv.2007.07593,
title = {Partially Observable Concurrent Kleene Algebra},
author = {Jana Wagemaker and Paul Brunet and Simon Docherty and Tobias Kappé and Jurriaan Rot and Alexandra Silva},
journal= {arXiv preprint arXiv:2007.07593},
year = {2023}
}
Comments
Accepted for publication at CONCUR 2020