Cyclic System for an Algebraic Theory of Alternating Parity Automata
Anupam Das, Abhishek De · Lecture notes in computer science · 2025
Abstract $$\omega $$ ω -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. Our main result is the soundness and completeness of our system for $$\omega $$ ω -language inclusion, heavily exploiting game-theoretic techniques from the theory of $$\omega $$ ω -regular languages.