## 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 Pi_{2} 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
Pi_{2} 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 Pi_{2}.

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

Previous |

Index |

Next