You are not logged in | Log in

Model checking of panic automata

Damian Niwinski (joint work with T. Knapik, P. Urzyczyn, and I. Walukiewicz)
Uniwersytet Warszawski
Oct. 19, 2005, 2:15 p.m.
room 5870
Seminar Automata Theory

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.