|
|
VOLUME 4, ISSUE 4, PAPER 14
|
Symbolic Backwards-Reachability Analysis for Higher-Order Pushdown Systems
|
©Matthew Hague, Oxford University
©Luke Ong, Oxford University
|
Abstract
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.
|
Publication date: December 5, 2008
Full Text: PDF | PostScript
DOI: 10.2168/LMCS-4(4:14)2008
Hit Counts: 3330 |
 Creative Commons | |
