Wagemaker, J;
Bonsangue, M;
Kappé, T;
Rot, J;
Silva, A;
(2019)
Completeness and Incompleteness of Synchronous Kleene Algebra.
In:
Mathematics of Program Construction.
(pp. pp. 385-413).
Springer: Cham, Switzerland.
Preview |
Text
1905.08554v2.pdf - Accepted Version Download (333kB) | Preview |
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.
| Type: | Proceedings paper |
|---|---|
| Title: | Completeness and Incompleteness of Synchronous Kleene Algebra |
| Event: | International Conference on Mathematics of Program Construction (MPC 2019) |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1007/978-3-030-33636-3_14 |
| Publisher version: | https://doi.org/10.1007/978-3-030-33636-3_14 |
| Language: | English |
| Additional information: | This version is the author accepted manuscript. For information on re-use, please refer to the publisher’s terms and conditions. |
| 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/10090952 |
Archive Staff Only
 |
View Item |
