Matthew Hague ; C. -H. Luke Ong - Symbolic Backwards-Reachability Analysis for Higher-Order Pushdown Systems

lmcs:831 - Logical Methods in Computer Science, December 5, 2008, Volume 4, Issue 4 - https://doi.org/10.2168/LMCS-4(4:14)2008
Symbolic Backwards-Reachability Analysis for Higher-Order Pushdown Systems

Authors: Matthew Hague ; C. -H. Luke Ong

    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.


    Volume: Volume 4, Issue 4
    Published on: December 5, 2008
    Accepted on: June 25, 2015
    Submitted on: September 26, 2007
    Keywords: Computer Science - Computational Complexity,Computer Science - Computer Science and Game Theory,F.1.1

    Linked data

    Source : ScholeXplorer IsReferencedBy DOI 10.1007/978-3-642-31585-5_18
    • 10.1007/978-3-642-31585-5_18
    • 10.1007/978-3-642-31585-5_18
    • 10.1007/978-3-642-31585-5_18
    A saturation method for collapsible pushdown systems
    Broadbent, Christopher ; Carayol, Arnaud ; Hague, Matthew ; Serre, Olivier ;

    9 Documents citing this article

    Share

    Consultation statistics

    This page has been seen 326 times.
    This article's PDF has been downloaded 319 times.