Computer Science – Computational Complexity
Scientific paper
2008-11-07
LMCS 4 (4:14) 2008
Computer Science
Computational Complexity
Scientific paper
10.2168/LMCS-4(4:14)2008
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. We show that this work has several applications in the verification of higher-order PDSs, such as linear-time model-checking, alternation-free mu-calculus model-checking and the computation of winning regions of reachability games.
Hague Matthew
Luke Ong C.-H.
No associations
LandOfFree
Symbolic Backwards-Reachability Analysis for Higher-Order Pushdown Systems does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Symbolic Backwards-Reachability Analysis for Higher-Order Pushdown Systems, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Symbolic Backwards-Reachability Analysis for Higher-Order Pushdown Systems will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-228668