The Library
Collapsible pushdown automata and recursion schemes
Tools
Hague, M., Murawski, Andrzej S., Ong, C. -H. L. and Serre, O. (2008) Collapsible pushdown automata and recursion schemes. In: 23rd Annual IEEE Symposium on Logic in Computer Science (LICS '08), Pittsburgh, PA, 24-27 June 2008. Published in: Logic in Computer Science, 2008. LICS '08. 23rd Annual IEEE Symposium on pp. 452-461. ISBN 9780769531830. doi:10.1109/LICS.2008.34 ISSN 1043-6871.
Research output not available from this repository.
Request-a-Copy directly from author or use local Library Get it For Me service.
Official URL: http://dx.doi.org/10.1109/LICS.2008.34
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 Gt= 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 resul- - t 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.
Item Type: | Conference Item (Paper) | ||||
---|---|---|---|---|---|
Divisions: | Faculty of Science, Engineering and Medicine > Science > Computer Science | ||||
Journal or Publication Title: | Logic in Computer Science, 2008. LICS '08. 23rd Annual IEEE Symposium on | ||||
Publisher: | IEEE | ||||
ISBN: | 9780769531830 | ||||
ISSN: | 1043-6871 | ||||
Book Title: | 2008 23rd Annual IEEE Symposium on Logic in Computer Science | ||||
Official Date: | June 2008 | ||||
Dates: |
|
||||
Page Range: | pp. 452-461 | ||||
DOI: | 10.1109/LICS.2008.34 | ||||
Status: | Peer Reviewed | ||||
Publication Status: | Published | ||||
Access rights to Published version: | Restricted or Subscription Access | ||||
Conference Paper Type: | Paper | ||||
Title of Event: | 23rd Annual IEEE Symposium on Logic in Computer Science (LICS '08) | ||||
Type of Event: | Conference | ||||
Location of Event: | Pittsburgh, PA | ||||
Date(s) of Event: | 24-27 June 2008 |
Request changes or add full text files to a record
Repository staff actions (login required)
View Item |