An algebraic theory of {\omega}-regular languages, via {\mu}{\nu}-expressions

TL;DR

This paper develops an algebraic framework for {}regular languages using {}{}}-expressions, extending previous work on finite automata to infinite words and automata with infinite behaviors.

Contribution

It introduces a dualised syntax and axiomatisation for alternating parity automata based on right-linear lattice expressions, connecting to fixed point logics and the linear-time -calculus.

Findings

Provides a sound and complete axiomatisation for {}regular languages.

Extends algebraic theory from finite automata to infinite words.

Connects automata theory with fixed point logics and -calculus.

Abstract

Alternating parity automata (APAs) provide a robust formalism for modelling infinite behaviours and play a central role in formal verification. Despite their widespread use, the algebraic theory underlying APAs has remained largely unexplored. In recent work, a notation for non-deterministic finite automata (NFAs) was introduced, along with a sound and complete axiomatisation of their equational theory via right-linear algebras. In this paper, we extend that line of work, in particular to the setting of infinite words. We present a dualised syntax, yielding a notation for APAs based on right-linear lattice expressions, and provide a natural axiomatisation of their equational theory with respect to the standard language model of {\omega}-regular languages. The design of this axiomatisation is guided by the theory of fixed point logics; in fact, the completeness factors cleanly through the completeness of the linear-time {\mu}-calculus.