A NEW TYPE OF PUSHDOWN AUTOMATA ON INFINITE TREES
Wuxu Peng, S. Purushothaman Iyer · International Journal of Foundations of Computer Science · 1995
In this paper we consider pushdown automata on infinite trees with empty stack as the accepting condition (ω-EPDTA). We provide the following regarding ω-EPDTA: (a) its relationship to other Pushdown automata on infinite trees, (b) a Kleene-Closure theorem and (c) a single exponential time algorithm for checking emptiness. We demonstrate the usefulness of ω-EPDTA through two example applications: defining the temporal uniform inevitability property and specifying a context-free process with unbounded state space, both of which cannot be defined and/or specified by the classical finite state automata on infinite trees. We also discuss the relevance of the results presented here to model-checking.