Symbolic Backwards-Reachability Analysis for Higher-Order Pushdown Systems

Higher-order pushdown systems (PDSs) generalise pushdown systems through theuse of higher-order stacks, that is, a nested "stack of stacks" structure.These systems may be used to model higher-order programs and are closelyrelated to the Caucal hierarchy of infinite graphs and safe higher-orderrecursion schemes. We consider the backwards-reachability problem over higher-order AlternatingPDSs (APDSs), a generalisation of higher-order PDSs. This builds on and extendsprevious work on pushdown systems and context-free higher-order processes in anon-trivial manner. In particular, we show that the set of configurations fromwhich a regular set of higher-order APDS configurations is reachable is regularand computable in n-EXPTIME. In fact, the problem is n-EXPTIME-complete. We show that this work has several applications in the verification ofhigher-order PDSs, such as linear-time model-checking, alternation-freemu-calculus model-checking and the computation of winning regions ofreachability games