Saturation of Concurrent Collapsible Pushdown Systems
From MaRDI portal
Abstract: 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.
Recommendations
- scientific article; zbMATH DE number 7361952
- A Saturation Method for Collapsible Pushdown Systems
- Parity to safety in polynomial time for pushdown and collapsible pushdown systems
- Reachability of scope-bounded multistack pushdown systems
- Constraint-based concurrency and beyond
- Variants of collapsible pushdown systems
- Implementations of the CSP Notation for Concurrent Systems
- The complexity of model checking (collapsible) higher-order pushdown systems
- Reachability analysis of communicating pushdown systems
Cited in
(5)
This page was built for publication: Saturation of Concurrent Collapsible Pushdown Systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2963923)
