UCL Discovery
UCL home » Library Services » Electronic resources » UCL Discovery

Completeness and Incompleteness of Synchronous Kleene Algebra

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.

[img] Text
1905.08554v2.pdf - Accepted version
Access restricted to UCL open access staff until 21 October 2020.

Download (333kB)

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)
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 > 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
Downloads since deposit
1Download
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item