Collapsible Pushdown Automata and Recursion Schemes

Overview & Synopsis

Collapsible pushdown automata (CPDA) are a new kind of higher-order pushdown automata in which every symbol in the stack has a link to a stack situated somewhere below it. In addition to the higher-order stack operations pushi and pop_i , CPDA have an important operation called c ollapse, whose effect is to “collapse” a stack s to the prefix as indicated by the link from the t op 1 -symbol of s. Our first result is that CPDA are equi-expressive with recursion schemes as generators of node-labelled ranked trees. In one direction, we give a simple algorithm that transforms an order-n CPDA to an order-n recursion scheme that generates the same tree, uniformly for all n ≥ 0. In the other direction, using ideas from game semantics, we give an effective transformation of order-n recursion schemes (not assumed to be homogeneously typed, and hence not necessarily safe) to order-n CPDA that compute traversals over a certain finite graph determined by the scheme, and hence paths in the tree generated by the scheme. Our equi-expressivity result is the first such automata-theoretic characterization of (general) recursion schemes. An important consequence of the equi-expressivity result is that it allows us to translate decision problems on trees generated by recursion schemes to equivalent problems on CPDA and vice versa. For example, since the Modal Mu-Calculus Model-Checking Problem for trees generated by order-n recursion schemes is n-EXPTIME complete, we show that it follows that the same decidability result holds for the problem of solving a parity game played on an order-n collapsible pushdown graph i.e. the configuration graph of a corresponding (order-n) collapsible pushdown system; the latter subsumes several well-known results about the solvability of games over (higher-order) pushdown graphs by (respectively) Walukiewicz, Cachat, and Knapik et al. Moreover our approach yields techniques that are radically different from standard methods for solving model-checking problems on infinite graphs generated by finite machines. This transfer of techniques goes both ways. Another innovation of our work is a self-contained proof of the solvability of parity games on collapsible pushdown graphs by generalizing standard techniques in the field. By appealing to our equi-expressivity result, we obtain a new proof of the decidability (and optimal complexity) of the Modal Mu-Calculus Model-Checking Problem of trees generated by recursion schemes. In contrast to higher-order pushdown graphs, we show that Monadic Second-Order (MSO) theories of collapsible pushdown graphs are undecidable. Hence collapsible pushdown graphs are, to our knowledge, the first example of a natural class of finitely-presentable graphs that have undecidable MSO theories while enjoying decidable modal mu-calculus theories.