交替奇偶自动机代数理论的循环系统

$\omega$-正则语言是正则语言在无限单词情境下的自然延伸。它们由多种自动机模型识别，其中最重要的是交替奇偶自动机 (APA)，它是 Büchi 自动机的泛化，通过对转移（包括 universal 和 existential 分支）和接受条件（通过奇偶条件）进行对称化。本文发展出一种操纵 APA 的循环证明系统，APA 采用 Right Linear Lattice 表达式的代数表示。该语法对先前引入的 Right Linear Algebras（用于非确定性有限自动机 NFA 的表示）进行二元化。这一二元化在我们设计的证明系统中引发对称性，lattice 操作在 Sequent 的每一侧以二元方式行为。我们的主要结果是该系统对 $\omega$-语言包含的 soundness 和 completeness 完全成立，广泛利用 $\omega$-正则语言理论中的博弈论技术。