A Kleene Theorem and Decision Problems for Probability and Angelic Nondeterminism
In order to reason about the capabilities and limitations of a specific com-puting model or programming language, a formal system that can model the behavior of a computational device is required. Once such a correspondence is established, we have access to tools to reason about the performed computation from both denotational and operational viewpoints: for example, the equational theory may be axiomatized, and we can classify the computations which can be carried out by the corresponding model of computation. Even in otherwise lim- ited models of computation, the combination of probability and nondetermin- ism in state-based systems is a particularly challenging problem, chiefly due to the provable lack of a distributive law between the powerset and Giry monads. This thesis focuses on the theory of a version of probabilistic Kleene al- gebra with angelic nondeterminism and the corresponding class of automata. This approach implements semantics via distributions over multisets in order to overcome the theoretical barriers arising from the absence of a distributive law. Chapter 3 introduces the model and establishes a correspondence between the expression and automaton models by proving a Kleene theorem. Such a theorem demonstrates that the two models of computation are equivalent and is the first instance of such a theorem for models including both probability and nondeterminism. This chapter also explore the coalgebraic theory, as well as demonstrating both operational and denotational semantics, in addition to some equational reasoning principles. In Chapter 4 of this thesis, we further extend this theory by investigating the significant decision problems related to this model of computation. In particular, we provide a decision procedure for language equivalence and an algorithm for determining whether a relation is a bisimulation. These algorithms both build off of a novel correspondence be- tween distributions over multisets and formal power series, which allows us to leverage results from polynomial algebra.