Symbolic backwards-reachability analysis for higher-order pushdown systems

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 push-down 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 con-figurations is reachable is regular and computable in n-EXPTIME. In fact, the problem is n-EXPTIME-complete. We show that this work has several applications in the verification of higher-order PDSs, such as linear-time model checking, alternation-free µ-calculus model-checking, the compu-tation of winning regions of reachability games and determining whether the word language accepted by a higher-order pushdown automata is non-empty