Wagemaker, J;
Brunet, P;
Docherty, S;
Kappé, T;
Rot, J;
Silva, A;
(2020)
Partially Observable Concurrent Kleene Algebra.
In:
31st International Conference on Concurrency Theory (CONCUR 2020).
(pp. 20:1-20:22).
Schloss Dagstuhl--Leibniz-Zentrum für Informatik: Dagstuhl, Germany.
Preview |
Text
Kappé_LIPIcs-CONCUR-2020-20.pdf - Published Version Download (652kB) | Preview |
Abstract
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.
| Type: | Proceedings paper |
|---|---|
| Title: | Partially Observable Concurrent Kleene Algebra |
| Event: | 31st International Conference on Concurrency Theory (CONCUR 2020) |
| ISBN-13: | 978-3-95977-160-3 |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.4230/LIPIcs.CONCUR.2020.20 |
| Publisher version: | https://doi.org/10.4230/LIPIcs.CONCUR.2020.20 |
| Language: | English |
| Additional information: | Copyright © Jana Wagemaker, Paul Brunet, Simon Docherty, Tobias Kappé, Jurriaan Rot, and Alexandra Silva; licensed under Creative Commons License CC-BY (https://creativecommons.org/licenses/by/3.0/legalcode). |
| Keywords: | Concurrent Kleene algebra, Kleene algebra with tests, observations, axiomatisation, completeness, sequential consistency |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/10109360 |
Archive Staff Only
 |
View Item |
