Saturation of Concurrent Collapsible Pushdown Systems
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.
Cite
@article{arxiv.1310.2631,
title = {Saturation of Concurrent Collapsible Pushdown Systems},
author = {Matthew Hague},
journal= {arXiv preprint arXiv:1310.2631},
year = {2013}
}
Comments
Long version of paper appearing in FSTTCS 2013