Cyclic system for an algebraic theory of alternating parity automata
Anupam Das, Abhishek De
TL;DR
The paper develops a cyclic, two-sided sequent calculus CRLL$_\mathcal{L}$ for Right-Linear Lattice (RLL) expressions that natively encode alternating parity automata (APAs) and their ω-regular languages. By establishing a tight correspondence between closed RLL expressions and APAs through the Fischer-Ladner closure and evaluation games, it proves soundness and completeness of CRLL$_\mathcal{L}$ for ω-language inclusion, enabling direct algebraic reasoning about APA properties such as emptiness, universality, and equivalence. The approach relies on a symmetric lattice-theoretic syntax with fixed points μ and ν to capture parity conditions, and on evaluation games whose adequacy reduces language questions to finite-memory, positionally determined games in the spirit of Büchi-Landweber. Overall, the work provides a rigorous, algebraic framework for reasoning about APAs and ω-regular languages, with potential implications for automated verification and formal reasoning about infinite-word systems.
Abstract
$ω$-regular languages are a natural extension of the regular languages to the setting of infinite words. Likewise, they are recognised by a host of automata models, one of the most important being Alternating Parity Automata (APAs), a generalisation of Büchi automata that symmetrises both the transitions (with universal as well as existential branching) and the acceptance condition (by a parity condition). In this work we develop a cyclic proof system manipulating APAs, represented by an algebraic notation of Right Linear Lattice expressions. This syntax dualises that of previously introduced Right Linear Algebras, which comprised a notation for non-deterministic finite automata (NFAs). This dualisation induces a symmetry in the proof systems we design, with lattice operations behaving dually on each side of the sequent. Our main result is the soundness and completeness of our system for $ω$-language inclusion, heavily exploiting game theoretic techniques from the theory of $ω$-regular languages.