2013 IEEE 54th Annual Symposium on Foundations of Computer Science (1991)

San Juan, Puerto Rico

Oct. 1, 1991 to Oct. 4, 1991

ISBN: 0-8186-2445-0

pp: 368-377

E.A. Emerson , Texas Univ., Austin, TX, USA

ABSTRACT

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.

INDEX TERMS

online algorithms, mu-calculus, determinacy, finite automata, infinite trees, complementation, equivalence, decidability, infinite games

CITATION

E.A. Emerson,
C.S. Jutla,
"Tree automata, mu-calculus and determinacy",

*2013 IEEE 54th Annual Symposium on Foundations of Computer Science*, vol. 00, no. , pp. 368-377, 1991, doi:10.1109/SFCS.1991.185392