2026-07-23T06:31:08Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:12832 2024-03-06T10:50:48Z ddc:004 open_access

Partially Observable Concurrent Kleene Algebra Wagemaker, Jana Brunet, Paul Docherty, Simon Kappé, Tobias Rot, Jurriaan Silva, Alexandra Concurrent Kleene algebra Kleene algebra with tests observations axiomatisation completeness sequential consistency 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Jana Wagemaker and Paul Brunet and Simon Docherty and Tobias Kappé and Jurriaan Rot and Alexandra Silva 2020 Is Part Of LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2020.20 urn:nbn:de:0030-drops-128324 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.20 eng https://creativecommons.org/licenses/by/3.0/legalcode