  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.
