Proceedings 32nd Annual Symposium of Foundations of Computer Science (1991)
San Juan, Puerto Rico
Oct. 1, 1991 to Oct. 4, 1991
E.A. Emerson , Texas Univ., Austin, TX, USA
It is shown that the propositional mu-calculus is equivalent in expressive power to finite automata on infinite trees. Since complementation is trivial in the mu-calculus, the equivalence provides a radically simplified, alternative proof of M.O. Rabin's (1989) complementation lemma for tree automata, which is the heart of one of the deepest decidability results. It is also shown 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 online algorithms.
online algorithms, mu-calculus, determinacy, finite automata, infinite trees, complementation, equivalence, decidability, infinite games
E. Emerson and C. Jutla, "Tree automata, mu-calculus and determinacy,"  Proceedings 32nd Annual Symposium of Foundations of Computer Science(FOCS), San Juan, Puerto Rico, 1991, pp. 368-377.