Model checking of panic automata

Speaker(s)

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

Affiliation

Uniwersytet Warszawski

Date

Oct. 19, 2005, 2:15 p.m.

Room

room 5870

Seminar

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.

---