On modal mu-calculus and Büchi tree automata

Roope Kaivola

Abstract: Modal mu-calculus and automata on infinite trees are complementary ways of describing infinite tree languages. We examine a fragment of modal mu-calculus, the alternation-depth class Pi2 and its relation to tree languages recognised by Büchi-automata. It is shown that there is an exact correspondence between languages characterised by formulae in Pi2 and languages recognised by Büchi-automata which do not distinguish subtrees. This involves an inductive mapping from formulae to automata, in which the core point is a construction of powerset automata recognising maximal and minimal fixpoints of a Büchi-automaton. The construction avoids altogether the usual complex process of complementing automata when mapping formulae to automata, leading to a more transparent translation. As a corollary of the result we see that the alternation-depth hierarchy of modal mu-calculus does not collapse at Pi2.

LFCS report ECS-LFCS-94-293, July 1994.

Previous | Index | Next