Higher-order pushdown systems (PDSs) generalise pushdown systems through the use of higher-order stacks, that is, a nested "stack of stacks" structure. We further generalise higher-order PDSs to higherorder Alternating PDSs (APDSs) and consider the backwards reachability problem over these systems. We prove that given an order-n APDS, the set of configurations from which a given regular set of configurations is reachable is itself regular and computable in n-EXPTIME. We show that the result has several useful applications in the verification of higher-order PDSs such as LTL model checking, alternation-free μ-calculus model checking, and the computation of winning regions of reachability games. © Springer-Verlag Berlin Heidelberg 2007.
CITATION STYLE
Hague, M., & Ong, C. H. L. (2007). Symbolic backwards-reachability analysis for higher-order pushdown systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4423 LNCS, pp. 213–227). Springer Verlag. https://doi.org/10.1007/978-3-540-71389-0_16
Mendeley helps you to discover research relevant for your work.