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