Modal mu-calculus and automata on infinite trees are complementary ways of describing infinite tree languages. In this paper we describe direct fixpoint constructions for Rabin-automata, allowing us to translate modal mu-calculus inductively to Rabin-automata. As Rabin-automata can also be mapped to moddal mu-calculus, the fixpoint constructions provide a new proof of the expressive equivalence of the two formalisms, and lead to a simple proof of Babin's complementation lemma, the core of the powerful decidability result for SnS.
展开▼
