Oxford University Computing Laboratory
4pm Tuesday, 11 August, 2009
Room IF 4.31/4.33, Informatics Forum
Higher-order pushdown systems (PDSs) generalise pushdown systems through the use of higher-order stacks, that is, a nested ``stack of stacks'' structure. These systems may be used to model higher-order programs and are closely related to the Caucal hierarchy of infinite graphs and safe higher-order recursion schemes.
We consider the backwards-reachability problem over higher-order Alternating PDSs (APDSs), a generalisation of higher-order PDSs. This builds on and extends previous work on pushdown systems and context-free higher-order processes in a non-trivial manner. In particular, we show that the set of configurations from which a regular set of higher-order APDS configurations is reachable is regular and computable in n-EXPTIME. In fact, the problem is n-EXPTIME-complete.
This work was originally presented in FoSSaCS 2007.