Schmid, Todd Junior Wayne; (2024) Coalgebraic Completeness Theorems for Effectful Process Algebras. Doctoral thesis (Ph.D), UCL (University College London).

Preview

Text Schmid_Thesis.pdf - Other Download (1MB) | Preview

Abstract

In 1984, Robin Milner proposed a nonstandard interpretation of regular expressions: as behaviours of nondeterministic processes rather than regular languages. This shift in interpretation drastically reduced the set of sound equivalences between regular expressions, making Arto Salomaa’s complete axiomatization of the algebra of regular languages unsound under the new interpretation. In the same paper, Milner adapted Salomaa’s axioms to give a sound axiomatization of bisimilarity and asked whether his axiomatization was complete. Milner’s completeness problem was open for nearly 38 years before Clemens Grabmayer published a positive solution in 2022. Milner’s problem motivated three decades of research into process algebra, the algebraic study of concurrent processes. Working concurrently with the process algebra community between the 1960s and 1990s, Volodymyr N. Redko, John H. Conway, Dexter Kozen, and their collaborators developed Kleene algebra (KA), an abstraction from the algebra of regular languages and generalization of Salomaa’s axiomatization. Their work led to the invention of Kleene algebra with Tests (KAT), which extends Kleene algebra with Boolean control flow for reasoning about imperative programs. A notable fragment of KAT, guarded Kleene algebra with tests (GKAT), consists of only the programs that can be written using the if-then-else and while-do imperative programming constructs. GKAT is a simple and efficient fragment of KAT for which a sound Salomaa-style axiomatization exists. However, the question of completeness for this axiomatization is still open. In this thesis, I connect the completeness problems of Milner and GKAT using techniques from universal algebra and coalgebra. In the first part of the thesis, I identify the source of difficulty in both these problems: In GKAT and Milner’s regular expressions modulo bisimilarity, some finite systems of formal equations are unsolvable. I show that every coalgebraic completeness theorem comes from a certain structured class of solvable systems of equations, and vice versa. In the second part of the thesis, I provide a partial completeness result for GKAT. Specifically, I show that the axioms of GKAT are complete for GKAT expressions of a specific form, called skip-free. The proof is a reduction to the completeness theorem for regular expressions modulo bisimilarity. In the last part of the thesis, I generalize the completeness problems of Milner and GKAT to a wide class of process algebras with algebraic effects, which I call effectful process algebras. Effectful process algebras capture a number of other process calculi than GKAT and regular expressions modulo bisimilarity, including a few process calculi that mix probability and nondeterminism. I develop the theory of effectful process algebras in general. I give a uniform construction of both the operational and denotational semantics of effectful process algebras and show that the two semantics coincide, as well as a uniform sound and complete axiomatization of bisimilarity in effectful process algebras. The axiomati zation includes a generalization of an axiom scheme used by Smolka et al. (2019) to obtain a completeness theorem for GKAT. My general completeness theorem for effectful process algebras instantiates to the bisimulation variant of this concrete completeness theorem for GKAT, as well as to completeness theorems for the other examples mentioned.

Download activity - last month

Export as XMLCSVJSON

Download activity - last 12 months

Export as CSVJSONXML

Downloads by country - last 12 months

Export as JSONCSVXML

Archive Staff Only

View Item