The<i>μ</i>-calculus alternation-depth hierarchy is strict on binary trees

Abstract

In this paper we give a simple proof that the alternation-depth hierarchy of the μ-calculus for binary trees is strict. The witnesses for this strictness are the automata that determine whether there is a winning strategy for the parity game played on a tree.