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

Concurrent Kleene Algebra: Completeness and Decidability

Kappé, Tobias; (2020) Concurrent Kleene Algebra: Completeness and Decidability. Doctoral thesis (Ph.D), UCL (University College London). Green open access

[thumbnail of main.pdf]
Preview
Text
main.pdf

Download (1MB) | Preview

Abstract

Concurrent Kleene Algebra (CKA) offers a set of axioms to reason about equivalence of concurrent programs, such that equivalent programs must have the same interpretation in any program semantics that respects the axioms of CKA. It builds on the well-known formalism of Kleene Algebra, which offers the same benefits for sequential programs. CKA is complete, that is, any valid equivalence can be proved from the axioms. Moreover, equivalence of programs according to CKA can be verified mechanically, i.e., equivalence is decidable. Crucial to the latter is the fact that programs can be represented as abstract machines, which admit equivalence checking. In this thesis, we investigate techniques to augment the reasoning power of CKA with additional truths particular to the program semantics at hand. Building on similar results about Kleene Algebra, we will show that for a large class of extensions, decidability and completeness can be recovered. In particular, our techniques will allow us to incorporate reasoning about interleaving, i.e., the partially sequential execution of concurrent programs, as well as control flow, such as the conditional branching and looping structures found in most programming languages. In the second half of this thesis, we will develop our own abstract machine model to represent programs modelled by Concurrent Kleene Algebra, and show that any such program can be modelled by a machine, and vice versa. We will then argue that equivalence of these automata is mechanisable, and that the correspondence between expressions and automata can be extended further to incorporate a more general form of concurrent program composition.

Type: Thesis (Doctoral)
Qualification: Ph.D
Title: Concurrent Kleene Algebra: Completeness and Decidability
Event: UCL (University College London)
Open access status: An open access version is available from UCL Discovery
Language: English
Additional information: Work on this thesis was supported by the ERC Starting Grant ProFoundNet (679127). // Copyright © The Author 2020. Original content in this thesis is licensed under the terms of the Creative Commons Attribution 4.0 International (CC BY 4.0) Licence (https://creativecommons.org/licenses/by/4.0/). Any third-party copyright material present remains the property of its respective owner(s) and is licensed under its existing terms. Access may initially be restricted at the author’s request.
Keywords: concurrency, Kleene algebra, pomsets, pomset automata, completeness, decidability, program equivalence
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/10109361
Downloads since deposit
417Downloads
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item