Model checking of panic automata

Prelegent(ci)

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

Afiliacja

Uniwersytet Warszawski

Termin

19 października 2005 14:15

Pokój

p. 5870

Seminarium

Seminarium „Teoria automatów”

---

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.

---