Tree Automata, Mu-Calculus and Determinacy (Extended Abstract)

Abstract

We show that the propositional Mu-Calculus is equivalent in expressive power to finite automata on infinite trees. Since complementation is trivial in the Mu-Calculus, our equivalence provides a radically simplified, alternative proof of Rabin's complementation lemma for tree automata, which is the heart of one of the deepest decidability results. We also show how Mu-Calculus can be used to establish determinacy of infinite games used in earlier proofs of complementation lemma, and certain games used in the theory of on-line algorithms.