2013/10/09 by Matthew Hague, Hague, Matthew · 1 citation
Computer Science · #F.1.1 #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Formal Methods in Verification #Logic, programming, and type systems #Parallel Computing and Optimization Techniques
paper · pdf · doi:10.48550/arxiv.1310.2631
openalex publication_date 2013/10/09 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Multi-stack pushdown systems are a well-studied model of concurrent computation using threads with first-order procedure calls. While, in general, reachability is undecidable, there are numerous restrictions on stack behaviour that lead to decidability. To model higher-order procedures calls, a generalisation of pushdown stacks called collapsible pushdown stacks are required. Reachability problems for multi-stack collapsible pushdown systems have been little studied. Here, we study ordered, phase-bounded and scope-bounded multi-stack collapsible pushdown systems using saturation techniques, showing decidability of control state reachability and giving a regular representation of all configurations that can reach a given control state.