Completeness and Incompleteness of Synchronous Kleene Algebra
Logic in Computer Science
2023-02-03 v2
Abstract
Synchronous Kleene algebra (SKA), an extension of Kleene algebra (KA), was proposed by Prisacariu as a tool for reasoning about programs that may execute synchronously, i.e., in lock-step. We provide a countermodel witnessing that the axioms of SKA are incomplete w.r.t. its language semantics, by exploiting a lack of interaction between the synchronous product operator and the Kleene star. We then propose an alternative set of axioms for SKA, based on Salomaa's axiomatisation of regular languages, and show that these provide a sound and complete characterisation w.r.t. the original language semantics.
Cite
@article{arxiv.1905.08554,
title = {Completeness and Incompleteness of Synchronous Kleene Algebra},
author = {Jana Wagemaker and Marcello Bonsangue and Tobias Kappé and Jurriaan Rot and Alexandra Silva},
journal= {arXiv preprint arXiv:1905.08554},
year = {2023}
}
Comments
Accepted at MPC 2019