Partially Observable Concurrent Kleene Algebra

conference paper, in CONCUR 2020

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.

Related talks

Avancées récentes sur les algèbres de Kleene concurrentes
séminaire du LACL in Créteil, December 2021
(in French)
.
More
Recent developments in concurrent Kleene algebra
JetBrains Research in St Petersburg (remote talk), October 2021
.
More
Avancées récentes sur les algèbres de Kleene concurrentes
Séminaire MAREL in Montpellier, April 2021
.
More
Avancées récentes sur les algèbres de Kleene concurrentes
Séminaire ACADIE in Toulouse, April 2021
.
More
Observations and locality in distributed processes
IRIS scientific meeting in London, March 2021
.
More
Avancées récentes sur les algèbres de Kleene concurrentes
séminaire LIRICA in Marseille, January 2021
(in French)
.
More
Avancées récentes sur les algèbres de Kleene concurrentes
Séminaire LOVE in Paris, January 2021
.
More
Recent developments in concurrent Kleene algebra
IRIS scientific meeting in London, December 2020
.
More
Pomsets with Boxes: Protection, Separation, and Locality in Concurrent Kleene Algebra
FSCD in Paris, July 2020
.
More
Recent developments in concurrent Kleene algebra
Séminaire PPS in Paris, June 2020
.
More
Pomsets with boxes: towards Atomic CKA
Highlights in Warsaw, September 2019
.
More
Pomset languages and concurrent Kleene algebra
Theory seminar - QMU in London, February 2018
.
More
Pomset languages and concurrent Kleene algebras
Séminaire automates in Paris, November 2017
.
More
On Decidability of Concurrent Kleene Algebra
CONCUR in Berlin, September 2017
.
More

Related papers

Equivalence checking for weak bi-Kleene algebra (in LMCS 2021)
with Tobias Kappé, Alexandra Silva, Bas Luttik and Fabio Zanasi.
More
Concurrent Kleene Algebra with Observations: From Hypotheses to Completeness (in FoSSaCS 2020)
with Tobias Kappé, Alexandra Silva, Fabio Zanasi and Jana Wagemaker.
More
Pomsets with Boxes: Protection, Separation, and Locality in Concurrent Kleene Algebra (in FSCD 2020)
with David Pym.
More
On Series-Parallel Pomset Languages: Rationality, Context-Freeness and Automata (in JLAMP 2019)
with Tobias Kappé, Alexandra Silva, Bas Luttik and Fabio Zanasi.
More
Kleene Algebra with Observations (in CONCUR 2019)
with Tobias Kappé, Alexandra Silva, Fabio Zanasi, Jurriaan Rot and Jana Wagemaker.
More
Concurrent Kleene Algebra: Free Model and Completeness (in ESOP 2018)
with Tobias Kappé, Alexandra Silva and Fabio Zanasi.
More
Brzozowski Goes Concurrent - A Kleene Theorem for Pomset Languages (in CONCUR 2017)
with Tobias Kappé, Alexandra Silva, Bas Luttik and Fabio Zanasi.
More
On Decidability of Concurrent Kleene Algebra (in CONCUR 2017)
with Damien Pous and Georg Struth.
More

Updated: