Automata Closure Constructions for Kleene Algebra with Hypotheses
Liam Chung

Abstract:
In this thesis, we will develop automaton constructions as a tool for studying the equational theories of Kleene algebra with arbitrary hypotheses. Kleene algebra with hypotheses is a framework for assigning language-based semantics to Kleene algebra-based systems where extra features are formulated as axioms in the equational logic.
These semantics are defined by a closure operation on languages called “hypothesis closure”. Completeness of the “hypothesis-closed” semantics can be shown via reductions to known systems, such as Kleene algebra with tests. However, doing so requires that the hypothesis closure can be effectively computed. This thesis proposes a general approach to calculating the hypothesis closure in terms of standard Kleene algebra, for arbitrary hypotheses.
We define two constructions on automata and prove they are correct, when they terminate. We examine cases where they terminate, and present a strategy for improving how often they do. In cases where the constructions terminate, proving completeness becomes much simpler via reductions, and we even obtain a decision procedure for equality, using automaton equivalence. We will therefore work extensively with automata-theoretic machinery to define the proposed constructions, and prove their correctness.