arXiv · 2505.10303
An algebraic theory of {\omega}-regular languages, via {\mu}{\nu}-expressions
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.
Explore related subjects
Keep this discovery
Explore connections, maps & timelines
Anupam Das, Abhishek De. 2025-05-15. An algebraic theory of {\omega}-regular languages, via {\mu}{\nu}-expressions. https://arxiv.org/abs/2505.10303
Cite the original work for its findings. Save a collection to share your selection of sources.