Lics

IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Twenty-Third Annual IEEE Symposium on

Logic in Computer Science (LICS 2008)

Paper: Collapsible Pushdown Automata and Recursion Schemes (at LICS 2008)

Authors: Matthew Hague Andrzej S. Murawski C.-H. Luke Ong Olivier Serre

Abstract

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 push and pop operations, CPDA have an important operation called collapse, whose effect is to "collapse" a stack s to the prefix as indicated by the link from the topmost symbol of s. Our first result is that CPDA are equi-expressive with recursion schemes as generators of (possibly infinite) 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 an abstract syntax graph of the scheme, and hence paths in the tree generated by the scheme. Our equi-expressivity result is the first automata-theoretic characterization of higher-order recursion schemes. Thus CPDA are also a characterization of the simply-typed lambda calculus with recursion (generated from uninterpreted 1st-order symbols) and of (pure) innocent strategies. An important consequence of the equi-expressivity result is that it allows us to reduce decision problems on trees generated by recursion schemes to equivalent problems on CPDA and vice versa. Thus we show, as a consequence of a recent result by Ong (modal mu-calculus model-checking of trees generated by recursion schemes is n-EXPTIME complete), that the problem of solving parity games over the configuration graphs of order-n CPDA is n-EXPTIME complete, subsuming several well-known results about the solvability of games over higher-order pushdown graphs by (respectively) Walukiewicz, Cachat, and Knapik et al. Another contribution of our work is a self-contained proof of the same solvability result by generalizing standard techniques in the field. By appealing to our equi-expressivity result, we obtain a new proof of Ong's result. In contrast to higher-order pushdown graphs, we show that the monadic second-order theories of the configuration graphs of CPDA are undecidable. It follows that -- as generators of graphs -- CPDA are strictly more expressive than higher-order pushdown automata.

BibTeX

  @InProceedings{HagueMurawskiOngSer-CollapsiblePushdown,
    author = 	 {Matthew Hague and Andrzej S. Murawski and C.-H. Luke Ong and Olivier Serre},
    title = 	 {Collapsible Pushdown Automata and Recursion Schemes},
    booktitle =  {Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science (LICS 2008)},
    year =	 {2008},
    month =	 {June}, 
    pages =      {452--461},
    location =   {Pittsburgh, PA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }
   

Last modified: 2018-06-2121:59
Andrzej Murawski