Seminarium Teoria Automatów

Prelegent: Damian Niwinski (joint work with T. Knapik, P. Urzyczyn, and I. Walukiewicz)

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.