2026-07-22T21:25:01Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:4382 2024-03-06T10:34:59Z ddc:004 open_access

Saturation of Concurrent Collapsible Pushdown Systems Hague, Matthew Concurrency Automata Higher-Order Verification Model-Checking 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Matthew Hague 2013 Is Part Of LIPIcs, Volume 24, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2013.313 urn:nbn:de:0030-drops-43829 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2013.313 eng https://creativecommons.org/licenses/by/3.0/legalcode