Proof Systems for the Modal $\mu$-Calculus Obtained by Determinizing Automata

TL;DR

This paper introduces a new determinization method for automata used in the modal μ-calculus, leading to a novel proof system with proven soundness and completeness.

Contribution

It presents a binary tree determinization construction for nondeterministic parity automata, enabling the development of a new annotated cyclic proof system for the μ-calculus.

Findings

The determinization construction is sound and complete.

The proof system $ extsf{BT}$ is sound and complete.

Automata determinization directly yields proof systems for the μ-calculus.

Abstract

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.