Anzeige
Erschienen in:
2005 | OriginalPaper | Buchkapitel
Unsafe Grammars and Panic Automata
verfasst von : Teodor Knapik, Damian Niwiński, Paweł Urzyczyn, Igor Walukiewicz
Erschienen in: Automata, Languages and Programming
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
We show that the problem of checking if an infinite tree generated by a higher-order grammar of level 2 (hyperalgebraic) satisfies a given
μ
-calculus formula (or, equivalently, if it is accepted by an alternating parity automaton) is decidable, actually 2-
Exptime
-complete. Consequently, the monadic second-order theory of any hyperalgebraic tree is decidable, so that the safety restriction can be removed from our previous decidability result. The last result has been independently obtained by Aehlig, de Miranda and Ong. Our proof goes
via
a characterization of possibly unsafe second-order grammars by a new variant of higher-order pushdown automata, which we call
panic automata
. In addition to the standard
pop
1
and
pop
2
operations, these automata have an option of a destructive move called
panic
. The model-checking problem is then reduced to the problem of deciding the winner in a parity game over a suitable 2nd order pushdown system.