An algebraic theory of ω-regular languages, via μν-expressions
Anupam Das, Abhishek De
TL;DR
The paper develops an algebraic framework for ω-regular languages via right-linear lattice expressions (RLL), presenting a sound and complete axiomatisation ($\mathsf{RLL}_\mathcal{L}$) w.r.t. the standard model $\mathcal{L}$ of ω-words. It dualises right-linear algebras to capture alternating parity automata and connects the equational theory to fixed-point logic by reducing completeness to linear-time $\mu$-calculus ($\mu\mathsf{LTL}$). A key contribution is showing that RLL expressions span a Boolean subalgebra of $\mathcal{L}$ through complementation, while addressing incompleteness via a duality axiom ($\mu$-$\nu$ dual). The results provide a robust algebraic foundation for reasoning about ω-regular languages and APAs, linking lattice-based syntax to fixed-point logics used in verification.
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 ω-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 μ-calculus.