Algebras for Automata: Reasoning with Regularity

Abstract

In the second half of the 20^th century various theories of regular expressions were proposed, eventually leading to the notion of a Kleene Algebra ($\mathrm{𝖪𝖠}$). Kozen and Krob independently proved the completeness of $\mathrm{𝖪𝖠}$ for the model of regular languages, a now celebrated result that has been refined and generalised over the years. In recent years proof theoretic approaches to regular languages have been studied, providing alternative routes to metalogical results like completeness and decidability.

In this talk I will present a new approach from a different starting point: finite state automata. A notation for non-deterministic finite automata is readily obtained via expressions with least fixed points, leading to a theory of right-linear algebras ($\mathrm{𝖱𝖫𝖠}$). $\mathrm{𝖱𝖫𝖠}$ is strictly more general than $\mathrm{𝖪𝖠}$, e.g. admitting $\omega$-regular languages as a model too, and enjoys a simpler proof theory than $\mathrm{𝖪𝖠}$. This allows us to recover (more general) metalogical results in a robust way, combining techniques from automata, games, and cyclic proofs. Finally I will discuss extensions of $\mathrm{𝖱𝖫𝖠}$ by greatest fixed points, comprising a notation for parity automata, to reason about $\omega$-regular languages too.

This talk is based on joint works with Abhishek De [2, 1].