Model checking of panic automata

Panic automata, invented by Pawel Urzyczyn, extend the concept of 2nd order pushdown automata (with stacks of stacks), by a destructive move called panic. They are in a sense equivalent to 2nd order tree grammars. We show the decidability, in fact, 2-EXPTIME-completeness, of the Mu-calculus model-checking problem for the configuration graphs of such automata. This implies decidability of the monadic second-order theories of hyperalgebraic trees, the result independently obtained by Aehlig, de Miranda and Ong.