Extensions of (Concurrent) Kleene Algebra

Kleene algebra is the algebra of regular expressions, and a fundamental structure in computer science. It appears in various contexts, such as program semantics, relational algebra, and automata theory. In this thesis we study Kleene algebras for program logics and semantics, although some of the results can be used in other domains.

In the first chapter we focus on Kleene algebra with hypotheses, a framework used to uniformly extend Kleene algebra with additional constraints. We provide an overview of existing classes of hypotheses with completeness and decidability results, and we develop tools to establish completeness and decidability for new classes of hypotheses, in a modular way.
Within this framework, we present alternative completeness proofs for known extensions of Kleene algebra: Kleene algebra with tests and Kleene algebra with observations.

The next chapter presents concurrent Kleene algebra, and concurrent Kleene algebra with hypotheses. We demonstrate the use of the framework by presenting concurrent Kleene algebra with observations, which is an algebra that combines concurrency and tests in the form of observations.

After that we introduce a specification language based on Kleene algebra: partially observable concurrent Kleene algebra (POCKA). POCKA can be used to reason about concurrent programs with variables and control structures that manipulate a shared global memory. We prove that POCKA is a sound and complete axiomatisation of a model of partial observations, and show that the semantics pass an important check for sequential consistency.

Lastly we present concurrent NetKAT (CNetKAT), a language with operators for specifying and reasoning about concurrency in scenarios where multiple packets in a network interact through state. We provide a sound and complete axiomatisation of the presented model. Besides using CNetKAT to analyse network behaviours, CNetKAT can be understood more generally as an algebraic framework for reasoning about programs with both local and global state.