Automata operating on infinite objects feature prominently in the theory of the modal $\mu$-calculus. One such application concerns the tableau games introduced by Niwi\'{n}ski & Walukiewicz, of which the winning condition for infinite plays can be naturally checked by a nondeterministic parity stream automaton. Inspired by work of Jungteerapanich and Stirling we show how determinization constructions of this automaton may be used to directly obtain proof systems for the $\mu$-calculus. More concretely, we introduce a binary tree construction for determinizing nondeterministic parity stream automata. Using this construction we define the annotated cyclic proof system $\mathsf{BT}$, where formulas are annotated by tuples of binary strings. Soundness and Completeness of this system follow almost immediately from the correctness of the determinization method.

翻译：在无限对象上运行的自动机在模态μ-演算理论中占据显著地位。其中一个应用涉及由Niwiński & Walukiewicz引入的表列博弈，其无限对局的获胜条件可通过非确定性奇偶流自动机自然验证。受Jungteerapanich与Stirling工作的启发，我们展示了如何利用该自动机的确定性构造直接获得μ-演算的证明系统。具体而言，我们引入了一种用于确定性非确定性奇偶流自动机的二叉树构造。借助这一构造，我们定义了带注释的循环证明系统$\mathsf{BT}$，其中公式由二进制字符串元组注释。该系统的可靠性与完备性几乎直接源自确定性方法的正确性。