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}$，其中公式由二元字符串元组注释。该系统的可靠性与完备性几乎可直接由确定化方法的正确性推导得出。