Kappé, Tobias;
(2020)
Concurrent Kleene Algebra: Completeness and Decidability.
Doctoral thesis (Ph.D), UCL (University College London).
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 |
Archive Staff Only
 |
View Item |
