# Saturation of Concurrent Collapsible Pushdown Systems

M. Hague

(Royal Holloway University of London, and LIGM, Marne-la-Vallée
<EMAIL_ADDRESS>
###### 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.

##  1 Introduction

Pushdown systems augment a finite-state machine with a stack and accurately
model first-order recursion. Such systems then are ideal for the analysis of
sequential first-order programs and several successful tools, such as Moped
[25] and SLAM [3], exist for their analysis. However, the domination of multi-
and many-core machines means that programmers must be prepared to work in
concurrent environments, with several interacting execution threads.

Unfortunately, the analysis of concurrent pushdown systems is well-known to be
undecidable. However, most concurrent programs don’t interact pathologically
and many restrictions on interaction have been discovered that give
decidability (e.g. [5, 6, 26, 14, 15]).

One particularly successful approach is _context-bounding_. This
underapproximates a concurrent system by bounding the number of context
switches that may occur [24]. It is based on the observation that most real-
world bugs require only a small number of thread interactions [23].
Additionally, a number of more relaxed restrictions on stack behaviour have
been introduced. In particular phase-bounded [29], scope-bounded [30], and
ordered [7] (corrected in [2]) systems. There are also generic frameworks —
that bound the tree- [20] or split-width [10] of the interactions between
communication and storage — that give decidability for all communication
architectures that can be defined within them.

Languages such as C++, Haskell, Javascript, Python, or Scala increasingly
embrace higher-order procedure calls, which present a challenge to
verification. A popular approach to modelling higher-order languages for
verification is that of (higher-order recursion) schemes [11, 21, 16].
Collapsible pushdown systems (CPDS) are an extension of pushdown systems [13]
with a “stack-of-stacks” structure. The “collapse” operation allows a CPDS to
retrieve information about the context in which a stack character was created.
These features give CPDS equivalent modelling power to schemes [13].

These two formalisms have good model-checking properties. E.g, it is decidable
whether a $\mu$-calculus formula holds on the execution graph of a scheme [21]
(or CPDS [13]). Although, the complexity of such analyses is high, it has been
shown by Kobayashi [15] (and Broadbent et al. for CPDS [9]) that they can be
performed in practice on real code examples.

However concurrency for these models has been little studied. Work by Seth
considers phase-bounding for CPDS without collapse [27] by reduction to a
finite state parity game. Recent work by Kobayashi and Igarashi studies
context-bounded recursion schemes [17].

Here, we study global reachability problems for ordered, phase-bounded, and
scope-bounded CPDS. We use _saturation_ methods, which have been successfully
implemented by e.g. Moped [25] for pushdown systems and C-SHORe [9] for CPDS.
Saturation was first applied to model-checking by Bouajjani et al. [4] and
Finkel et al. [12]. We presented a saturation technique for CPDS in ICALP 2012
[8]. Here, we present the following advances.

  1. 1.

Global reachability for ordered CPDSs (§5). This is based on Atig’s algorithm
[1] for ordered PDSs and requires a non-trivial generalisation of his notion
of _extended_ PDSs (§3). For this we introduce the notion of _transition
automata_ that encapsulate the behaviour of the saturation algorithm. In
Appendix F we show how to use the same machinery to solve the global
reachability problem for phase-bounded CPDSs.

  2. 2.

Global reachability for scope-bounded CPDSs (§6). This is a backwards analysis
based upon La Torre and Napoli’s forwards analysis for scope-bounded PDSs,
requiring new insights to complete the proofs.

Because the naive encoding of a single second-order stack has an undecidable
MSO theory (we show this folklore result in Appendix A) it remains a
challenging open problem to generalise the generic frameworks above ([20, 10])
to CPDSs, since these frameworks rely on MSO decidability over graph
representations of the storage and communication structure.

##  2 Preliminaries

Before defining CPDSs, we define $2\uparrow_{0}\left({x}\right)=x$ and
$2\uparrow_{i+1}\left({x}\right)=2^{2\uparrow_{i}\left({x}\right)}$.

###  2.1 Collapsible Pushdown Systems (CPDS)

For a readable introduction to CPDS we defer to a survey by Ong [22]. Here, we
can only briefly describe higher-order collapsible stacks and their
operations. We use a notion of collapsible stacks called _annotated stacks_
(which we refer to as collapsible stacks). These were introduced in ICALP
2012, and are essentially equivalent to the classical model [8].

#### Higher-Order Collapsible Stacks

An order-$1$ stack is a stack of symbols from a stack alphabet $\Sigma$, an
order-$n$ stack is a stack of order-$(n-1)$ stacks. A collapsible stack of
order $n$ is an order-$n$ stack in which the stack symbols are annotated with
collapsible stacks which may be of any order $\leq n$. Note, often in examples
we will omit annotations for clarity. We fix the maximal order to $n$, and use
$k$ to range between $n$ and $1$. We simultaneously define for all $1\leq
k\leq n$, the set $\mathrm{Stacks}_{k}^{n}$ of order-$k$ stacks whose symbols
are annotated by stacks of order at most $n$. Note, we use subscripts to
indicate the order of a stack. Furthermore, the definition below uses a least
fixed-point. This ensures that all stacks are finite. An order-$k$ stack is a
collapsible stack in $\mathrm{Stacks}_{k}^{n}$.

######  Definition 2.1 (Collapsible Stacks)

The family of sets $(\mathrm{Stacks}_{k}^{n})_{1\leq k\leq n}$ is the smallest
family (for point-wise inclusion) such that:

  1. 1.

for all $2\leq k\leq n$, $\mathrm{Stacks}_{k}^{n}$ is the set of all (possibly
empty) sequences $[{w_{1}\ldots w_{\ell}}]_{k}$ with
$w_{1},\ldots,w_{\ell}\in\mathrm{Stacks}_{k-1}^{n}$.

  2. 2.

$\mathrm{Stacks}_{1}^{n}$ is all sequences
$[{{a_{1}}^{w_{1}}\ldots{a_{\ell}}^{w_{\ell}}}]_{1}$ with $\ell\geq 0$ and for
all $1\leq i\leq\ell$, $a_{i}$ is a stack symbol in $\Sigma$ and $w_{i}$ is a
collapsible stack in $\bigcup\limits_{1\leq k\leq n}\mathrm{Stacks}_{k}^{n}$.

An order-$n$ stack can be represented naturally as an edge-labelled tree over
the alphabet
$\left\\{{[_{n-1},\ldots,[_{1},]_{1},\ldots,]_{n-1}}\right\\}\uplus\Sigma$,
with $\Sigma$-labelled edges having a second target to the tree representing
the annotation. We do not use $[_{n}$ or $]_{n}$ since they would appear
uniquely at the beginning and end of the stack. An example order-$3$ stack is
given below, with only a few annotations shown (on $a$ and $c$). The
annotations are order-$3$ and order-$2$ respectively.

[nodealign=true,colsep=2ex,rowsep=2ex] $\bullet$ & $\bullet$ $\bullet$
$\bullet$ $\bullet$ $\bullet$ $\bullet$

$\bullet$ $\bullet$ $\bullet$ $\bullet$ $\bullet$ $\bullet$

$\bullet$ $\bullet$ $\bullet$ $\bullet$

^$[_{2}$^$[_{1}$^$a$^$b$^$]_{1}$^$]_{2}$

^$[_{2}$^$[_{1}$^$c$^$]_{1}$^$]_{2}$

^$[_{1}$^$d$^$]_{1}$

Given an order-$n$ stack $w=[{w_{1}\ldots w_{\ell}}]_{n}$, we define
$top_{n+1}(w)=w$ and

$\begin{array}[]{rcll}{top_{n}}\mathord{\left({[{w_{1}\ldots
w_{\ell}}]_{n}}\right)}&=&w_{1}&\text{when $\ell>0$}\\\
{top_{n}}\mathord{\left({[{}]_{n}}\right)}&=&[{}]_{n-1}&\text{otherwise}\\\
{top_{k}}\mathord{\left({[{w_{1}\ldots
w_{\ell}}]_{n}}\right)}&=&{top_{k}}\mathord{\left({w_{1}}\right)}&\text{when
$k<n$ and $\ell>0$}\end{array}$

noting that ${top_{k}}\mathord{\left({w}\right)}$ is undefined if
${top_{k^{\prime}}}\mathord{\left({w}\right)}=[{}]_{k^{\prime}-1}$ for any
$k^{\prime}>k$.

We write ${u}:_{k}{v}$ — where $u$ is order-$(k-1)$ — to denote the stack
obtained by placing $u$ on top of the $top_{k}$ stack of $v$. That is, if
$v=[{v_{1}\ldots v_{\ell}}]_{k}$ then ${u}:_{k}{v}=[{uv_{1}\ldots
v_{\ell}}]_{k}$, and if $v=[{v_{1}\ldots v_{\ell}}]_{k^{\prime}}$ with
$k^{\prime}>k$, ${u}:_{k}{v}=[{\left({{u}:_{k}{v_{1}}}\right)v_{2}\ldots
v_{\ell}}]_{k^{\prime}}$. This composition associates to the right. E.g., the
stack $[{[{[{{a}^{w}b}]_{1}}]_{2}}]_{3}$ above can be written ${u}:_{3}{v}$
where $u$ is the order-$2$ stack $[{[{{a}^{w}b}]_{1}}]_{2}$ and $v$ is the
empty order-$3$ stack $[{}]_{3}$. Then ${u}:_{3}{{u}:_{3}{v}}$ is
$[{[{[{{a}^{w}b}]_{1}}]_{2}[{[{{a}^{w}b}]_{1}}]_{2}}]_{3}$.

#### Operations on Order-$n$ Collapsible Stacks

The following operations can be performed on an order-$n$ stack where $noop$
is the null operation ${noop}\mathord{\left({w}\right)}=w$.

$\begin{array}[]{rcl}\mathcal{O}_{n}&=&\left\\{{noop,pop_{1}}\right\\}\cup\left\\{{rew_{a},push^{k}_{a},copy_{k},pop_{k}}\
\left|\ {a\in\Sigma\land 2\leq k\leq n}\right.\right\\}\end{array}$

We define each $o\in\mathcal{O}_{n}$ for an order-$n$ stack $w$. Annotations
are created by $push^{k}_{a}$, which pushes a character onto $w$ and annotates
it with
${top_{k+1}}\mathord{\left({{pop_{k}}\mathord{\left({w}\right)}}\right)}$.
This, in essence, attaches a closure to a new character.

  1. 1.

We set ${pop_{k}}\mathord{\left({{u}:_{k}{v}}\right)}=v$.

  2. 2.

We set ${copy_{k}}\mathord{\left({{u}:_{k}{v}}\right)}={u}:_{k}{{u}:_{k}{v}}$.

  3. 3.

We set
${collapse_{k}}\mathord{\left({{{a}^{u^{\prime}}}:_{1}{{u}:_{(k+1)}{v}}}\right)}={u^{\prime}}:_{(k+1)}{v}$
when $u$ is order-$k$ and $1\leq k<n$; and
${collapse_{n}}\mathord{\left({{{a}^{u}}:_{1}{v}}\right)}=u$ when $u$ is
order-$n$.

  4. 4.

We set ${push^{k}_{b}}\mathord{\left({w}\right)}={{b}^{u}}:_{1}{w}$ where
$u={top_{k+1}}\mathord{\left({{pop_{k}}\mathord{\left({w}\right)}}\right)}$.

  5. 5.

We set
${rew_{b}}\mathord{\left({{{a}^{u}}:_{1}{v}}\right)}={{b}^{u}}:_{1}{v}$.

For example, beginning with $[{[{a}]_{1}[{b}]_{1}}]_{2}$ and applying
$push^{2}_{c}$ we obtain $[{[{{c}^{[{[{b}]_{1}}]_{2}}a}]_{1}[{b}]_{1}}]_{2}$.
In this setting, the order-$2$ context information for the new character $c$
is $[{[{b}]_{1}}]_{2}$. We can then apply $copy_{2};collapse_{2}$ to get
$[{[{{c}^{[{[{b}]_{1}}]_{2}}a}]_{1}[{{c}^{[{[{b}]_{1}}]_{2}}a}]_{1}[{b}]_{1}}]_{2}$
then $[{[{b}]_{1}}]_{2}$. That is, $collapse_{k}$ replaces the current
$top_{k+1}$ stack with the annotation attached to $c$.

#### Collapsible Pushdown Systems

We are now ready to define collapsible PDS.

######  Definition 2.2 (Collapsible Pushdown Systems)

An order-$n$ _collapsible pushdown system ( $n$-CPDS)_ is a tuple
$\mathcal{C}=\left({\mathcal{P},\Sigma,\mathcal{R}}\right)$ where
$\mathcal{P}$ is a finite set of control states, $\Sigma$ is a finite stack
alphabet, and
$\mathcal{R}\subseteq\left({\mathcal{P}\times\Sigma\times\mathcal{O}_{n}\times\mathcal{P}}\right)$
is a set of rules.

We write _configurations_ of a CPDS as a pair
$\langle{p},{w}\rangle\in\mathcal{P}\times\mathrm{Stacks}_{n}^{n}$. We have a
transition
$\langle{p},{w}\rangle\longrightarrow\langle{p^{\prime}},{w^{\prime}}\rangle$
via a rule $\left({{p},{a},{o},{p^{\prime}}}\right)$ when
${top_{1}}\mathord{\left({w}\right)}=a$ and
$w^{\prime}={o}\mathord{\left({w}\right)}$.

#### Consuming and Generating Rules

We distinguish two kinds of rule or operation: a rule
$\left({{p},{a},{o},{p^{\prime}}}\right)$ or operation $o$ is _consuming_ if
$o=pop_{k}$ or $o=collapse_{k}$ for some $k$. Otherwise, it is _generating_.
We write $\mathcal{R}^{{\mathcal{P}},{\Sigma}}_{\mathcal{G}_{n}}$ for the set
of generating rules of the form $\left({{p},{a},{o},{p^{\prime}}}\right)$ such
that $p,p^{\prime}\in\mathcal{P}$ and $a\in\Sigma$, and $o\in\mathcal{O}_{n}$.
We simply write $\mathcal{R}_{\mathcal{G}_{n}}$ when no confusion may arise.

###  2.2 Saturation for CPDS

Our algorithms for concurrent CPDSs build upon the saturation technique for
CPDSs [8]. In essence, we represent sets of configurations $C$ using a
$\mathcal{P}$-stack automaton $A$ reading stacks. We define such automata and
their languages ${\mathcal{L}}\mathord{\left({A}\right)}$ below. Saturation
adds new transitions to $A$ — depending on rules of the CPDS and existing
transitions in $A$ — to obtain $A^{\prime}$ representing configurations with a
path to a configuration in $C$. I.e., given a CPDS $\mathcal{C}$ with control
states $\mathcal{P}$ and a $\mathcal{P}$-stack automaton $A_{0}$, we compute
${Pre^{*}_{\mathcal{C}}}\mathord{\left({A_{0}}\right)}$ which is the smallest
set s.t.
${Pre^{*}_{\mathcal{C}}}\mathord{\left({A_{0}}\right)}\supseteq{\mathcal{L}}\mathord{\left({A_{0}}\right)}$
and
${Pre^{*}_{\mathcal{C}}}\mathord{\left({A_{0}}\right)}\supseteq\left\\{{\langle{p},{w}\rangle}\
\left|\
{\exists\langle{p},{w}\rangle\longrightarrow\langle{p^{\prime}},{w^{\prime}}\rangle\;\textrm{s.t.\;}\langle{p^{\prime}},{w^{\prime}}\rangle\in{Pre^{*}_{\mathcal{C}}}\mathord{\left({A_{0}}\right)}}\right.\right\\}$.

#### Stack Automata

Sets of stacks are represented using order-$n$ stack automata. These are
alternating automata with a nested structure that mimics the nesting in a
higher-order collapsible stack. We recall the definition below.

######  Definition 2.3 (Order-$n$ Stack Automata)

An _order- $n$ stack automaton_ is a tuple
$A=\left({\mathbb{Q}_{n},\ldots,\mathbb{Q}_{1},\Sigma,\Delta_{n},\ldots,\Delta_{1},\mathcal{F}_{n},\ldots,\mathcal{F}_{1}}\right)$
where $\Sigma$ is a finite stack alphabet,
$\mathbb{Q}_{n},\ldots,\mathbb{Q}_{1}$ are disjoint, and

  1. 1.

for all $2\leq k\leq n$, we have $\mathbb{Q}_{k}$ is a finite set of states,
$\mathcal{F}_{k}\subseteq\mathbb{Q}_{k}$ is a set of accepting states, and
$\Delta_{k}\subseteq\mathbb{Q}_{k}\times\mathbb{Q}_{k-1}\times
2^{\mathbb{Q}_{k}}$ is a transition relation such that for all $q$ and $Q$
there is _at most one_ $q^{\prime}$ with
$\left({q,q^{\prime},Q}\right)\in\Delta_{k}$, and

  2. 2.

$\mathbb{Q}_{1}$ is a finite set of states,
$\mathcal{F}_{1}\subseteq\mathbb{Q}_{1}$ is a set of accepting states, and the
transition relation is $\Delta_{1}\subseteq\bigcup\limits_{2\leq k\leq
n}\left({\mathbb{Q}_{1}\times\Sigma\times 2^{\mathbb{Q}_{k}}\times
2^{\mathbb{Q}_{1}}}\right)$.

States in $\mathbb{Q}_{k}$ recognise order-$k$ stacks. Stacks are read from
“top to bottom”. A stack ${u}:_{k}{v}$ is accepted from $q$ if there is a
transition $\left({q,q^{\prime},Q}\right)\in\Delta_{k}$, written
$q\xrightarrow{q^{\prime}}Q$, such that $u$ is accepted from
$q^{\prime}\in\mathbb{Q}_{(k-1)}$ and $v$ is accepted from each state in $Q$.
At order-$1$, a stack ${{a}^{u}}:_{1}{v}$ is accepted from $q$ if there is a
transition $\left({q,a,Q_{col},Q}\right)$ where $u$ is accepted from all
states in $Q_{col}$ and $v$ is accepted from all states in $Q$. An empty
order-$k$ stack is accepted by any state in $\mathcal{F}_{k}$. We write
$w\in{\mathcal{L}_{q}}\mathord{\left({A}\right)}$ to denote the set of all
stacks $w$ accepted from $q$. Note that a transition to the empty set is
distinct from having no transition.

We show a part run using $q_{3}\xrightarrow{q_{2}}Q_{3}\in\Delta_{3}$,
$q_{2}\xrightarrow{q_{1}}Q_{2}\in\Delta_{2}$,
$q_{1}\xrightarrow[Q_{col}]{a}Q_{1}\in\Delta_{1}$.

[nodealign=true,colsep=2ex,rowsep=2ex] hich return a set of long-form
transitions to be added by saturation. When $r$ is consuming,
${\Pi_{r}}\mathord{\left({A}\right)}$ returns the set of long-form transitions
to be added to $A$ due to the rule $r$. When $r$ is generating $\Pi_{r}$ also
takes as an argument a long-form transition $t$ of $A$. Thus
${\Pi_{r}}\mathord{\left({t,A}\right)}$ returns the set of long-form
transitions that should be added to $A$ as a result of the rule $r$ combined
with the transition $t$ (and possibly other transitions of $A$).

For example, if $r=\left({{p},{a},{rew_{b}},{p^{\prime}}}\right)$ and
$t={q_{p^{\prime}}}\xrightarrow[Q_{col}]{b}\left({{Q_{1},\ldots,Q_{n}}}\right)$
is a transition of $A$, then ${\Pi_{r}}\mathord{\left({t,A}\right)}$ contains
only the long-form transition
$t^{\prime}={q_{p}}\xrightarrow[Q_{col}]{a}\left({{Q_{1},\ldots,Q_{n}}}\right)$.
The idea is if $\langle{p^{\prime}},{{{b}^{u}}:_{1}{w}}\rangle$ is accepted by
$A$ via a run whose first (sequence of) transition(s) is $t$, then by adding
$t^{\prime}$ we will be able to accept $\langle{p},{{{a}^{u}}:_{1}{w}}\rangle$
via a run beginning with $t^{\prime}$ instead of $t$. We have
$\langle{p},{{{a}^{u}}:_{1}{w}}\rangle\in{Pre^{*}_{\mathcal{C}}}\mathord{\left({A}\right)}$
since it can reach $\langle{p^{\prime}},{{{b}^{u}}:_{1}{w}}\rangle$ via the
rule $r$.

######  Definition 2.4 (The Saturation Function $\Pi$)

For a CPDS with rules $\mathcal{R}$, and given an order-$n$ stack automaton
$A_{i}$ we define $A_{i+1}={\Pi}\mathord{\left({A_{i}}\right)}$. The state-
sets of $A_{i+1}$ are defined implicitly by the transitions which are those in
$A_{i}$ plus, for each
$r=\left({{p},{a},{o},{p^{\prime}}}\right)\in\mathcal{R}$, when

  1. 1.

$o$ is consuming and $t\in{\Pi_{r}}\mathord{\left({A_{i}}\right)}$, then add
$t$ to $A_{i+1}$,

  2. 2.

$o$ is generating, $t$ is in $A_{i}$, and
$t^{\prime}\in{\Pi_{r}}\mathord{\left({t,A}\right)}$, then add $t^{\prime}$ to
$A_{i+1}$.

In ICALP 2012 we showed that saturation adds up to
${\mathcal{O}}\mathord{\left({2\uparrow_{n}\left({{f}\mathord{\left({\left|{\mathcal{P}}\right|}\right)}}\right)}\right)}$
transitions, for some polynomial $f$, and that this can be reduced to
${\mathcal{O}}\mathord{\left({2\uparrow_{n-1}\left({{f}\mathord{\left({\left|{\mathcal{P}}\right|}\right)}}\right)}\right)}$
(which is optimal) by restricting all $Q_{n}$ to have size $1$ when $A_{0}$ is
“non-alternating at order-$n$”. Since this property holds of all $A_{0}$ used
here, we use the optimal algorithm for complexity arguments.

##  3 Extended Collapsible Pushdown Systems

To analyse concurrent systems, we extend CPDS following Atig [1]. Atig’s
extended PDSs allow words from arbitrary languages to be pushed on the stack.
Our notion of extended CPDSs allows sequences of _generating operations_ from
a language ${\mathcal{L}_{g}}$ to be applied, rather than a single operation
per rule. We can specify ${\mathcal{L}_{g}}$ by any system (e.g. a Turing
machine).

######  Definition 3.1 (Extended CPDSs)

An order-$n$ _extended CPDS ( $n$-ECPDS)_ is a tuple
$\mathcal{C}=\left({\mathcal{P},\Sigma,\mathcal{R}}\right)$ where
$\mathcal{P}$ is a finite set of control states, $\Sigma$ is a finite stack
alphabet, and
$\mathcal{R}\subseteq\left({\mathcal{P}\times\Sigma\times\mathcal{O}_{n}\times\mathcal{P}}\right)\cup\left({\mathcal{P}\times\Sigma\times
2^{\left({\mathcal{R}^{{\mathcal{P}},{\Sigma}}_{\mathcal{G}_{n}}}\right)^{\ast}}\times\mathcal{P}}\right)$
is a set of rules.

As before, we have a transition
$\langle{p},{w}\rangle\longrightarrow\langle{p^{\prime}},{w^{\prime}}\rangle$
of an $n$-ECPDS via a rule $\left({{p},{a},{o},{p^{\prime}}}\right)$ with
${top_{1}}\mathord{\left({w}\right)}=a$ and
$w^{\prime}={o}\mathord{\left({w}\right)}$. Additionally, we have a transition
$\langle{p},{w}\rangle\longrightarrow\langle{p^{\prime}},{w^{\prime}}\rangle$
when we have a rule $\left({{p},{a},{{\mathcal{L}_{g}}},{p^{\prime}}}\right)$,
a sequence
$\left({{p},{a},{o_{1}},{p_{1}}}\right)\left({{p_{1}},{a_{2}},{o_{2}},{p_{2}}}\right)\ldots\left({{p_{\ell-1}},{a_{\ell}},{o_{\ell}},{p^{\prime}}}\right)\in{\mathcal{L}_{g}}$
and
$w^{\prime}={o_{\ell}}\mathord{\left({\cdots{o_{1}}\mathord{\left({w}\right)}}\right)}$.
That is, a single extended rule may apply a sequence of stack updates in one
step. A run of an ECPDS is a sequence
$\langle{p_{0}},{w_{0}}\rangle\longrightarrow\langle{p_{1}},{w_{1}}\rangle\longrightarrow\cdots$.

###  3.1 Reachability Analysis

We adapt saturation for ECPDSs. In Atig’s algorithm, an essential property is
the decidability of
${\mathcal{L}_{g}}\cap{\mathcal{L}}\mathord{\left({A}\right)}$ for some
order-1 $\mathcal{P}$-stack automaton $A$ and a language ${\mathcal{L}_{g}}$
appearing in a rule of the extended PDS. We need analogous machinery in our
setting. For this, we first define a class of finite automata called
_transition_ automata, written $\mathcal{T}$. The states of these automata
will be long-form transitions of a stack automaton
$t={q}\xrightarrow[Q_{col}]{a}\left({{Q_{1},\ldots,Q_{n}}}\right)$.
Transitions $t\xrightarrow{r}t^{\prime}$ are labelled by rules. We write
$t\xrightarrow{\overrightarrow{r}}_{\ast}t^{\prime}$ to denote a run over
$\overrightarrow{r}\in\left({\mathcal{R}_{\mathcal{G}_{n}}}\right)^{\ast}$.

During the saturation algorithm we will build from $A_{i}$ a transition
automaton $\mathcal{T}$. Then, for each rule
$\left({{p},{a},{{\mathcal{L}_{g}}},{p^{\prime}}}\right)$ we add to $A_{i+1}$
a new long-form transition $t$ if there is a word
$\overrightarrow{r}\in{\mathcal{L}_{g}}$ such that
$t\xrightarrow{\overrightarrow{r}}_{\ast}t^{\prime}$ is a run of $\mathcal{T}$
and $t^{\prime}$ is already a transition of $A_{i}$.

For example, consider
$\left({{p},{a},{{\mathcal{L}_{g}}},{p^{\prime}}}\right)$ where
${\mathcal{L}_{g}}=\left\\{{\left({{p},{a},{rew_{b}},{p^{\prime}}}\right)}\right\\}$.
A transition

$\left({{q_{p}}\xrightarrow[Q_{col}]{a}\left({{Q_{1},\ldots,Q_{n}}}\right)}\right)\xrightarrow{\left({{p},{a},{rew_{b}},{p^{\prime}}}\right)}\left({{q_{p^{\prime}}}\xrightarrow[Q_{col}]{b}\left({{Q_{1},\ldots,Q_{n}}}\right)}\right)$

will correspond to the fact that the presence of
${q_{p^{\prime}}}\xrightarrow[Q_{col}]{b}\left({{Q_{1},\ldots,Q_{n}}}\right)$
in $A_{i}$ causes
${q_{p}}\xrightarrow[Q_{col}]{a}\left({{Q_{1},\ldots,Q_{n}}}\right)$ to be
added by $\Pi$. A run $t_{1}\xrightarrow{r_{1}}t_{2}\xrightarrow{r_{2}}t_{3}$
comes into play when e.g. ${\mathcal{L}_{g}}=\left\\{{r_{1}r_{2}}\right\\}$.
If the rule were split into two ordinary rules with intermediate control
states, $\Pi$ would first add $t_{2}$ derived from $t_{3}$, and then from
$t_{2}$ derive $t_{1}$. In the case of extended CPDSs, the intermediate
transition $t_{2}$ is not added to $A_{i+1}$, but its effect is still present
in the addition of $t_{1}$. Below, we repeat the above intuition more
formally. Fix a $n$-ECPDS
$\mathcal{C}=\left({\mathcal{P},\Sigma,\mathcal{R}}\right)$.

#### Transition Automata

We build a transition automaton from a given $\mathcal{P}$-stack automaton
$A$. Let $A$ have order-$n$ to order-$1$ state-sets $Q_{n},\ldots,Q_{1}$ and
alphabet $\Sigma$, let $T_{A}$ be the set of all
${q}\xrightarrow[Q_{col}]{a}\left({{Q_{1},\ldots,Q_{n}}}\right)$ with $q\in
Q_{n}$, for all $k$, $Q_{k}\subseteq\mathbb{Q}_{k}$, and for some $k$,
$Q_{col}\subseteq\mathbb{Q}_{k}$.

######  Definition 3.2 (Transition Automata)

Given an order-$n$ $\mathcal{P}$-stack automaton $A$ with alphabet $\Sigma$,
and $t,t^{\prime}\in T_{A}$, we define the transition automaton
$\mathcal{T}^{A}_{{t},{t^{\prime}}}=\left({T_{A},\mathcal{R}^{{\mathcal{P}},{\Sigma}}_{\mathcal{G}_{n}},\delta,t,t^{\prime}}\right)$
such that $\delta\subseteq
T_{A}\times\mathcal{R}^{{\mathcal{P}},{\Sigma}}_{\mathcal{G}_{n}}\times T_{A}$
is the smallest set such that $t_{1}\xrightarrow{r}t_{2}\in\delta$ if
$t_{1}\in{\Pi_{r}}\mathord{\left({t_{2},A}\right)}$.

We define
${\mathcal{L}}\mathord{\left({\mathcal{T}^{A}_{{t},{t^{\prime}}}}\right)}=\left\\{{\overrightarrow{r}}\
\left|\ {t\xrightarrow{\overrightarrow{r}}_{\ast}t^{\prime}}\right.\right\\}$.

#### Extended Saturation Function

We now extend the saturation function following the intuition explained above.
For $t={q_{p}}\xrightarrow[Q_{col}]{a}\left({{Q_{1},\ldots,Q_{n}}}\right)$,
let ${top_{1}}\mathord{\left({t}\right)}=a$ and
${control}\mathord{\left({t}\right)}=p$.

######  Definition 3.3 (Extended Saturation Function $\Pi$)

The extended $\Pi$ is $\Pi$ from Definition 2.4 plus for each extended rule
$\left({{p},{a},{{\mathcal{L}_{g}}},{p^{\prime}}}\right)\in\mathcal{R}$ and
$t,t^{\prime}$, we add $t$ to $A_{i+1}$ whenever  1.
${control}\mathord{\left({t}\right)}=p$and
${top_{1}}\mathord{\left({t}\right)}=a$,  2. $t^{\prime}$is a transition of
$A_{i}$ with ${control}\mathord{\left({t^{\prime}}\right)}=p^{\prime}$, and
3.
${\mathcal{L}_{g}}\cap{\mathcal{L}}\mathord{\left({\mathcal{T}^{A_{i}}_{{t},{t^{\prime}}}}\right)}\neq\emptyset$.

######  Theorem 3.1 (Global Reachability of ECPDS)

Given an ECPDS $\mathcal{C}$ and a $\mathcal{P}$-stack automaton $A_{0}$, the
fixed point $A$ of the extended saturation procedure accepts
${Pre^{*}_{\mathcal{C}}}\mathord{\left({A_{0}}\right)}$.

In order for the saturation algorithm to be effective, we need to be able to
decide
${\mathcal{L}_{g}}\cap{\mathcal{L}}\mathord{\left({\mathcal{T}^{A_{i}}_{{t},{t^{\prime}}}}\right)}\neq\emptyset$.
We argue in the appendix that number of transitions added by extended
saturation has the same upper bound as the unextended case.

##  4 Multi-Stack CPDSs

We define a general model of concurrent collapsible pushdown systems, which we
later restrict. In the sequel, assume a bottom-of-stack symbol $\perp$ and
define the “empty” stacks $\perp_{0}=\perp$ and
$\perp_{k+1}=[{\perp_{k}}]_{k+1}$. As standard, we assume that $\perp$ is
neither pushed onto, nor popped from, the stack (though may be copied by
$copy_{k}$).

######  Definition 4.1 (Multi-Stack Collapsible Pushdown Systems)

An order-$n$ _multi-stack collapsible pushdown system ( $n$-MCPDS)_ is a tuple
$\mathcal{C}=\left({\mathcal{P},\Sigma,\mathcal{R}_{1},\ldots,\mathcal{R}_{m}}\right)$
where $\mathcal{P}$ is a finite set of control states, $\Sigma$ is a finite
stack alphabet, and for each $1\leq i\leq m$ we have a set of rules
$\mathcal{R}_{i}\subseteq\mathcal{P}\times\Sigma\times\mathcal{O}_{n}\times\mathcal{P}$.

A configuration of $\mathcal{C}$ is a tuple
$\langle{p},{w_{1},\ldots,w_{m}}\rangle$. There is a transition
$\langle{p},{w_{1},\ldots,w_{m}}\rangle\longrightarrow\langle{p^{\prime}},{w_{1},\ldots,w_{i-1},w^{\prime}_{i},w_{i+1},\ldots,w_{m}}\rangle$
via $\left({{p},{a},{o},{p^{\prime}}}\right)\in\mathcal{R}_{i}$ when
$a={top_{1}}\mathord{\left({w_{i}}\right)}$ and
$w^{\prime}_{i}={o}\mathord{\left({w_{i}}\right)}$.

We also need MCPD _Automata_ , which are MCPDSs defining languages over an
input alphabet $\Gamma$. For this, we add labelling input characters to the
rules. Thus, a rule $\left({{p},{a},{\gamma},{o},{p^{\prime}}}\right)$ reads a
character $\gamma\in\Gamma$. This is defined formally in Appendix D.

We are interested in two problems for a given $n$-MCPDS $\mathcal{C}$.

######  Definition 4.2 (Control State Reachability Problem)

Given control states ${p_{\text{in}}},{p_{\text{out}}}$ of $\mathcal{C}$,
decide if there is for some $w_{1},\ldots,w_{m}$ a run
$\langle{{p_{\text{in}}}},{\perp_{n},\ldots,\perp_{n}}\rangle\longrightarrow\cdots\longrightarrow\langle{{p_{\text{out}}}},{w_{1},\ldots,w_{m}}\rangle$.

######  Definition 4.3 (Global Control State Reachability Problem)

Given a control state ${p_{\text{out}}}$ of $\mathcal{C}$, construct a
representation of the set of configurations
$\langle{p},{w_{1},\ldots,w_{m}}\rangle$ such that there exists for some
$w^{\prime}_{1},\ldots,w^{\prime}_{m}$ a run
$\langle{p},{w_{1},\ldots,w_{m}}\rangle\longrightarrow\cdots\longrightarrow\langle{{p_{\text{out}}}},{w^{\prime}_{1},\ldots,w^{\prime}_{m}}\rangle$.

We represent sets of configurations as follows. In Appendix D we show it forms
an effective boolean algebra, membership is linear time, and emptiness is in
PSPACE.

######  Definition 4.4 (Regular Set of Configurations)

A regular set $R$ of configurations of a multi-stack CPDS $\mathcal{C}$ is
definable via a finite set $\chi$ of tuples
$\left({p,A_{1},\ldots,A_{m}}\right)$ where $p$ is a control state of
$\mathcal{C}$ and $A_{i}$ is a stack automaton with designated initial state
$q_{i}$ for each $i$. We have $\langle{p},{w_{1},\ldots,w_{m}}\rangle\in R$
iff there is some $\left({p,A_{1},\ldots,A_{m}}\right)\in\chi$ such that
$w_{i}\in{\mathcal{L}_{q_{i}}}\mathord{\left({A_{i}}\right)}$ for each $i$.

Finally, we often partition runs of an MCPDS
$\sigma=\sigma_{1}\ldots\sigma_{\ell}$ where each $\sigma_{i}$ is a sequence
of configurations of the MCPDS. A transition from $c$ to $c^{\prime}$ occurs
in segment $\sigma_{i}$ if $c^{\prime}$ is a configuration in $\sigma_{i}$.
Thus, transitions from $\sigma_{i}$ to $\sigma_{i+1}$ are said to belong to
$\sigma_{i+1}$.

##  5 Ordered CPDS

We generalise _ordered multi-stack pushdown systems_ [7]. Intuitively, we can
only remove characters from stack $i$ whenever all stacks $j<i$ are empty.

######  Definition 5.1 (Ordered CPDS)

An order-$n$ _ordered CPDS_ ($n$-OCPDS) is an $n$-MCPDS
$\mathcal{C}=\left({\mathcal{P},\Sigma,\mathcal{R}_{1},\ldots,\mathcal{R}_{m}}\right)$
such that a transition from $\langle{p},{w_{1},\ldots,w_{m}}\rangle$ using the
rule $r$ on stack $i$ is permitted iff, when $r$ is consuming, for all $1\leq
j<i$ we have $w_{j}=\perp_{n}$.

######  Theorem 5.1 (Decidability of Reachability Problems)

For $n$-OCPDSs the control state reachability problem and the global control
state reachability problem are decidable.

We outline the proofs below. In Appendix E we show control state reachability
uses
${\mathcal{O}}\mathord{\left({2\uparrow_{m(n-1)}\left({\ell}\right)}\right)}$
time, where $\ell$ is polynomial in the size of the OCPDS, and we have at most
${\mathcal{O}}\mathord{\left({2\uparrow_{mn}\left({\ell}\right)}\right)}$
tuples in the solution to the global problem. First observe that reachability
can be reduced to reaching
$\langle{{p_{\text{out}}}},{\perp_{n},\ldots,\perp_{n}}\rangle$ by clearing
the stacks at the end of the run.

#### Control State Reachability

Using our notion of ECPDS, we may adapt Atig’s inductive algorithm for ordered
PDSs [1] for the control state reachability problem. The induction is over the
number of stacks. W.l.o.g. we assume that all rules
$\left({{p},{\perp},{o},{p^{\prime}}}\right)$ of $\mathcal{C}$ have
$o=push^{n}_{a}$.

In the base case, we have an $n$-OCPDS with a single stack, for which the
global reachability problem is known to be decidable (e.g. [4]).

In the inductive case, we have an $n$-OCPDS $\mathcal{C}$ with $m$ stacks. By
induction, we can decide the reachability problem for $n$-OCPDSs with fewer
than $m$ stacks. We first show how to reduce the problem to reachability
analysis of an extended CPDS, and then finally we show how to decide
${\mathcal{L}_{g}}\cap{\mathcal{L}}\mathord{\left({\mathcal{T}^{A_{i}}_{{t},{t^{\prime}}}}\right)}\neq\emptyset$
using an $n$-OCPDS with $(m-1)$ stacks.

Consider the $m$th stack of $\mathcal{C}$. A run of $\mathcal{C}$ can be split
into $\sigma_{1}\tau_{1}\sigma_{2}\tau_{2}\ldots\sigma_{\ell}\tau_{\ell}$.
During the subruns $\sigma_{i}$, the first $(m-1)$ stacks are non-empty, and
during $\tau_{i}$, the first $(m-1)$ stacks are empty. Moreover, during each
$\sigma_{i}$, only generating operations may occur on stack $m$.

We build an extended CPDS that directly models the $m$th stack during the
$\tau_{i}$ segments where the first $(m-1)$ stacks are empty, and uses rules
of the form $\left({{p},{a},{{\mathcal{L}_{g}}},{p^{\prime}}}\right)$ to
encapsulate the behaviour of the $\sigma_{i}$ sections where the first $(m-1)$
stacks are non-empty. The ${\mathcal{L}_{g}}$ attached to such a rule is the
sequence of updates applied to the $m$th stack during $\sigma_{i}$.

We begin by defining, from the OCPDS $\mathcal{C}$ with $m$ stacks, an OCPDA
$\mathcal{C}^{L}$ with $(m-1)$ stacks. This OCPDA will be used to define the
${\mathcal{L}_{g}}$ described above. $\mathcal{C}^{L}$ simulates a segment
$\sigma_{i}$. Since all updates to stack $m$ in $\sigma_{i}$ are generating,
$\mathcal{C}^{L}$ need only track its top character, hence only keeps $(m-1)$
stacks. The top character of stack $m$ is kept in the control state, and the
operations that would have occurred on stack $m$ are output.

######  Definition 5.2 ($\mathcal{C}^{L}$)

Given an $n$-OCPDS
$\mathcal{C}=\left({\mathcal{P},\Sigma,\mathcal{R}_{1},\ldots,\mathcal{R}_{m}}\right)$,
we define $\mathcal{C}^{L}$ to be an $n$-OCPDA with $(m-1)$ stacks
$\left({\mathcal{P}\times\Sigma,\Sigma,\mathcal{R}^{\prime}_{1}\cup\mathcal{R}^{\prime},\mathcal{R}^{\prime}_{2},\ldots,\mathcal{R}^{\prime}_{m-1}}\right)$
over input alphabet $\mathcal{R}_{\mathcal{G}_{n}}$ where for all $i$

$\mathcal{R}^{\prime}_{i}=\left\\{{\left({{\left({p,a}\right)},{b},{\left({{p},{a},{noop},{p^{\prime}}}\right)},{o},{\left({p^{\prime},a}\right)}}\right)}\
\left|\
{a\in\Sigma\land\left({{p},{b},{o},{p^{\prime}}}\right)\in\mathcal{R}_{i}}\right.\right\\}\text{,
and}$
$\begin{array}[]{rcl}\mathcal{R}^{\prime}&=&\left\\{{\left({{\left({p,a}\right)},{b},{r},{noop},{\left({p^{\prime},c}\right)}}\right)}\
\left|\ {b\in\Sigma\land
r=\left({{p},{a},{rew_{c}},{p^{\prime}}}\right)\in\mathcal{R}_{m}}\right.\right\\}\
\cup\\\
&&\left\\{{\left({{\left({p,a}\right)},{b},{r},{noop},{\left({p^{\prime},a}\right)}}\right)}\
\left|\ {b\in\Sigma\land
r=\left({{p},{a},{copy_{k}},{p^{\prime}}}\right)\in\mathcal{R}_{m}}\right.\right\\}\
\cup\\\
&&\left\\{{\left({{\left({p,a}\right)},{b},{r},{noop},{\left({p^{\prime},c}\right)}}\right)}\
\left|\ {b\in\Sigma\land
r=\left({{p},{a},{push^{k}_{c}},{p^{\prime}}}\right)\in\mathcal{R}_{m}}\right.\right\\}\
\cup\\\
&&\left\\{{\left({{\left({p,a}\right)},{b},{r},{noop},{\left({p^{\prime},a}\right)}}\right)}\
\left|\ {b\in\Sigma\land
r=\left({{p},{a},{noop},{p^{\prime}}}\right)\in\mathcal{R}_{m}}\right.\right\\}\
.\end{array}$

We define the language
${\mathcal{L}^{{b},{i}}_{{p},{a},{p^{\prime}}}}\mathord{\left({\mathcal{C}^{L}}\right)}$
to be the set of words $\gamma_{1}\ldots\gamma_{\ell}$ such that there exists
a run of $\mathcal{C}^{L}$ over input $\gamma_{1}\ldots\gamma_{\ell}$ from
$\langle{\left({p,a}\right)},{w_{1},\ldots,w_{m-1}}\rangle$ to
$\langle{\left({p^{\prime},c}\right)},{\perp_{n},\ldots,\perp_{n}}\rangle$ for
some $c$, where $w_{i}={push^{n}_{b}}\mathord{\left({\perp_{n}}\right)}$ and
$w_{j}=\perp_{n}$ for all $j\neq i$. This language describes the effect on
stack $m$ of a run $\sigma_{j}$ from $p$ to $p^{\prime}$. (Note, by
assumption, all $\sigma_{j}$ start with some $push^{n}_{b}$.)

We now define the extended CPDS $\mathcal{C}^{R}$ that simulates $\mathcal{C}$
by keeping track of stack $m$ in its stack and using extended rules based on
$\mathcal{C}^{L}$ to simulate parts of the run where the first $(m-1)$ stacks
are not all empty. Note, since all rules operating on $\perp$ (i.e.
$\left({{p},{\perp},{o},{p^{\prime}}}\right)$) have $o=push^{n}_{b}$, rules
from $\mathcal{R}_{1},\ldots,\mathcal{R}_{m-1}$ may only fire during (or at
the start of) the segments where the first $(m-1)$ stacks are non-empty (and
thus appear in $\mathcal{R}_{\mathcal{L}_{g}}$ below).

######  Definition 5.3 ($\mathcal{C}^{R}$)

Given an $n$-OCPDS
$\mathcal{C}=\left({\mathcal{P}\times\Sigma,\Sigma,\mathcal{R}_{1},\ldots,\mathcal{R}_{m}}\right)$
with $m$ stacks, we define $\mathcal{C}^{R}$ to be an $n$-ECPDS such that
$\mathcal{C}^{R}=\left({\mathcal{P},\Sigma,\mathcal{R}^{\prime}}\right)$ where
$\mathcal{R}^{\prime}=\mathcal{R}_{m}\cup\mathcal{R}_{\mathcal{L}_{g}}$ and

$\mathcal{R}_{\mathcal{L}_{g}}=\left\\{{\left({{p},{a},{{\mathcal{L}^{{b},{i}}_{{p_{1}},{a},{p_{2}}}}\mathord{\left({\mathcal{C}^{L}}\right)}},{p_{2}}}\right)}\
\left|\
{a\in\Sigma\land\left({{p},{\perp},{push^{n}_{b}},{p_{1}}}\right)\in\mathcal{R}_{i}\land
1\leq i<m}\right.\right\\}$

######  Lemma 5.1 ($\mathcal{C}^{R}$ simulates $\mathcal{C}$)

Given an $n$-OCPDS $\mathcal{C}$ and control states
${p_{\text{in}}},{p_{\text{out}}}$, we have
$\langle{{p_{\text{in}}}},{w}\rangle\in{Pre^{*}_{\mathcal{C}^{R}}}\mathord{\left({A}\right)}$,
where $A$ is the $\mathcal{P}$-stack automaton accepting only the
configuration $\langle{{p_{\text{out}}}},{\perp_{n}}\rangle$ iff
$\langle{{p_{\text{in}}}},{\perp_{n},\ldots,\perp_{n},w}\rangle\longrightarrow\cdots\longrightarrow\langle{{p_{\text{out}}}},{\perp_{n},\ldots,\perp_{n}}\rangle$.

Lemma 5.1 only gives an effective decision procedure if we can decide
${\mathcal{L}_{g}}\cap{\mathcal{L}}\mathord{\left({\mathcal{T}^{A_{i}}_{{t},{t^{\prime}}}}\right)}\neq\emptyset$
for all rules $\left({{p},{a},{{\mathcal{L}_{g}}},{p^{\prime}}}\right)$
appearing in $\mathcal{C}^{R}$. For this, we use a standard product
construction between the $\mathcal{C}^{L}$ associated with
${\mathcal{L}_{g}}$, and $\mathcal{T}^{A_{i}}_{{t},{t^{\prime}}}$. This gives
an ordered CPDS with $(m-1)$ stacks, for which, by induction over the number
of stacks, reachability (and emptiness) is decidable. Note, the initial
transition of the construction sets up the initial stacks of
$\mathcal{C}^{L}$.

######  Definition 5.4 ($\mathcal{C}_{\emptyset}$)

Given the non-emptiness problem
${\mathcal{L}^{{b},{i}}_{{p_{1}},{a},{p_{2}}}}\mathord{\left({\mathcal{C}^{L}}\right)}\cap{\mathcal{L}}\mathord{\left({\mathcal{T}^{A_{i}}_{{t},{t^{\prime}}}}\right)}\neq\emptyset$,
where ${top_{1}}\mathord{\left({t}\right)}=a$,
$\mathcal{C}^{L}=\left({\mathcal{P}\times\Sigma,\Sigma,\mathcal{R}_{1},\ldots,\mathcal{R}_{m-1}}\right)$
and
$\mathcal{T}^{A_{i}}_{{t},{t^{\prime}}}=\left({T_{A_{i}},\mathcal{R}_{\mathcal{G}_{n}},\delta,t,t^{\prime}}\right)$,
we define an $n$-OCPDS
$\mathcal{C}_{\emptyset}=\left({\mathcal{P}^{\emptyset},\Sigma,\mathcal{R}^{\emptyset}_{1},\ldots,\mathcal{R}^{\emptyset}_{i}\cup\mathcal{R}_{I/O},\ldots,\mathcal{R}^{\emptyset}_{m-1}}\right)$
where, for all $1\leq i\leq(m-1)$,

$\displaystyle\mathcal{P}^{\emptyset}$
$\displaystyle=\left\\{{p_{1},p_{2}}\right\\}\uplus\left\\{{\left({p,t_{1}}\right)}\
\left|\ {t_{1}\in
T_{A_{i}}\land{control}\mathord{\left({t_{1}}\right)}=p}\right.\right\\}\ ,$
$\displaystyle\mathcal{R}_{I/O}$
$\displaystyle=\left\\{{\left({{p_{1}},{\perp},{push^{n}_{b}},{\left({p_{1},t}\right)}}\right)}\right\\}\cup\left\\{{\left({{\left({p_{2},t}\right)},{\perp},{noop},{p_{2}}}\right)}\
\left|\ {t\in T_{A_{i}}}\right.\right\\}\ ,\text{ and}$
$\displaystyle\mathcal{R}^{\emptyset}_{i}$
$\displaystyle=\left\\{{\left({{\left({p,t_{1}}\right)},{c},{o},{\left({p^{\prime},t_{2}}\right)}}\right)}\
\left|\
{\left({{\left({p,{top_{1}}\mathord{\left({t_{1}}\right)}}\right)},{c},{r},{o},{\left({p^{\prime},{top_{1}}\mathord{\left({t_{2}}\right)}}\right)}}\right)\in\mathcal{R}_{i}\land\left({t_{1},r,t_{2}}\right)\in\Delta}\right.\right\\}$

######  Lemma 5.2 (Language Emptiness for OCPDS)

We have
${\mathcal{L}^{{b},{i}}_{{p_{1}},{a},{p_{2}}}}\mathord{\left({\mathcal{C}^{L}}\right)}\cap{\mathcal{L}}\mathord{\left({\mathcal{T}^{A_{i}}_{{t},{t^{\prime}}}}\right)}\neq\emptyset$
iff, in $\mathcal{C}_{\emptyset}$ from Definition 5.4, we have that
$\langle{p_{2}},{\perp_{n},\ldots\perp_{n}}\rangle$ is reachable from
$\langle{p_{1}},{\perp_{n},\ldots,\perp_{n}}\rangle$.

#### Global Reachability

We sketch a solution to the global reachability problem, giving a full proof
in Appendix E. From Lemma 5.1 ($\mathcal{C}^{R}$ simulates $\mathcal{C}$) we
gain a representation
$A_{m}={Pre^{*}_{\mathcal{C}^{R}}}\mathord{\left({A}\right)}$ of the set of
configurations $\langle{p},{\perp_{n},\ldots,\perp_{n},w_{m}}\rangle$ that
have a run to $\langle{{p_{\text{out}}}},{\perp_{n},\ldots,\perp_{n}}\rangle$.
Now take any $\langle{p},{\perp_{n},\ldots,\perp_{n},w_{m-1},w_{m}}\rangle$
that reaches $\langle{{p_{\text{out}}}},{\perp_{n},\ldots,\perp_{n}}\rangle$.
The run must pass some
$\langle{p^{\prime}},{\perp_{n},\ldots,\perp_{n},w^{\prime}_{m}}\rangle$ with
$\langle{p^{\prime}},{w^{\prime}_{m}}\rangle$ accepted by $A_{m}$. From the
product construction above, one can (though not immediately) extract a tuple
$\left({p,A_{m-1},A^{\prime}_{m}}\right)$ such that $w_{m-1}$ is accepted by
$A_{m-1}$ and $w_{m}$ is accepted by $A^{\prime}_{m}$. We repeat this
reasoning down to stack $1$ and obtain a tuple of the form
$\left({p,A_{1},\ldots,A_{m}}\right)$. We can only obtain a finite set of
tuples in this manner, giving a solution to the global reachability problem.

##  6 Scope-Bounded CPDS

Recently, scope-bounded multi-pushdown systems were introduced [30] and their
reachability problem was shown to be decidable. Furthermore, reachability for
scope- and phase-bounding was shown to be incomparable [30]. Here we consider
scope-bounded CPDS.

A run $\sigma=\sigma_{1}\ldots\sigma_{\ell}$ of an MCPDS is _context-
partitionable_ when, for each $\sigma_{i}$, if a transition in $\sigma_{i}$ is
via $r\in\mathcal{R}_{j}$ on stack $j$, then all transitions of $\sigma_{i}$
are via rules in $\mathcal{R}_{j}$ on stack $j$. A _round_ is a context-
partitioned run $\sigma_{1}\ldots\sigma_{m}$, where during $\sigma_{i}$ only
$\mathcal{R}_{i}$ is used. A _round-partitionable_ run can be partitioned
$\sigma_{1}\ldots\sigma_{\ell}$ where each $\sigma_{i}$ is a round. A run of
an SBCPDS is such that any character or stack removed from a stack must have
been created at most $\zeta$ rounds earlier. For this, we define pop- and
collapse-rounds for stacks. That is, we mark each stack and character with the
round in which it was created. When we copy a stack via $copy_{k}$, the pop-
round of the new copy of the stack is the current round. However, all stacks
and characters within the copy of $u$ keep the same pop- and collapse-round as
in the original $u$.

E.g. take $[{u}]_{2}$ where $u=[{ab}]_{1}$, $u$ and $a$ have pop-round $2$,
and $b$ has pop-round $1$. Suppose in round $3$ we use $copy_{2}$ to obtain
$[{uu}]_{2}$. The new copy of $u$ has pop-round $3$ (the current round), but
the $a$ and $b$ appearing in the copy of $u$ still have pop-rounds $2$ and $1$
respectively. If the scope-bound is $2$, the latest each $a$ and the original
$u$ could be popped is in round $4$, but the new $u$ may be popped in round
$5$.

We will write ${{}_{\mathfrak{p}}\mathord{w}}$ for a stack $w$ with pop-round
$\mathfrak{p}$ and ${{}_{\mathfrak{p},\mathfrak{c}}\mathord{a}}$ for a
character with pop-round $\mathfrak{p}$ and collapse-round $\mathfrak{c}$.
Pop- and collapse-rounds will be sometimes omitted for clarity. Note, the
outermost stack will always have pop-round $0$. In particular, for all
${u}:_{k}{v}$ in the definition below, the pop-round of $v$ is 0.

######  Definition 6.1 (Pop- and Collapse-Round)

Given a round-partitioned run $\sigma_{1}\ldots\sigma_{\ell}$ we define
inductively the pop- and collapse-rounds. The pop- and collapse-round of each
stack and character in the first configuration of $\sigma_{1}$ is $0$. Take a
transition
$\langle{p},{w}\rangle\longrightarrow\langle{p^{\prime}},{w^{\prime}}\rangle$
with $\langle{p^{\prime}},{w^{\prime}}\rangle$ in $\sigma_{z}$ via a rule
$\left({{p},{a},{o},{p^{\prime}}}\right)$. If $o=noop$ then $w=w^{\prime}$,
otherwise when

  1. 1.

$o=copy_{k}$ and $w={{{}_{\mathfrak{p}}\mathord{u}}}:_{k}{v}$, then
$w^{\prime}={{{}_{z}\mathord{u}}}:_{k}{({{{}_{\mathfrak{p}}\mathord{u}}}:_{k}{v})}$
where
${{}_{z}\mathord{u}}={{}_{z}\mathord{[{{{}_{\mathfrak{p}_{1}}\mathord{u_{1}}}\ldots{{}_{\mathfrak{p}_{\ell}}\mathord{u_{\ell}}}}]_{k-1}}}$
when
${{}_{\mathfrak{p}}\mathord{u}}={{}_{\mathfrak{p}}\mathord{[{{{}_{\mathfrak{p}_{1}}\mathord{u_{1}}}\ldots{{}_{\mathfrak{p}_{\ell}}\mathord{u_{\ell}}}}]_{k-1}}}$.

  2. 2.

$o=push^{k}_{b}$, then
$w^{\prime}={{{}_{z,\mathfrak{c}}\mathord{{b}^{\left({{}_{\mathfrak{p}^{\prime}}\mathord{u}}\right)}}}}:_{1}{w}$
where
${{}_{\mathfrak{p}^{\prime}}\mathord{u}}={top_{k+1}}\mathord{\left({{pop_{k}}\mathord{\left({w}\right)}}\right)}$
and $\mathfrak{c}$ is the pop-round of ${top_{k}}\mathord{\left({w}\right)}$.
(Note, when $k=n$, we know $\mathfrak{p}^{\prime}=0$ since the $top_{n+1}$
stack is outermost.)

  3. 3.

$o=pop_{k}$, when $w={u}:_{k}{v}$ then $w^{\prime}=v$.

  4. 4.

We set
${collapse_{k}}\mathord{\left({{{a}^{\left({{}_{\mathfrak{p}}\mathord{u^{\prime}}}\right)}}:_{1}{{u}:_{(k+1)}{v}}}\right)}={{{}_{\mathfrak{p}}\mathord{u^{\prime}}}}:_{(k+1)}{v}$
when $u$ is order-$k$ and $1\leq k<n$; and
${collapse_{n}}\mathord{\left({{{a}^{\left({{}_{0}\mathord{u}}\right)}}:_{1}{v}}\right)}={{}_{0}\mathord{u}}$
when $u$ is order-$n$.

  5. 5.

$o=rew_{b}$ and
$w={{{}_{\mathfrak{p},\mathfrak{c}}\mathord{{a}^{\left({{}_{\mathfrak{p}^{\prime}}\mathord{u}}\right)}}}}:_{1}{v}$,
then
$w^{\prime}={{{}_{\mathfrak{p},\mathfrak{c}}\mathord{{b}^{\left({{}_{\mathfrak{p}^{\prime}}\mathord{u}}\right)}}}}:_{1}{v}$.

######  Definition 6.2 (Scope-Bounded CPDS)

A $\zeta$-scope-bounded $n$-CPDS ($n$-SBCPDS) $\mathcal{C}$ is an order-$n$
MCPDS whose runs are all runs of $\mathcal{C}$ that are round-partitionable,
that is $\sigma_{1}\ldots\sigma_{\ell}$, such that for all $z$, if a
transition in $\sigma_{z}$ from $\langle{p},{w}\rangle$ to
$\langle{p^{\prime}},{w^{\prime}}\rangle$ is

  1. 1.

a $pop_{k}$ transition with $1<k\leq n$ and
$w={{{}_{\mathfrak{p}}\mathord{u}}}:_{k}{v}$, then $z-\zeta\leq\mathfrak{p}$,

  2. 2.

a $pop_{1}$ transition with
$w={{{}_{\mathfrak{p},\mathfrak{c}}\mathord{{a}^{u}}}}:_{1}{v}$, then
$z-\zeta\leq\mathfrak{p}$, or

  3. 3.

a $collapse_{k}$ transition with
$w={{{}_{\mathfrak{p},\mathfrak{c}}\mathord{{a}^{u}}}}:_{1}{v}$, then
$z-\zeta\leq\mathfrak{c}$.

La Torre and Napoli’s decidability proof for the order-$1$ case already uses
the saturation method [30]. However, while La Torre and Napoli use a forwards-
reachability analysis, we must use a backwards analysis. This is because the
forwards-reachable set of configurations is in general not regular. We thus
perform a backwards analysis for CPDS, resulting in a similar approach.
However, the proofs of correctness of the algorithm are quite different.

######  Theorem 6.1 (Decidability of Reachability Problems)

For $n$-OCPDSs the control state reachability problem and the global control
state reachability problem are decidable.

In Appendix E we show our non-global algorithm requires
${\mathcal{O}}\mathord{\left({2\uparrow_{n-1}\left({\ell}\right)}\right)}$
space, where $\ell$ is polynomial in $\zeta$ and the size of the SBCPDS, and
we have at most
${\mathcal{O}}\mathord{\left({2\uparrow_{n}\left({\ell}\right)}\right)}$
tuples in the global reachability solution. La Torre and Parlato give an
alternative control state reachability algorithm at order-$1$ using _thread
interfaces_ , which allows sequentialisation [19] and should generalise
order-$n$, but, does not solve the global reachability problem.

#### Control State Reachability

Fix initial and target control states ${p_{\text{in}}}$ and
${p_{\text{out}}}$. The algorithm first builds a _reachability graph_ , which
is a finite graph with a certain kind of path iff ${p_{\text{out}}}$ can be
reached from ${p_{\text{in}}}$. To build the graph, we define layered stack
automata. These have states $q_{p}^{i}$ for each $1\leq i\leq\zeta$ which
represent the stack contents $i$ rounds later. Thus, a layer automaton tracks
the stack across $\zeta$ rounds, which allows analysis of scope-bounded CPDSs.

######  Definition 6.3 ($\zeta$-Layered Stack Automata)

A _$\zeta$ -layered stack automaton_ is a stack automaton $A$ such that
$\mathbb{Q}_{n}=\left\\{{q_{p}^{i}}\ \left|\ {p\in\mathcal{P}\land 1\leq
i\leq\zeta}\right.\right\\}$.

A state $q_{p}^{i}$ is of layer $i$. A state $q^{\prime}$ labelling
$q\xrightarrow{q^{\prime}}Q$ has the same layer as $q$. We require that there
is no $q\xrightarrow{q^{\prime}}Q$ with $q^{\prime\prime}\in Q$ where $q$ is
of layer $i$ and $q^{\prime\prime}$ is of layer $j<i$. Similarly, there is no
$q\xrightarrow[Q_{col}]{a}Q$ with $q^{\prime}\in Q\cup Q_{col}$ where $q$ is
of layer $i$ and $q^{\prime}$ is of layer $j<i$.

Next, we define several operations from which the reachability graph is
constructed. The $\text{\tt Predecessor}_{j}$ operation connects stack $j$
between two rounds. We define for stack $j$

${\text{\tt
Predecessor}_{j}}\mathord{\left({A,q_{p},q_{p^{\prime}}}\right)}={\text{\tt
Saturate}_{j}}\mathord{\left({{\text{\tt EnvMove}}\mathord{\left({{\text{\tt
Shift}}\mathord{\left({A}\right)},q_{p_{1}}^{1},q_{p_{2}}^{2}}\right)}}\right)}$

where definitions of Shift, EnvMove and $\text{\tt Saturate}_{j}$ are given in
Appendix G. Shift moves transitions in layer $i$ to layer $(i+1)$. E.g.
$q_{p}^{1}\xrightarrow{q}\left\\{{q_{p^{\prime}}^{2}}\right\\}$ would become
$q_{p}^{2}\xrightarrow{q}\left\\{{q_{p^{\prime}}^{3}}\right\\}$. Moreover,
transitions involving states in layer $\zeta$ are removed. This is because the
stack elements in layer $\zeta$ will “go out of scope”. EnvMove adds a new
transition (analogously to a $\left({{p_{1}},{a},{rew_{a}},{p_{2}}}\right)$
rule) corresponding to the control state change from $p_{1}$ to $p_{2}$
effected by the runs over the other stacks between the current round and the
next (hence layers $1$ and $2$ in the definition above). $\text{\tt
Saturate}_{j}$ gets by saturation all configurations of stack $j$ that can
reach via $\mathcal{R}_{j}$ the stacks accepted from the layer-$1$ states of
its argument (i.e. saturation using initial states $\left\\{{q_{p}^{1}}\
\left|\ {p\in\mathcal{P}}\right.\right\\}$, which accept stacks from the next
round).

The current layer automaton represents a stack across up to $\zeta$ rounds.
The predecessor operation adds another round on to the front of this
representation. A key new insight in our proofs is that if a transition goes
to a layer $i$ state, then it represents part of a run where the stack read by
the transition is removed in $i$ rounds time. Thus, if we add a transition at
layer $0$ (were it to exist) that depends on a transition of layer $\zeta$,
then the push or copy operation would have a corresponding pop $(\zeta+1)$
scopes away. Scope-bounding forbids this.

#### The Reachability Graph

The reachability graph
$\mathcal{G}^{{p_{\text{out}}}}_{\mathcal{C}}=\left({\mathcal{V},\mathcal{E}}\right)$
has vertices $\mathcal{V}$ and edges $\mathcal{E}$. Firstly, $\mathcal{V}$
contains some _initial_ vertices
$\left({p_{0},A_{1},p_{1},\ldots,p_{m-1},A_{m},p_{m}}\right)$ where
$p_{m}={p_{\text{out}}}$, and for all $1\leq i\leq m$ we have that $A_{i}$ is
the layer automaton ${\text{\tt Saturate}_{i}}\mathord{\left({A}\right)}$
where for all $w$, $A$ accepts $\langle{p_{i}},{w}\rangle$ from
$q_{p_{i}}^{1}$. Furthermore, we require that there is some $w$ such that
$\langle{p_{i-1}},{w}\rangle$ is accepted by $A_{i}$ from $q_{p_{i}}^{1}$.
That is, there is a run from $\langle{p_{i-1}},{w}\rangle$ to $p_{i}$.
Intuitively, initial vertices model the final round of a run to
${p_{\text{out}}}$ with context switches at $p_{0},\ldots,p_{m}$.

The complete set $\mathcal{V}$ is the set of all tuples
$\left({p_{0},A_{1},p_{1},\ldots,p_{m-1},A_{m},p_{m}}\right)$ where there is
some $w$ such that $\langle{p_{i-1}},{w}\rangle$ is accepted by $A_{i}$ from
state $q_{p_{i-1}}^{1}$. To ensure finiteness, we can bound $A_{i}$ to at most
$N$ states. The value of $N$ is
${\mathcal{O}}\mathord{\left({2\uparrow_{n-1}\left({\ell}\right)}\right)}$
where $\ell$ is polynomial in $\zeta$ and the size of $\mathcal{C}$. We give a
full definition of $N$ and proof in Appendix G.

We have an edge from a vertex $\left({p_{0},A_{1},\ldots,A_{m},p_{m}}\right)$
to
$\left({p^{\prime}_{0},A^{\prime}_{1},\ldots,A^{\prime}_{m},p^{\prime}_{m}}\right)$
whenever $p_{m}=p^{\prime}_{0}$ and for all $i$ we have $A_{i}={\text{\tt
Predecessor}_{i}}\mathord{\left({A^{\prime}_{i},q_{p_{i}},q_{p^{\prime}_{i-1}}}\right)}$.
An edge means the two rounds can be concatenated into a run since the control
states and stack contents match up.

######  Lemma 6.1 (Simulation by
$\mathcal{G}^{{p_{\text{out}}}}_{\mathcal{C}}$)

Given a scope-bounded CPDS $\mathcal{C}$ and control states
${p_{\text{in}}},{p_{\text{out}}}$, there is a run of $\mathcal{C}$ from
$\langle{{p_{\text{in}}}},{w_{1},\ldots,w_{m}}\rangle$ to
$\langle{{p_{\text{out}}}},{w^{\prime}_{1},\ldots,w^{\prime}_{m}}\rangle$ for
some $w^{\prime}_{1},\ldots,w^{\prime}_{m}$ iff there is a path in
$\mathcal{G}^{{p_{\text{out}}}}_{\mathcal{C}}$ to a vertex
$\left({p_{0},A_{1},\ldots,A_{m},p_{m}}\right)$ with $p_{0}={p_{\text{in}}}$
from an initial vertex where for all $i$ we have
$\langle{p_{i-1}},{w_{i}}\rangle$ accepted from $q_{p_{i}}^{1}$ of $A_{i}$.

#### Global Reachability

The $\left({p_{0},A_{1},p_{1},\ldots,p_{m-1},A_{m},p_{m}}\right)$ in
$\mathcal{G}^{{p_{\text{out}}}}_{\mathcal{C}}$ reachable from an initial
vertex are finite in number. We know by Lemma 6.1 that there is such a vertex
accepting all $\langle{p_{i-1}},{w_{i}}\rangle$ iff
$\langle{p_{0}},{w_{1},\ldots,w_{m}}\rangle$ can reach the target control
state. Let $\chi$ be the set of tuples
$\left({p_{0},A_{1},\ldots,A_{m}}\right)$ for each reachable vertex as above,
where $A_{i}$ is restricted to the initial state $q_{p_{i-1}}^{1}$. This is a
regular solution to the global control state reachability problem.

##  7 Conclusion

We have shown decidability of global reachability for ordered and scope-
bounded collapsible pushdown systems (and phase-bounded in the appendix). This
leads to a challenge to find a general framework capturing these systems.
Furthermore, we have only shown upper-bound results. Although, in the case of
phase-bounded systems, our upper-bound matches that of Seth for CPDSs without
collapse [27], we do not know if it is optimal. Obtaining matching lower-
bounds is thus an interesting though non-obvious problem. Recently, a more
relaxed notion of scope-bounding has been studied [18]. It would be
interesting to see if we can extend our results to this notion. We are also
interested in developing and implementing algorithms that may perform well in
practice.

#### Acknowledgments

Many thanks for initial discussions with Arnaud Carayol and to the referees
for their helpful remarks. This work was supported by Fond. Sci. Math. Paris;
AMIS [ANR 2010 JCJC 0203 01 AMIS]; FREC [ANR 2010 BLAN 0202 02 FREC]; VAPF
(Région IdF); and the Engineering and Physical Sciences Research Council
[EP/K009907/1].

## References

  * [1] M. F. Atig.  Model-checking of ordered multi-pushdown automata.  Logical Methods in Computer Science, 8(3), 2012.
  * [2] M. F. Atig, B. Bollig, and P. Habermehl.  Emptiness of multi-pushdown automata is 2etime-complete.  In Developments in Language Theory, pages 121–133, 2008.
  * [3] T. Ball and S. K. Rajamani.  The SLAM project: Debugging system software via static analysis.  In POPL, pages 1–3, Portland, Oregon, Jan. 16–18, 2002.
  * [4] A. Bouajjani, J. Esparza, and O. Maler.  Reachability analysis of pushdown automata: Application to model-checking.  In CONCUR, pages 135–150, 1997.
  * [5] A. Bouajjani, J. Esparza, and T. Touili.  A generic approach to the static analysis of concurrent programs with procedures.  SIGPLAN Not., 38(1):62–73, 2003.
  * [6] A. Bouajjani, M. Müller-Olm, and T. Touili.  Regular symbolic analysis of dynamic networks of pushdown systems.  CONCUR 2005 - Concurrency Theory, pages 473–487, 2005.
  * [7] L. Breveglieri, A. Cherubini, C. Citrini, and S. Crespi-Reghizzi.  Multi-push-down languages and grammars.  Int. J. Found. Comput. Sci., 7(3):253–292, 1996.
  * [8] C. H. Broadbent, A. Carayol, M. Hague, and O. Serre.  A saturation method for collapsible pushdown systems.  In ICALP, pages 165–176, 2012.
  * [9] C. H. Broadbent, A. Carayol, M. Hague, and O. Serre.  C-shore: a collapsible approach to higher-order verification.  In ICFP, pages 13–24, 2013.
  * [10] A. Cyriac, P. Gastin, and K. N. Kumar.  MSO decidability of multi-pushdown systems via split-width.  In CONCUR, pages 547–561, 2012.
  * [11] W. Damm.  The io- and oi-hierarchies.  Theor. Comput. Sci., 20:95–207, 1982.
  * [12] A. Finkel, B. Willems, and P. Wolper.  A direct symbolic approach to model checking pushdown systems.  In INFINITY, volume 9, pages 27–37, 1997.
  * [13] M. Hague, A. S. Murawski, C.-H. L. Ong, and O. Serre.  Collapsible pushdown automata and recursion schemes.  In LICS, pages 452–461, 2008.
  * [14] A. Heußner, J. Leroux, A. Muscholl, and G. Sutre.  Reachability analysis of communicating pushdown systems.  In Proc. 13th Int. Conf. Foundations of Software Science and Computation Structures (FOSSACS’10), Paphos, Cyprus, Mar. 2010, volume 6014 of Lecture Notes in Computer Science, pages 267–281. Springer, 2010.
  * [15] V. Kahlon.  Reasoning about threads with bounded lock chains.  In CONCUR, pages 450–465, 2011.
  * [16] T. Knapik, D. Niwinski, P. Urzyczyn, and I. Walukiewicz.  Unsafe grammars and panic automata.  In ICALP, pages 1450–1461, 2005.
  * [17] N. Kobayashi and A. Igarashi.  Model-checking higher-order programs with recursive types.  In ESOP, pages 431–450, 2013.
  * [18] S. La Torre and M. Napoli.  A temporal logic for multi-threaded programs.  In IFIP TCS, pages 225–239, 2012.
  * [19] S. La Torre and G. Parlato.  Scope-bounded multistack pushdown systems: Fixed-point, sequentialization, and tree-width.  In FSTTCS, pages 173–184, 2012.
  * [20] P. Madhusudan and G. Parlato.  The tree width of auxiliary storage.  In POPL, pages 283–294, 2011.
  * [21] C.-H. L. Ong.  On model-checking trees generated by higher-order recursion schemes.  In LICS, pages 81–90, 2006.
  * [22] L. Ong.  Recursion schemes, collapsible pushdown automata and higher-order model checking.  In LATA, pages 13–41, 2013.
  * [23] S. Qadeer.  The case for context-bounded verification of concurrent programs.  In Proceedings of the 15th international workshop on Model Checking Software, SPIN ’08, pages 3–6, Berlin, Heidelberg, 2008. Springer-Verlag.
  * [24] S. Qadeer and J. Rehof.  Context-bounded model checking of concurrent software.  In TACAS, pages 93–107, 2005.
  * [25] S. Schwoon.  Model-checking Pushdown Systems.  PhD thesis, Technical University of Munich, 2002.
  * [26] K. Sen and M. Viswanathan.  Model checking multithreaded programs with asynchronous atomic methods.  In CAV, pages 300–314, 2006.
  * [27] A. Seth.  Games on higher order multi-stack pushdown systems.  In RP, pages 203–216, 2009.
  * [28] A. Seth.  Global reachability in bounded phase multi-stack pushdown systems.  In CAV, pages 615–628, 2010.
  * [29] S. L. Torre, P. Madhusudan, and G. Parlato.  A robust class of context-sensitive languages.  In LICS, pages 161–170, 2007.
  * [30] S. L. Torre and M. Napoli.  Reachability of multistack pushdown systems with scope-bounded matching relations.  In CONCUR, pages 203–218, 2011.

##  Appendix A Undecidability of MSO Over The Naive Encoding of Order-$2$
Stacks

We show that the naive graph representation of an order-$2$ stack leads to the
undecidability of MSO. By naive graph representation we mean a graph where
each node is a configuration on a run of the CPDS, and we have an edge
labelled $S$ between $c_{1}$ and $c_{2}$ if the configurations are
neighbouring on the run. We have an further edge labelled $1$ if $c_{2}$ was
obtained by popping a character via $pop_{1}$ that was first pushed on to the
stack by a $push^{k}_{a}$ at node $c_{1}$. More formally, we define the
_originating configuration_ for each character.

######  Definition A.1 (Originating Configuration)

Given a run as a sequence of configurations $c_{1},c_{2},\ldots$ we define
inductively the originating configuration of each character. The originating
configuration of each character in $c_{1}$ is $1$. Take a transition
$c_{i}\longrightarrow c_{i+1}$ via a rule
$\left({{p},{a},{o},{p^{\prime}}}\right)$. If

  1. 1.

$o=copy_{k}$, then each character copied inherits its originating
configuration from the character it is a copy of. All other characters keep
the same originating configuration.

  2. 2.

$o=push^{k}_{b}$, all characters maintain the same originating configuration
except the new $b$ character that has originating configuration $i$.

  3. 3.

$o=rew_{b}$, all characters maintain the same originating configuration except
the new $b$ character that has the originating configuration of the $a$
character it is replacing.

  4. 4.

$o=noop,pop_{k}$ or $collapse_{k}$, all originating configurations are
inherited from the previous stack.

Thus, from a run $c_{1},c_{2},\ldots$ we define a graph
$\left({\mathcal{V},\mathcal{E}_{1},\mathcal{E}_{2}}\right)$ with vertices
$\mathcal{V}=\left\\{{c_{1},c_{2},\ldots}\right\\}$ and edge sets
$\mathcal{E}_{1}$ and $\mathcal{E}_{2}$, where
$\mathcal{E}_{1}=\left\\{{\left({c_{i},c_{i+1}}\right)}\ \left|\ {1\leq
i}\right.\right\\}$ and $\mathcal{E}_{2}$ contains all pairs
$\left({c_{i},c_{j}}\right)$ where $c_{j}$ was obtained by a $pop_{1}$ from
$c_{j-1}$ and the originating configuration of the character removed is $i$.

Now, consider the CPDS generating the following run

$\begin{array}[]{l}\langle{p_{0}},{[{[{\perp}]_{1}}]_{2}}\rangle\longrightarrow\langle{p_{1}},{[{[{a\perp}]_{1}}]_{2}}\rangle\longrightarrow\langle{p_{2}},{[{[{a\perp}]_{1}[{a\perp}]_{1}}]_{2}}\rangle\longrightarrow\langle{p_{2}},{[{[{\perp}]_{1}[{a\perp}]_{1}}]_{2}}\rangle\longrightarrow\\\
\\\
\langle{p_{0}},{[{[{a\perp}]_{1}}]_{2}}\rangle\longrightarrow\langle{p_{1}},{[{[{aa\perp}]_{1}}]_{2}}\rangle\longrightarrow\langle{p_{2}},{[{[{aa\perp}]_{1}[{aa\perp}]_{1}}]_{2}}\rangle\longrightarrow\langle{p_{2}},{[{[{a\perp}]_{1}[{aa\perp}]_{1}}]_{2}}\rangle\longrightarrow\\\
\langle{p_{2}},{[{[{\perp}]_{1}[{aa\perp}]_{1}}]_{2}}\rangle\longrightarrow\\\
\\\
\langle{p_{0}},{[{[{aa\perp}]_{1}}]_{2}}\rangle\longrightarrow\langle{p_{1}},{[{[{aaa\perp}]_{1}}]_{2}}\rangle\longrightarrow\langle{p_{2}},{[{[{aaa\perp}]_{1}[{aaa\perp}]_{1}}]_{2}}\rangle\longrightarrow\langle{p_{2}},{[{[{aa\perp}]_{1}[{aaa\perp}]_{1}}]_{2}}\rangle\\\
\longrightarrow\langle{p_{2}},{[{[{a\perp}]_{1}[{aaa\perp}]_{1}}]_{2}}\rangle\longrightarrow\langle{p_{2}},{[{[{\perp}]_{1}[{aaa\perp}]_{1}}]_{2}}\rangle\longrightarrow\\\
\\\ \langle{p_{0}},{[{[{aaa\perp}]_{1}}]_{2}}\rangle\longrightarrow\cdots\
.\end{array}$

That is, beginning at $\langle{p_{0}},{\perp_{2}}\rangle$ the CPDS pushes an
$a$ character, copies the stack with a $copy_{2}$ and removes all $a$s. After
all $a$s are removed, it performs $pop_{2}$ the obtain the stack below
containing only $a$. It pushes another $a$ onto the stack and repeats this
process. After each $pop_{2}$ it adds one more $a$ character, performs a
$copy_{2}$, pops all $a$s and so on. This produces the graph shown below with
$\mathcal{E}_{1}$ represented with solid lines, and $\mathcal{E}_{2}$ with
dashed lines. Furthermore, nodes from which an $a$ is pushed are the target of
a dashed arrow, and nodes reached by popping an $a$ are the sources of dashed
arrows.

[nodealign=true,rowsep=15ex]

$c_{1}$ $c_{2}$ $c_{3}$ $c_{4}$ $c_{5}$ $c_{6}$ $c_{7}$ $c_{8}$ $c_{9}$
$c_{10}$ $c_{11}$ $c_{12}$ $c_{13}$ $c_{14}$ $c_{15}$ $\cdots$

In this graph we can interpret the infinite half-grid. We restrict the graph
to nodes that are the source of a dashed arrow. We define horizontal and
vertical edges to obtain the grid below.

[nodealign=true,rowsep=5ex,colsep=5ex]

& $\vdots$

$c_{13}$ $\cdots$

$c_{8}$ $c_{14}$ $\cdots$

$c_{4}$ $c_{9}$ $c_{15}$ $\cdots$

There is a vertical edge from $c$ to $c^{\prime}$ whenever
$\left({c^{\prime},c}\right)\in\mathcal{E}_{1}$. There is a horizontal edge
from $c$ to $c^{\prime}$ whenever we have $c^{\prime\prime}$ such that

  1. 1.

$\left({c^{\prime\prime},c}\right)\in\mathcal{E}_{2}$ and
$\left({c^{\prime\prime},c^{\prime}}\right)\in\mathcal{E}_{2}$, and

  2. 2.

there is a path in $\mathcal{E}_{1}$ from $c$ to $c^{\prime}$, and

  3. 3.

there is no $c^{\prime\prime\prime}$ on the above path with
$\left({c^{\prime\prime},c^{\prime\prime\prime}}\right)\in\mathcal{E}_{2}$.

Thus, we can MSO-interpret the infinite half-grid, and hence MSO is
undecidable over this graph.

This naive encoding contains basic matching information about pushes and pops.
It remains an interesting open problem to obtain an encoding of CPDS that is
amenable to MSO based frameworks that give positive decidability results for
concurrent behaviours.

##  Appendix B Definition of The Saturation Function

We first introduce two more short-hand notation for sets of transitions.

The first is a variant on the long-form transitions. E.g. for the run in
Section 2 we can write
${q_{3}}\xrightarrow{q_{1}}\left({{Q_{2},Q_{3}}}\right)$ to represent the use
of $q_{3}\xrightarrow{q_{2}}Q_{3}$ and $q_{2}\xrightarrow{q_{1}}Q_{2}$ as the
first two transitions in the run. That is, for a sequence
$q\xrightarrow{q_{k-1}}Q_{k},q_{k-1}\xrightarrow{q_{k-2}}Q_{k-1},\ldots,q_{k^{\prime}}\xrightarrow{q_{k^{\prime}-1}}Q_{k^{\prime}}$
in $\Delta_{k}$ to $\Delta_{k^{\prime}}$ respectively, we write
${q}\xrightarrow{q_{k^{\prime}-1}}\left({{Q_{k^{\prime}},\ldots,Q_{k}}}\right)$.

The second notation represents sets of long-form transitions. We write
${Q}\xrightarrow[Q_{col}]{a}\left({{Q_{1},\ldots,Q_{k}}}\right)$ if there is a
set $\left\\{{t_{1},\ldots,t_{\ell}}\right\\}$ of long-form transitions such
that $Q=\left\\{{q_{1},\ldots,q_{\ell}}\right\\}$ and for all $1\leq
i\leq\ell$ we have
$t_{i}={q_{i}}\xrightarrow[Q^{i}_{col}]{a}\left({{Q^{i}_{1},\ldots,Q^{i}_{k}}}\right)$
and $Q_{col}=\bigcup_{1\leq
i\leq\ell}Q^{i}_{col}\subseteq\mathbb{Q}_{k^{\prime}}$ for some $k^{\prime}$,
and for all $k^{\prime}$, $Q_{k^{\prime}}=\bigcup_{1\leq
i\leq\ell}Q^{i}_{k^{\prime}}$.

######  Definition B.1 (The Auxiliary Saturation Function $\Pi_{r}$)

For a consuming CPDS rule $r=\left({{p},{a},{o},{p^{\prime}}}\right)$ we
define for a given stack automaton $A$, the set
${\Pi_{r}}\mathord{\left({A}\right)}$ to be the smallest set such that, when

  1. 1.

$o=pop_{k}$, for each
${q_{p^{\prime}}}\xrightarrow{q_{k}}\left({{Q_{k+1},\dots,Q_{n}}}\right)$ in
$A$, the set ${\Pi_{r}}\mathord{\left({A}\right)}$ contains the transition
${q_{p}}\xrightarrow[\emptyset]{a}\left({{\emptyset,\ldots,\emptyset,\left\\{{q_{k}}\right\\},Q_{k+1},\ldots,Q_{n}}}\right)$,

  2. 2.

$o=collapse_{k}$, when $k=n$, the set ${\Pi_{r}}\mathord{\left({A}\right)}$
contains
${q_{p}}\xrightarrow[\left\\{{q_{p^{\prime}}}\right\\}]{a}\left({{\emptyset,\ldots,\emptyset}}\right)$,
and when $k<n$, for each transition
${q_{p^{\prime}}}\xrightarrow{q_{k}}\left({{Q_{k+1},\dots,Q_{n}}}\right)$ in
$A$, the set ${\Pi_{r}}\mathord{\left({A}\right)}$ contains the transition
${q_{p}}\xrightarrow[\left\\{{q_{k}}\right\\}]{a}\left({{\emptyset,\ldots,\emptyset,Q_{k+1},\ldots,Q_{n}}}\right)$,

For a generating CPDS rule $r=\left({{p},{a},{o},{p^{\prime}}}\right)$ we
define for a given stack automaton $A$ and long-form transition $t$ of $A$,
the set ${\Pi_{r}}\mathord{\left({t,A}\right)}$ to be the smallest set such
that, when

  1. 1.

$o=copy_{k}$,
$t={q_{p^{\prime}}}\xrightarrow[Q_{col}]{a}\left({{Q_{1},\ldots,Q_{k},\ldots,Q_{n}}}\right)$
and
${Q_{k}}\xrightarrow[Q^{\prime}_{col}]{a}\left({{Q^{\prime}_{1},\ldots,Q^{\prime}_{k}}}\right)$
is in $A$, the set ${\Pi_{r}}\mathord{\left({t,A}\right)}$ contains the
transition

${q_{p}}\xrightarrow[Q_{col}\cup Q^{\prime}_{col}]{a}\left({{Q_{1}\cup
Q^{\prime}_{1},\ldots,Q_{k-1}\cup
Q^{\prime}_{k-1},Q^{\prime}_{k},Q_{k+1},\ldots,Q_{n}}}\right)\ ,$

  2. 2.

$o=push^{k}_{b}$, for all transitions
$t={q_{p^{\prime}}}\xrightarrow[Q_{col}]{b}\left({{Q_{1},\ldots,Q_{n}}}\right)$
and $Q_{1}\xrightarrow[Q^{\prime}_{col}]{a}Q^{\prime}_{1}$ is in $A$ with
$Q_{col}\subseteq\mathbb{Q}_{k}$, the set
${\Pi_{r}}\mathord{\left({t,A}\right)}$ contains the transition

${q_{p}}\xrightarrow[Q^{\prime}_{col}]{a}\left({{Q^{\prime}_{1},Q_{2},\ldots,Q_{k-1},Q_{k}\cup
Q_{col},Q_{k+1},\ldots,Q_{n}}}\right)\ ,$

  3. 3.

$o=rew_{b}$ or $o=noop$,
$t={q_{p^{\prime}}}\xrightarrow[Q_{col}]{b}\left({{Q_{1},\dots,Q_{n}}}\right)$
the set ${\Pi_{r}}\mathord{\left({t,A}\right)}$ contains the transition
${q_{p}}\xrightarrow[Q_{col}]{a}\left({{Q_{1},\dots,Q_{n}}}\right)$ (where
$b=a$ if $o=noop$).

As a remark, omitted from the main body of the paper, during saturation, we
add transitions
${q_{n}}\xrightarrow[Q_{col}]{a}\left({{Q_{1},\ldots,Q_{n}}}\right)$ to the
automaton. Recall this represents a sequence of transitions
$q\xrightarrow{q_{k-1}}Q_{k}\in\Delta_{k},q_{k-1}\xrightarrow{q_{k-2}}Q_{k-1}\in\Delta_{k-1},\ldots,q_{1}\xrightarrow[Q_{col}]{a}Q_{1}\in\Delta_{1}$.
Hence, we first, for each $n\geq k>1$, add $q_{k}\xrightarrow{q_{k-1}}Q_{k}$
to $\Delta_{k}$ if it does not already exist. Then, we add
$q_{1}\xrightarrow[Q_{col}]{a}Q_{1}$ to $\Delta_{1}$. Note, in particular, we
only add _at most one_ $q^{\prime}$ with
$\left({q,q^{\prime},Q}\right)\in\Delta_{k}$ for all $q$ and $Q$. This ensures
termination.

Also, we say a state is _initial_ if it is of the form $q_{p}\in Q_{n}$ for
some control state $p$ or if it is a state $q_{k}\in Q_{k}$ for $k<n$ such
that there exists a transition $q_{k+1}\xrightarrow{q_{k}}Q_{k+1}$ in
$\Delta_{k+1}$. A pre-condition (that does not sacrifice generality) of the
saturation technique is that there are no incoming transitions to initial
states.

##  Appendix C Proofs for Extended CPDS

We provide the proof of Theorem 3.1 (Global Reachability of ECPDS). The proof
is via the two lemmas in the sections that follow. A large part of the proof
is identical to ICALP 2012 and hence not repeated here.

###  C.1 Completeness of Saturation for ECPDS

######  Lemma C.1 (Completeness of $\Pi$)

Given an extended CPDS $\mathcal{C}$ and an order-$n$ stack automaton $A_{0}$,
the automaton $A$ constructed by saturation with $\Pi$ is such that
$\langle{p},{w}\rangle\in{Pre^{*}_{\mathcal{C}}}\mathord{\left({A_{0}}\right)}$
implies $w\in{\mathcal{L}_{q_{p}}}\mathord{\left({A}\right)}$.

_Proof._ We begin with a definition of
${Pre^{*}_{\mathcal{C}}}\mathord{\left({A_{0}}\right)}$ that permits an
inductive proof of completeness. Thus, let
${Pre^{*}_{\mathcal{C}}}\mathord{\left({A_{0}}\right)}=\bigcup\limits_{\alpha<\omega}{Pre^{\alpha}_{\mathcal{C}}}\mathord{\left({A_{0}}\right)}$
where

$\begin{array}[]{rcl}{Pre^{0}_{\mathcal{C}}}\mathord{\left({A_{0}}\right)}&=&\left\\{{\langle{p},{w}\rangle}\
\left|\
{w\in{\mathcal{L}_{q_{p}}}\mathord{\left({A_{0}}\right)}}\right.\right\\}\\\
\\\
{Pre^{\alpha+1}_{\mathcal{C}}}\mathord{\left({A_{0}}\right)}&=&\left\\{{\langle{p},{w}\rangle}\
\left|\
{\exists\langle{p},{w}\rangle\longrightarrow\langle{p^{\prime}},{w^{\prime}}\rangle\in{Pre^{\alpha}_{\mathcal{C}}}\mathord{\left({A_{0}}\right)}}\right.\right\\}\end{array}$

The proof is by induction over $\alpha$. In the base case, we have
$w\in{\mathcal{L}_{q_{p}}}\mathord{\left({A_{0}}\right)}$ and the existence of
a run of $A_{0}$, and thus a run in $A$ comes directly from the run of
$A_{0}$. Now, inductively assume
$\langle{p},{w}\rangle\longrightarrow\langle{p^{\prime}},{w^{\prime}}\rangle$
and an accepting run of $w^{\prime}$ from $q_{p^{\prime}}$ of $A$.

There are two cases depending on the rule used in the transition above. Here
we consider the case where the rule is of the form
$\left({{p},{{top_{1}}\mathord{\left({w}\right)}},{{\mathcal{L}_{g}}},{p^{\prime}}}\right)$.
The case where the rule is a standard CPDS rule is identical to ICALP 2012 and
hence we do not repeat it here (although a variation of the proof appears in
the proof of Lemma G.2).

Take the rule
$\left({{p},{{top_{1}}\mathord{\left({w}\right)}},{{\mathcal{L}_{g}}},{p^{\prime}}}\right)$
and the sequence
$\left({{p_{0}},{a_{1}},{o_{1}},{p_{1}}}\right)\ldots,\left({{p_{\ell-1}},{a_{\ell}},{o_{\ell}},{p_{\ell}}}\right)\in{\mathcal{L}_{g}}$
that witnessed the transition, observing that $p_{0}=p$ and
$p_{\ell}=p^{\prime}$. Now, let
$w_{i}={o_{\ell}}\mathord{\left({\cdots{o_{i+1}}\mathord{\left({w^{\prime}}\right)}}\right)}$
for all $0\leq i\leq\ell$. Note, $w=w_{0}$ and $w^{\prime}=w_{\ell}$.

Take
$t^{\prime}={q_{p^{\prime}}}\xrightarrow[Q_{col}]{b}\left({{Q_{1},\ldots,Q_{n}}}\right)$
to be the first transition on the accepting run of
$\langle{p^{\prime}},{w^{\prime}}\rangle$. Beginning with
$t_{\ell}=t^{\prime}$, we are going to show that there is a run of
$\langle{p_{i}},{w_{i}}\rangle$ beginning with $t_{i}$ and thereafter only
using transitions appearing in $A$. Since, by the definition of $\Pi$, we add
$t_{0}=t$ to $A$, we will obtain an accepting run of $A$ for
$\langle{p_{0}},{w_{0}}\rangle=\langle{p},{w}\rangle$ as required. We will
induct from $\ell$ down to $0$.

The base case $i=\ell$ is trivial, since $t_{\ell}=t^{\prime}$ and we already
have an accepting run of $A$ over $\langle{p_{\ell}},{w_{\ell}}\rangle$
beginning with $t_{\ell}$. Now, assume the case for
$\langle{p_{i}},{w_{i}}\rangle$ and $t_{i}$. We show the case for $i-1$. Take
$\left({p_{i-1},a_{i},o_{i},p_{i}}\right)$, we do a case split on $o_{i}$. A
reader familiar with the saturation method for CPDS will observe that the
arguments below are very similar to the arguments for ordinary CPDS rules.

  1. 1.

When $o_{i}=copy_{k}$, let $w_{i-1}={u_{k-1}}:_{k}{{\cdots}:_{n}{u_{n}}}$. We
know

$w_{i}={u_{k-1}}:_{k}{{u_{k-1}}:_{k}{{u_{k}}:_{(k+1)}{{\cdots}:_{n}{u_{n}}}}}\
.$

Let
$t_{i}={q_{p_{i}}}\xrightarrow[Q_{col}]{a}\left({{Q_{1},\ldots,Q_{k},\ldots
Q_{n}}}\right)$ and
${Q_{k}}\xrightarrow[Q^{\prime}_{col}]{a}\left({{Q^{\prime}_{1},\ldots,Q^{\prime}_{k}}}\right)$
be the initial transitions used on the run of $w_{i}$ (where the transition
from $Q_{k}$ reads the second copy of $u_{k-1}$).

From the construction of $\mathcal{T}^{A}_{{t},{t^{\prime}}}$ we have have a
transition
$t_{i-1}\xrightarrow{\left({{p_{i-1}},{a_{i}},{o_{i}},{p_{i}}}\right)}t_{i}$
where

$t_{i-1}={q_{p_{i-1}}}\xrightarrow[Q_{col}\cup
Q^{\prime}_{col}]{a}\left({{Q_{1}\cup Q^{\prime}_{1},\ldots,Q_{k-1}\cup
Q^{\prime}_{k-1},Q^{\prime}_{k},Q_{k+1},\ldots,Q_{n}}}\right)\ .$

Since we know ${u_{k}}:_{(k+1)}{{\cdots}:_{n}{u_{n}}}$ is accepted from
$Q^{\prime}_{k}$ via $Q_{k+1},\ldots,Q_{n}$, and we know that $u_{k-1}$ is
accepted from $Q_{1},\ldots,Q_{k-1}$ and
$Q^{\prime}_{1},\ldots,Q^{\prime}_{k-1}$ via $a$-transitions labelling
annotations with $Q_{col}$ and $Q^{\prime}_{col}$ respectively, we obtain an
accepting run of $w_{i-1}$.

  2. 2.

When $o_{i}=push^{k}_{c}$, let
$w_{i-1}={u_{k-1}}:_{k}{{u_{k}}:_{k+1}{{\cdots}:_{n}{u_{n}}}}$. We know
$w_{i}={push^{k}_{c}}\mathord{\left({w_{i-1}}\right)}$ is

${{c}^{u_{k}}}:_{1}{{u_{k-1}}:_{k}{{\cdots}:_{n}{u_{n}}}}\ .$

Let
$t_{i}={q_{p_{i}}}\xrightarrow[Q_{col}]{c}\left({{Q_{1},\ldots,Q_{n}}}\right)\quad\text{and}\quad
Q_{1}\xrightarrow[Q^{\prime}_{col}]{a}Q^{\prime}_{1}$ be the first transitions
used on the accepting run of $w_{i}$. The construction of
$\mathcal{T}^{A}_{{t},{t^{\prime}}}$ means we have a transition
$t_{i-1}\xrightarrow{\left({{p_{i-1}},{a_{i}},{o_{i}},{p_{i}}}\right)}t_{i}$
where
$t_{i-1}={q_{p_{i-1}}}\xrightarrow[Q^{\prime}_{col}]{a}\left({{Q^{\prime}_{1},Q_{2},\ldots,Q_{k}\cup
Q_{col},\ldots,Q_{n}}}\right)$. Thus we can construct an accepting run of
$w_{i-1}$ (which is $w_{i}$ without the first $c$ on top of the top order-$1$
stack). A run from $Q_{k}\cup Q_{col}$ exists since $u_{k}$ is also the stack
annotating $c$.

  3. 3.

When $o_{i}=rew_{c}$ let
${q_{p_{i}}}\xrightarrow[Q_{col}]{c}\left({{Q_{1},\ldots,Q_{n}}}\right)$ be
the first transition on the accepting run of $w_{i}={{c}^{u}}:_{1}{v}$ for
some $v$ and $u$. From the construction of
$\mathcal{T}^{A}_{{t},{t^{\prime}}}$ we know we have a transition
$t_{i-1}\xrightarrow{\left({{p_{i-1}},{a_{i}},{o_{i}},{p_{i}}}\right)}t_{i}$
where
$t_{i-1}={q_{p_{i-1}}}\xrightarrow[Q_{col}]{a}\left({{Q_{1},\ldots,Q_{n}}}\right)$,
from which we get an accepting run of $w_{i-1}={{a}^{u}}:_{1}{v}$ as required.

  4. 4.

When $o_{i}=noop$ let
${q_{p_{i}}}\xrightarrow[Q_{col}]{a}\left({{Q_{1},\ldots,Q_{n}}}\right)$ be
the first transition on the accepting run of $w_{i}={{a}^{u}}:_{1}{v}$ for
some $v$ and $u$. From the construction of
$\mathcal{T}^{A}_{{t},{t^{\prime}}}$ we know we have a transition
$t_{i-1}\xrightarrow{\left({{p_{i-1}},{a_{i}},{o_{i}},{p_{i}}}\right)}t_{i}$
where
$t_{i-1}={q_{p_{i-1}}}\xrightarrow[Q_{col}]{a}\left({{Q_{1},\ldots,Q_{n}}}\right)$,
from which we get an accepting run of $w_{i-1}={{a}^{u}}:_{1}{v}$ as required.

Hence, for every
$\langle{p},{w}\rangle\in{Pre^{*}_{\mathcal{C}}}\mathord{\left({A_{0}}\right)}$
we have $w\in{\mathcal{L}_{q_{p}}}\mathord{\left({A}\right)}$. $\square$

###  C.2 Soundness of Saturation for ECPDS

As in the previous section, the soundness argument repeats a large part of the
proof given in ICALP 2012. We first recall the machinery used for soundness,
before giving the soundness proof.

First, assume all stack automata are such that their initial states are not
final. This is assumed for the automaton $A_{0}$ in and preserved by the
saturation function $\Gamma$.

We assign a “meaning” to each state of the automaton. For this, we define what
it means for an order-$k$ stack $w$ to satisfy a state $q\in\mathbb{Q}_{k}$,
which is denoted $w\models q$.

######  Definition C.1 ($w\models q$)

For any $Q\subseteq\mathbb{Q}_{k}$ and any order-$k$ stack $w$, we write
$w\models Q$ if $w\models q$ for all $q\in Q$, and we define $w\models q$ by a
case distinction on $q$.

  1. 1.

$q$ is an initial state in $\mathbb{Q}_{n}$. Then for any order-$n$ stack $w$,
we say that $w\models q$ if
$\langle{q},{w}\rangle\in{Pre^{*}_{\mathcal{C}}}\mathord{\left({A_{0}}\right)}$.

  2. 2.

$q$ is an initial state in $\mathbb{Q}_{k}$, labeling a transition
$q_{k+1}\xrightarrow{q}Q_{k+1}\in\Delta_{k+1}$. Then for any order-$k$ stack
$w$, we say that $w\models q$ if for all order-$(k+1)$ stacks s.t. $v\models
Q_{k+1}$, then ${w}:_{(k+1)}{v}\models q_{k+1}$.

  3. 3.

$q$ is a non-initial state in $\mathbb{Q}_{k}$. Then for any order-$k$ stack
$w$, we say that $w\models q$ if $A_{0}$ accepts $w$ from $q$.

By unfolding the definition, we have that an order-$k$ stack $w_{k}$ satisfies
an initial state $q_{k}\in\mathbb{Q}_{k}$ with
${q}\xrightarrow{q_{k}}\left({{Q_{k+1},\dots,Q_{n}}}\right)$ if for any
order-$(k+1)$ stack $w_{k+1}\models Q_{k+1}$, …, and any order-$n$ stack
$w_{n}\models Q_{n}$, we have ${w_{k}}:_{(k+1)}{{\cdots}:_{n}{w_{n}}}\models
q$.

######  Definition C.2 (Soundness of transitions)

A transition ${q}\xrightarrow[Q_{col}]{a}\left({{Q_{1},\ldots,Q_{k}}}\right)$
is sound if for any order-$1$ stack $w_{1}\models Q_{1}$, …, and any order-$k$
stack $w_{k}\models Q_{k}$ and any stack $u\models Q_{col}$, we have
${{a}^{u}}:_{1}{{w_{1}}:_{2}{{\cdots}:_{k}{w_{k}}}}\models q$.

The proof of the following lemma can be found in ICALP 2012 [8].

######  Lemma C.2 ([8])

If ${q_{p}}\xrightarrow[Q_{col}]{a}\left({{Q_{1},\ldots,Q_{n}}}\right)$ is
sound, then any transition
${q_{k}}\xrightarrow[Q_{col}]{a}\left({{Q_{1},\ldots,Q_{k}}}\right)$ contained
within the transition from $q_{p}$ is sound.

######  Definition C.3 (Soundness of stack automata)

A stack automaton $A$ is sound if the following holds.

  * •

$A$ is obtained from $A_{0}$ by adding new initial states of order $<n$ and
transitions starting in an initial state.

  * •

In $A$, any transition
${q}\xrightarrow[Q_{col}]{a}\left({{Q_{1},\ldots,Q_{k}}}\right)$ for $k\leq n$
is sound.

Unsurprisingly, if some order-$n$ stack $w$ is accepted by a _sound_ stack
automaton $A$ from a state $q_{p}$ then $\langle{p},{w}\rangle$ belongs to
${Pre^{*}_{\mathcal{C}}}\mathord{\left({A_{0}}\right)}$. More generally, we
have the following lemma whose proof can be found in ICALP 2012.

######  Lemma C.3 ([8])

Let $A$ be a sound stack automaton $A$ and let $w$ be an order-$k$ stack. If
$A$ accepts $w$ from a state $q\in\mathbb{Q}_{k}$ then $w\models q$. In
particular, if $A$ accepts an order-$n$ stack $w$ from a state
$q_{p}\in\mathbb{Q}_{n}$ then $\langle{p},{w}\rangle$ belongs to
${Pre^{*}_{\mathcal{C}}}\mathord{\left({A_{0}}\right)}$.

We also recall that the initial automaton $A_{0}$ is sound.

######  Lemma C.4 (Soundness of $A_{0}$ [8])

The automaton $A_{0}$ is sound.

We are now ready to prove that the soundness of saturation for extended CPDS.

######  Lemma C.5 (Soundness of $\Pi$)

The automaton $A$ constructed by saturation with $\Pi$ and $\mathcal{C}$ from
$A_{0}$ is sound.

_Proof._ The proof is by induction on the number of iterations of $\Pi$. The
base case is the automaton $A_{0}$ and the result was established in Lemma
C.4. As in the completeness case, the argument for the ordinary CPDS rules is
identical to ICALP 2012 and not repeated here (although the arguments appear
in the proof of Lemma G.3).

We argue the case for those transitions added because of extended rules
$\left({{p},{a},{{\mathcal{L}_{g}}},{p^{\prime}}}\right)$.

Hence, we consider the inductive step for transitions introduced by extended
rules of the form $\left({{p},{c},{{\mathcal{L}_{g}}},{p^{\prime}}}\right)$.
Take the $t,t^{\prime}$ and
$\left({{p_{0}},{a_{1}},{o_{1}},{p_{1}}}\right)\left({{p_{1}},{a_{2}},{o_{2}},{p_{2}}}\right)\ldots\left({{p_{\ell-1}},{a_{\ell}},{o_{\ell}},{p_{\ell}}}\right)\in{\mathcal{L}_{g}}\cap{\mathcal{L}}\mathord{\left({\mathcal{T}^{A_{i}}_{{t},{t^{\prime}}}}\right)}$
with $t^{\prime}$ being a transition of $A_{i}$ that led to the introduction
of $t$. Note $p=p_{0}$ and $p^{\prime}=p_{\ell}$.

Let $t_{0},\ldots,t_{\ell}$ be the sequence of states on the accepting run of
$\mathcal{T}^{A_{i}}_{{t},{t^{\prime}}}$. In particular $t_{0}=t$ and
$t_{\ell}=t^{\prime}$. We will prove by induction from $i=\ell$ to $i=0$ that
for each $t_{i}$, letting

$t_{i}={q_{p_{i}}}\xrightarrow[Q_{col}]{a}\left({{Q_{1},\ldots,Q_{n}}}\right)\
,$

and for all $u\models Q_{col}$, $w_{1}\models Q_{1}$, …, $w_{n}\models Q_{n}$
that for $w^{i}={{a}^{u}}:_{1}{{w_{1}}:_{2}{\cdots{}:_{n}{w_{n}}}}$ we have
${o_{\ell}}\mathord{\left({\cdots{o_{i+1}}\mathord{\left({w^{i}}\right)}}\right)}\models
q_{p^{\prime}}$. Thus, at $t_{0}=t$ , we have
${o_{\ell}}\mathord{\left({\cdots{o_{1}}\mathord{\left({w^{0}}\right)}}\right)}\models
q_{p^{\prime}}$ and thus
$\langle{p^{\prime}},{{o_{\ell}}\mathord{\left({\cdots{o_{1}}\mathord{\left({w^{0}}\right)}}\right)}}\rangle\in{Pre^{*}_{\mathcal{C}}}\mathord{\left({A_{0}}\right)}$.
Since the above sequence

$\left({{p_{0}},{a_{1}},{o_{1}},{p_{1}}}\right)\left({{p_{1}},{a_{2}},{o_{2}},{p_{2}}}\right)\ldots\left({{p_{\ell-1}},{a_{\ell}},{o_{\ell}},{p_{\ell}}}\right)$

is in ${\mathcal{L}_{g}}$, we have
$\langle{p_{0}},{w^{0}}\rangle\in{Pre^{*}_{\mathcal{C}}}\mathord{\left({A_{0}}\right)}$
and thus $w^{0}\models q_{p}$, giving soundness of the new transition $t_{0}$.

The base case is $t_{\ell}=t^{\prime}$. Since $t^{\prime}$ appears in $A_{i}$,
we know it is sound. That gives us that $w^{\ell}\models q_{p^{\prime}}$ as
required.

Now assume that $t_{i}$ satisfies the hypothesis. We prove that $t_{i-1}$ does
also. Take the transition
$t_{i-1}\xrightarrow{\left({{p_{i-1}},{a_{i}},{o_{i}},{p_{i}}}\right)}t_{i}$.
We perform a case split on $o_{i}$. Readers familiar with ICALP 2012 will
notice that the arguments here very much follow the soundness proof for
ordinary rules.

  1. 1.

Assume that $o_{i}=copy_{k}$, that we had

$t_{i}={q_{p_{i}}}\xrightarrow[Q_{col}]{a}\left({{Q_{1},\ldots,Q_{n}}}\right)\quad\text{and}\quad{Q_{k}}\xrightarrow[Q^{\prime}_{col}]{a}\left({{Q^{\prime}_{1},\ldots,Q^{\prime}_{k}}}\right)$

where the latter set of transition are in $A_{i}$ and therefore sound, and
that

$t_{i-1}={q_{p_{i-1}}}\xrightarrow[Q_{col}\cup
Q^{\prime}_{col}]{a}\left({{Q_{1}\cup Q^{\prime}_{1},\ldots,Q_{k-1}\cup
Q^{\prime}_{k-1},Q^{\prime}_{k},Q_{k+1},\ldots,Q_{n}}}\right)\ .$

To establish the property for this latter transition, we have to prove that
for any $w_{1}\models Q_{1}\cup Q^{\prime}_{1},\ldots$, any $w_{k-1}\models
Q_{k-1}\cup Q^{\prime}_{k-1}$, any $w_{k}\models Q^{\prime}_{k},$ any
$w_{k+1}\models Q_{k+1},\ldots$, any $w_{n}\models Q_{n}$ and any $u\models
Q_{col}\cup Q^{\prime}_{col}$, we have for
$w^{i-1}={{a}^{u}}:_{1}{{w_{1}}:_{2}{{\cdots}:_{n}{w_{n}}}}$ that
${o_{\ell}}\mathord{\left({\cdots{o_{i}}\mathord{\left({w^{i-1}}\right)}}\right)}\models
q_{p^{\prime}}$.

Let
$v={top_{k}}\mathord{\left({w^{i-1}}\right)}={{a}^{u}}:_{1}{{w_{1}}:_{2}{{\cdots}:_{(k-1)}{w_{k-1}}}}$.

From the soundness of
${Q_{k}}\xrightarrow[Q^{\prime}_{col}]{a}\left({{Q^{\prime}_{1},\ldots,Q^{\prime}_{k}}}\right)$
and as $u\models Q^{\prime}_{col},w_{1}\models
Q^{\prime}_{1},\ldots,w_{k}\models Q^{\prime}_{k}$, we have
${v}:_{k}{w_{k}}\models Q_{k}$.

Then, from $w_{1}\models Q_{1},\ldots,w_{k-1}\models Q_{k-1}$, and
${v}:_{k}{w_{k}}\models Q_{k}$, and $w_{k+1}\models
Q_{k+1},\ldots,w_{n}\models Q_{n}$ and $u\models Q_{col}$ and the induction
hypothesis for
$t_{i}={q_{p_{i}}}\xrightarrow[Q_{col}]{a}\left({{Q_{1},\ldots,Q_{n}}}\right)$
we get

${o_{\ell}}\mathord{\left({\cdots{o_{i+1}}\mathord{\left({{copy_{k}}\mathord{\left({w}\right)}}\right)}}\right)}={o_{\ell}}\mathord{\left({\cdots{o_{i+1}}\mathord{\left({{v}:_{k}{{v}:_{k}{{w_{k}}:_{(k+1)}{{\cdots}:_{n}{w_{n}}}}}}\right)}}\right)}\models
q_{p^{\prime}}$

as required.

  2. 2.

Assume that $o_{i}=push^{k}_{b}$, that we have

$t_{i}={q_{p_{i}}}\xrightarrow[Q_{col}]{b}\left({{Q_{1},\ldots,Q_{n}}}\right)\quad\text{and}\quad
Q_{1}\xrightarrow[Q^{\prime}_{col}]{a}(Q^{\prime}_{1})$

where the latter set of transitions is sound, and that we have

$t_{i-1}={q_{p_{i-1}}}\xrightarrow[Q^{\prime}_{col}]{a}\left({{Q^{\prime}_{1},Q_{2},\ldots,Q_{k}\cup
Q_{col},\ldots,Q_{n}}}\right)\ .$

To prove the induction hypothesis for the latter transition, we have to prove
that for any $w_{1}\models Q^{\prime}_{1}$, any $w_{2}\models Q_{2},\ldots$,
any $w_{k-1}\models Q_{k-1}$, any $w_{k}\models Q_{k}\cup Q_{col}$, any
$w_{k+1}\models Q_{k+1},\ldots$, any $w_{n}\models Q_{n}$ and any $u\models
Q^{\prime}_{col}$, that we have for
$w^{i-1}={{a}^{u}}:_{1}{{w_{1}}:_{2}{{\cdots}:_{n}{w_{n}}}}$ that
${o_{\ell}}\mathord{\left({\cdots{o_{i}}\mathord{\left({w^{i-1}}\right)}}\right)}\models
q_{p^{\prime}}$.

From the soundness of
${Q_{1}}\xrightarrow[Q^{\prime}_{col}]{a}\left({{Q^{\prime}_{1}}}\right)$ and
as $u\models Q^{\prime}_{col}$ and $w_{1}\models Q^{\prime}_{1}$ we have
${{a}^{u}}:_{1}{w_{1}}\models Q_{1}$.

Then, from ${{a}^{u}}:_{1}{w_{1}}\models Q_{1},w_{2}\models
Q_{2},\ldots,w_{n}\models Q_{n}$, and
${top_{k+1}}\mathord{\left({{pop_{k}}\mathord{\left({w}\right)}}\right)}=w_{k}\models
Q_{col}$, and induction for
$t_{i}={q_{p_{i}}}\xrightarrow[Q_{col}]{b}\left({{Q_{1},\ldots,Q_{n}}}\right)$,
we get

${o_{\ell}}\mathord{\left({\cdots{o_{i+1}}\mathord{\left({{push^{k}_{b}}\mathord{\left({w^{i-1}}\right)}}\right)}}\right)}={o_{\ell}}\mathord{\left({\cdots{o_{i+1}}\mathord{\left({{{b}^{w_{k}}}:_{1}{{{a}^{u}}:_{1}{{w_{1}}:_{2}{{\cdots}:_{n}{w_{n}}}}}}\right)}}\right)}\models
q_{p^{\prime}}$

as required.

  3. 3.

Assume that $o=rew_{b}$, that we have
$t_{i}={q_{p_{i}}}\xrightarrow[Q_{col}]{b}\left({{Q_{1},\dots,Q_{n}}}\right)$
and that

$t_{i-1}={q_{p}}\xrightarrow[Q_{col}]{a}\left({{Q_{1},\dots,Q_{n}}}\right)\ .$

To prove the hypothesis for this later transition, we have to prove that for
any $w_{1}\models Q_{1},\ldots,$ for any $w_{n}\models Q_{n}$ and any
$u\models Q_{col}$, we have that for
$w^{i-1}={{a}^{u}}:_{1}{{w_{1}}:_{2}{{\cdots}:_{n}{w_{n}}}}$ we have
${o_{\ell}}\mathord{\left({\cdots{o_{i}}\mathord{\left({w^{i-1}}\right)}}\right)}\models
q_{p^{\prime}}$.

From $w_{1}\models Q_{1},\ldots,w_{n}\models Q_{n}$, and $u\models Q_{col}$,
and the hypothesis for
$t_{i}={q_{p_{i}}}\xrightarrow[Q_{col}]{b}\left({{Q_{1},\dots,Q_{n}}}\right)$,
we get

${o_{\ell}}\mathord{\left({\cdots{o_{i+1}}\mathord{\left({{rew_{b}}\mathord{\left({w^{i-1}}\right)}}\right)}}\right)}={o_{\ell}}\mathord{\left({\cdots{o_{i+1}}\mathord{\left({{{b}^{u}}:_{1}{{w_{1}}:_{2}{{\cdots}:_{n}{w_{n}}}}}\right)}}\right)}\models
q_{p^{\prime}}$

as required.

  4. 4.

Assume that $o=noop$, that we have
$t_{i}={q_{p_{i}}}\xrightarrow[Q_{col}]{b}\left({{Q_{1},\dots,Q_{n}}}\right)$
and that

$t_{i-1}={q_{p}}\xrightarrow[Q_{col}]{a}\left({{Q_{1},\dots,Q_{n}}}\right)\ .$

To prove the hypothesis for this later transition, we have to prove that for
any $w_{1}\models Q_{1},\ldots,$ for any $w_{n}\models Q_{n}$ and any
$u\models Q_{col}$, we have that for
$w^{i-1}={{a}^{u}}:_{1}{{w_{1}}:_{2}{{\cdots}:_{n}{w_{n}}}}$ we have
${o_{\ell}}\mathord{\left({\cdots{o_{i}}\mathord{\left({w^{i-1}}\right)}}\right)}\models
q_{p^{\prime}}$.

From $w_{1}\models Q_{1},\ldots,w_{n}\models Q_{n}$, and $u\models Q_{col}$,
and the hypothesis for
$t_{i}={q_{p_{i}}}\xrightarrow[Q_{col}]{a}\left({{Q_{1},\dots,Q_{n}}}\right)$,
we get

${o_{\ell}}\mathord{\left({\cdots{o_{i+1}}\mathord{\left({{rew_{a}}\mathord{\left({w^{i-1}}\right)}}\right)}}\right)}={o_{\ell}}\mathord{\left({\cdots{o_{i+1}}\mathord{\left({{{a}^{u}}:_{1}{{w_{1}}:_{2}{{\cdots}:_{n}{w_{n}}}}}\right)}}\right)}\models
q_{p^{\prime}}$

as required.

This completes the proof. $\square$

###  C.3 Complexity of Saturation for ECPDS

We argue that saturation for ECPDS maintains the same complexity as saturation
for CPDS.

###### Proposition C.1

The saturation construction for an order-$n$ CPDS $\mathcal{C}$ and an
order-$n$ stack automaton $A_{0}$ runs in $n$-EXPTIME.

_Proof._ The number of states of $A$ is bounded by
$2\uparrow_{(n-1)}\left({\ell}\right)$ where $\ell$ is the size of
$\mathcal{C}$ and $A_{0}$: each state in $\mathbb{Q}_{k}$ was either in
$A_{0}$ or comes from a transition in $\Delta_{k+1}$. Since the automata are
alternating, there is an exponential blow up at each order except at
order-$n$. Each iteration of the algorithm adds at least one new transition.
Only $2\uparrow_{n}\left({\ell}\right)$ transitions can be added. $\square$

The complexity can be reduced by a single exponential when runs of the stack
automata are “non-alternating at order-$n$”. In this case an exponential is
avoided by only adding a transition
${q_{p}}\xrightarrow[Q_{col}]{a}\left({{Q_{1},\ldots,Q_{n}}}\right)$ when
$Q_{n}$ contains at most one element.

We refer the reader to ICALP 2012 for a full discussion of non-alternation
since it relies on the original notion of collapsible pushdown system that we
have not defined here. ICALP 2012 describes the connection between our notion
of CPDS (using annotations) and the original notion, as well as defining non-
alternation at order-$n$ and arguing completeness for the restricted
saturation step. It is straightforward to extend this proof to include ECPDS
as in the proof of Lemma C.1 (Completeness of $\Pi$) above.

##  Appendix D Definitions and Proofs for Multi-Stack CPDS

###  D.1 Multi-Stack Collapsible Pushdown Automata

We formally define mutli-stack collapsible pushdown automata.

######  Definition D.1 (Multi-Stack Collapsible Pushdown Automata)

An order-$n$ _multi-stack collapsible pushdown automaton ( $n$-OCPDA)_ over
input alphabet $\Gamma$ is a tuple
$\mathcal{C}=\left({\mathcal{P},\Sigma,\mathcal{R}_{1},\ldots,\mathcal{R}_{m}}\right)$
where $\mathcal{P}$ is a finite set of control states, $\Sigma$ is a finite
stack alphabet, $\Gamma$ is a finite set of output symbols, and for each
$1\leq i\leq m$ we have a set of rules
$\mathcal{R}_{i}\subseteq\mathcal{P}\times\Sigma\times\Gamma\times\mathcal{O}_{n}\times\mathcal{P}$.

Configurations of an OCPDA are defined identically to configurations for
OCPDS. We have a transition

$\langle{p},{w_{1},\ldots,w_{m}}\rangle\xrightarrow{\gamma}\langle{p^{\prime}},{w_{1},\ldots,w_{i-1},w^{\prime}_{i},w_{i+1},\ldots,w_{m}}\rangle$

whenever
$r=\left({{p},{a},{\gamma},{o},{p^{\prime}}}\right)\in\mathcal{R}_{i}$ with
$a={top_{1}}\mathord{\left({w}\right)}$,
$w^{\prime}_{i}={o}\mathord{\left({w_{i}}\right)}$.

###  D.2 Regular Sets of Configurations

We prove several properties about Definition 4.4 (Regular Set of
Configurations).

###### Property D.1

Regular sets of configurations of a multi-stack CPDS

  1. 1.

form an effective boolean algebra,

  2. 2.

the emptiness problem is decidable in PSPACE,

  3. 3.

the membership problem is decidable in linear time.

_Proof._ We first prove $(\ref{item:bool-alg})$. We recall from [8] that stack
automata form an effective boolean algebra. Given two regular sets $\chi_{1}$
and $\chi_{2}$, we can form $\chi=\chi_{1}\cup\chi_{2}$ as the simple union of
the two sets of tuples. We obtain the intersection of $\chi_{1}$ and
$\chi_{2}$ by defining $\chi=\chi_{1}\cap\chi_{2}$ via a product construction.
That is,

$\chi=\left\\{{\left({p,A_{1}\cap A^{\prime}_{1},\ldots,A_{m}\cap
A^{\prime}_{m}}\right)}\ \left|\
{\begin{array}[]{c}\left({p,A_{1},\ldots,A_{m}}\right)\in\chi_{1}\ \land\\\
\left({p,A^{\prime}_{1},\ldots,A^{\prime}_{m}}\right)\in\chi_{2}\end{array}}\right.\right\\}\
.$

It remains to define the complement $\overline{\chi}$ of a set $\chi$. Let
$\chi=\chi_{1}\cup\cdots\cup\chi_{\ell}$ where each $\chi_{i}$ is a singleton
set of tuples. Observe that
$\overline{\chi}=\overline{\chi_{1}}\cap\cdots\cap\overline{\chi_{\ell}}$.
Hence, we define for a singleton $\chi_{i}$ its complement
$\overline{\chi_{i}}$. Let $A$ be a stack automaton accepting all stacks.
Furthermore, let $\chi_{i}$ contain only
$\left({p,A_{1},\ldots,A_{\ell}}\right)$. We define

$\begin{array}[]{rcl}\overline{\chi_{i}}&=&\left\\{{\left({p^{\prime},A,\ldots,A}\right)}\
\left|\ {p\neq p^{\prime}\in\mathcal{P}}\right.\right\\}\ \cup\\\
&&\left\\{{\left({p,A,\ldots,A,\overline{A_{j}},A,\ldots,A}\right)}\ \left|\
{1\leq j\leq m}\right.\right\\}\ .\end{array}$

That is, either the control state does not match, or at least one of the $m$
stacks does not match.

We now prove $(\ref{item:emptiness})$. We know from [8] that the emptiness
problem for a stack automaton is PSPACE. By checking all tuples to find some
tuple $\left({p,A_{1},\ldots,A_{m}}\right)$ such that $A_{i}$ is non-empty for
all $i$, we have a PSPACE algorithm for determining the emptiness of a regular
set $\chi$.

Finally, we show $(\ref{item:membership})$, recalling from [8] that the
membership problem for stack automata is linear time. To check whether
$\langle{p},{w_{1},\ldots,w_{m}}\rangle$ is contained in $\chi$ we check each
tuple $\left({p,A_{1},\ldots,A_{m}}\right)\in\chi$ to see if $w_{i}$ is
contained in $A_{i}$ for all $i$. This requires linear time. $\square$

##  Appendix E Proofs for Ordered CPDS

###  E.1 Proofs for Simulation by $\mathcal{C}^{R}$

We prove Lemma 5.1 ($\mathcal{C}^{R}$ simulates $\mathcal{C}$) via Lemma E.1
and Lemma E.2 below.

###### Lemma E.1

Given an $n$-OCPDS $\mathcal{C}$ and control states
${p_{\text{in}}},{p_{\text{out}}}$, we have

$\langle{{p_{\text{in}}}},{\perp_{n},\ldots,\perp_{n},w}\rangle\longrightarrow\cdots\longrightarrow\langle{{p_{\text{out}}}},{\perp_{n},\ldots,\perp_{n}}\rangle\
.$

only if
$\langle{{p_{\text{in}}}},{w}\rangle\in{Pre^{*}_{\mathcal{C}^{R}}}\mathord{\left({A}\right)}$,
where $A$ is the $\mathcal{P}$-stack automaton accepting only the
configuration $\langle{{p_{\text{out}}}},{\perp_{n}}\rangle$.

_Proof._ Take such a run

$\langle{{p_{\text{in}}}},{\perp_{n},\ldots,\perp_{n},w}\rangle\longrightarrow\cdots\longrightarrow\langle{{p_{\text{out}}}},{\perp_{n},\ldots,\perp_{n}}\rangle$

of $\mathcal{C}$. Observe that the run can be partitioned into
$\tau_{0}\sigma_{1}\tau_{1}\ldots\sigma_{\ell}\tau_{\ell}$ where during each
$\tau_{i}$, the first $(m-1)$ stacks are $\perp_{n}$, and, during each
$\sigma_{i}$, there is at least one stack in the first $(m-1)$ stacks that is
not $\perp_{n}$. Let $p^{1}_{i}$ be the control state of the first
configuration of $\tau_{i}$, $p^{2}_{i}$ be the control state in the final
configuration of $\tau_{i}$, $p^{3}_{i}$ be the control state at the beginning
of each $\sigma_{i}$, and $p^{4}_{i}$ be the control state at the end of each
$\sigma_{i}$. Note, $p^{4}_{\ell}={p_{\text{out}}}$ and
$p^{1}_{1}={p_{\text{in}}}$. Next, let $r_{i}$ be the rule fired between the
final configuration of $\tau_{i-1}$ and the first configuration of
$\sigma_{i}$ (if it exists). Finally, let $w_{i}$ be the contents of stack $m$
in the final configuration of each $\tau_{i}$. Note $w_{\ell}=w$.

We proceed by backwards induction from $i=\ell$ down to $i=0$. Trivially it is
the case that
$\langle{p^{4}_{\ell}},{w_{\ell}}\rangle\in{Pre^{*}_{\mathcal{C}^{R}}}\mathord{\left({A}\right)}$.

In the inductive step, first assume
$\langle{p^{4}_{i}},{w_{i}}\rangle\in{Pre^{*}_{\mathcal{C}^{R}}}\mathord{\left({A}\right)}$.
We have the final configuration of $\tau_{i}$ is
$\langle{p^{4}_{i}},{\perp_{n},\ldots,\perp_{n},w_{i}}\rangle$. Let
$\langle{p^{3}_{i}},{\perp_{n},\ldots,\perp_{n},w^{\prime}}\rangle$ be the
first configuration of $\tau_{i}$. Note, since we assume all rules of the form
$\left({{p_{1}},{\perp},{o},{p_{2}}}\right)$ have $o=push^{n}_{a}$ for some
$a$, and during $\tau_{i}$ the first $(m-1)$ stacks are empty, we know that no
rule from $\mathcal{R}_{1},\ldots,\mathcal{R}_{m-1}$ was used during
$\tau_{i}$. Thus, $\tau_{i}$ is a run of $\mathcal{C}^{R}$ using only rules
from $\mathcal{R}_{m}$. Hence, we have
$\langle{p^{3}_{i}},{w^{\prime}}\rangle\in{Pre^{*}_{\mathcal{C}^{R}}}\mathord{\left({A}\right)}$.

Now consider $\sigma_{i}$ with
$\langle{p^{3}_{i}},{\perp_{n},\ldots,\perp_{n},w^{\prime}}\rangle$ appended
to the end. Suppose we have that
$r_{i-1}=\left({{p^{4}_{i-1}},{\perp},{push^{n}_{b}},{p^{1}_{i}}}\right)\in\mathcal{R}_{j}$.
We thus have a run

$\langle{p^{1}_{i}},{w^{\prime}_{1},\ldots,w^{\prime}_{m-1},w_{i-1}}\rangle\xrightarrow{r^{1}}\cdots\xrightarrow{r^{\ell-1}}\langle{p^{2}_{i}},{w^{\prime\prime}_{1},\ldots,w^{\prime\prime}_{m}}\rangle\xrightarrow{r^{\ell}}\langle{p^{3}_{i}},{\perp_{n},\ldots,\perp_{n},w^{\prime}}\rangle$

where $w^{\prime}_{j}={push^{n}_{b}}\mathord{\left({\perp_{n}}\right)}$ and
$w^{\prime}_{j^{\prime}}=\perp_{n}$ for all $j^{\prime}\neq j$. Since it is
not the case that the first $(m-1)$ stacks are empty, we know that only
generating rules from $\mathcal{R}_{m}$ can be used during this run. Let
${top_{1}}\mathord{\left({w_{i-1}}\right)}=a$. From this run we can
immediately project a sequence
$\left({{p^{0}},{a^{1}},{o^{1}},{p^{1}}}\right)\left({{p^{1}},{a^{2}},{o^{2}},{p^{2}}}\right)\ldots\left({{p^{\ell^{\prime}-1}},{a^{\ell}},{o^{\ell^{\prime}}},{p^{\ell^{\prime}}}}\right)\in{\mathcal{L}^{{b},{j}}_{{p^{1}_{i}},{a},{p^{3}_{i}}}}\mathord{\left({\mathcal{C}^{L}}\right)}$
such that we have
$w^{\prime}={o^{\ell^{\prime}}}\mathord{\left({\cdots{o^{1}}\mathord{\left({w_{i-1}}\right)}}\right)}$,
$p^{0}=p^{1}_{i}$ and $p^{\ell^{\prime}}=p^{3}_{i}$. Since we have
$\langle{p^{3}_{i}},{w^{\prime}}\rangle\in{Pre^{*}_{\mathcal{C}^{R}}}\mathord{\left({A}\right)}$
and a rule
$\left({{p^{4}_{i-1}},{a},{{\mathcal{L}^{{b},{j}}_{{p^{1}_{i}},{a},{p^{3}_{i}}}}\mathord{\left({\mathcal{C}^{L}}\right)}},{p^{3}_{i}}}\right)$
in $\mathcal{C}^{R}$, we thus have
$\langle{p^{4}_{i-1}},{w_{i-1}}\rangle\in{Pre^{*}_{\mathcal{C}^{R}}}\mathord{\left({A}\right)}$
as required.

Hence, when $i=0$, we have
$\langle{{p_{\text{in}}}},{w}\rangle\in{Pre^{*}_{\mathcal{C}^{R}}}\mathord{\left({A}\right)}$,
completing the proof. $\square$

###### Lemma E.2

Given an $n$-OCPDS $\mathcal{C}$ and control states
${p_{\text{in}}},{p_{\text{out}}}$, we have

$\langle{{p_{\text{in}}}},{\perp_{n},\ldots,\perp_{n},w}\rangle\longrightarrow\cdots\longrightarrow\langle{{p_{\text{out}}}},{\perp_{n},\ldots,\perp_{n}}\rangle\
.$

whenever
$\langle{{p_{\text{in}}}},{w}\rangle\in{Pre^{*}_{\mathcal{C}^{R}}}\mathord{\left({A}\right)}$,
where $A$ is the $\mathcal{P}$-stack automaton accepting only the
configuration $\langle{{p_{\text{out}}}},{\perp_{n}}\rangle$.

_Proof._ Since
$\langle{{p_{\text{in}}}},{w}\rangle\in{Pre^{*}_{\mathcal{C}^{R}}}\mathord{\left({A}\right)}$
we have a run of $\mathcal{C}^{R}$ of the form $\sigma_{1}\ldots\sigma_{\ell}$
where the rules used to connect the last configuration of $\sigma_{i}$ to
$\sigma_{i+1}$ are of the form
$\left({{p^{\prime}_{i}},{a},{{\mathcal{L}_{g}}},{p_{i+1}}}\right)$ and no
other rules of this form are used otherwise. Thus, let $p^{\prime}_{i}$ denote
the control state at the end of $\sigma_{i}$ and $p_{i}$ denote the control
state in the first configuration of $\sigma_{i}$. Similarly, let
$w^{\prime}_{i}$ denote the stack contents at the end of $\sigma_{i}$ and
$w_{i}$ the stack contents at the beginning.

We proceed by induction from $i=\ell$ down to $i=1$. In the base case, we
immediately have a run from
$\langle{p_{\ell}},{\perp_{n},\ldots,\perp_{n},w_{\ell}}\rangle$ to
$\langle{p^{\prime}_{\ell}},{\perp_{n},\ldots,\perp_{n}}\rangle$. Now, assume
the we have a run from
$\langle{p^{\prime}_{i}},{\perp_{n},\ldots,\perp_{n},w^{\prime}_{i}}\rangle$
to the final configuration. Since we have a run to this configuration from
$\langle{p_{i}},{w_{i}}\rangle$ to
$\langle{p^{\prime}_{i}},{w^{\prime}_{i}}\rangle$ in $\mathcal{C}^{R}$ that
uses only ordinary rules, we can execute the same run from
$\langle{p_{i}},{\perp_{n},\ldots,\perp_{n},w_{i}}\rangle$ to reach
$\langle{p^{\prime}_{i}},{\perp_{n},\ldots,\perp_{n},w^{\prime}_{i}}\rangle$.

Now consider the rule
$\left({{p^{\prime}_{i-1}},{a},{{\mathcal{L}_{g}}},{p_{i}}}\right)$ that
connects $\sigma_{i-1}$ and $\sigma_{i}$. We have
${\mathcal{L}_{g}}={\mathcal{L}^{{b},{j}}_{{p^{1}_{i}},{a},{p_{i}}}}\mathord{\left({\mathcal{C}^{L}}\right)}$
for some $p^{1}_{i}$, $b$ and $j$, and there is a rule
$\left({{p^{\prime}_{i-1}},{\perp},{push^{n}_{b}},{p^{1}_{i}}}\right)\in\mathcal{R}_{j}$
of $\mathcal{C}$. Furthermore, there is a sequence
$\left({{p^{0}},{a^{1}},{o^{1}},{p^{1}}}\right)\left({{p^{1}},{a^{2}},{o^{2}},{p^{2}}}\right)\ldots\left({{p^{\ell^{\prime}-1}},{a^{\ell}},{o^{\ell^{\prime}}},{p^{\ell^{\prime}}}}\right)\in{\mathcal{L}_{g}}$
such that
$w_{i}={o^{\ell^{\prime}}}\mathord{\left({\cdots{o^{1}}\mathord{\left({w^{\prime}_{i-1}}\right)}}\right)}$,
$p^{0}=p^{1}_{i}$, and $p^{\ell^{\prime}}=p_{i}$.

From the definition of $\mathcal{C}^{L}$, this sequence immediately describes
a run

$\begin{array}[]{rcl}\langle{p^{\prime}_{i-1}},{\perp_{n},\ldots,\perp_{n},w^{\prime}_{i-1}}\rangle&\longrightarrow&\langle{p^{1}_{i}},{\perp_{n},\ldots,{push^{n}_{b}}\mathord{\left({\perp_{n}}\right)},\ldots,\perp_{n},w^{\prime}_{i-1}}\rangle\\\
&\longrightarrow&\cdots\\\
&\longrightarrow&\langle{p_{i}},{\perp_{n},\ldots,\perp_{n},w_{i}}\rangle\end{array}$

of $\mathcal{C}$. Thus we have a run from
$\langle{p^{\prime}_{i-1}},{\perp_{n},\ldots,\perp_{n},w^{\prime}_{i-1}}\rangle$
to the final configuration, to complete the inductive case.

Finally, when $i=1$, we repeat the first half of the argument above to obtain
a run from $\langle{p_{1}},{\perp_{n},\ldots,\perp_{n},w_{1}}\rangle$, and
since $p_{1}={p_{\text{in}}}$ and $w_{1}=w$ we have a run of $\mathcal{C}$ as
required. $\square$

###  E.2 Proofs for Language Emptiness for OCPDS

We prove Lemma 5.2 (Language Emptiness for OCPDS) below.

_Proof._ By standard product construction arguments, a run of
$\mathcal{C}_{\emptyset}$ can be projected into runs of $\mathcal{C}^{L}$ and
$\mathcal{T}^{A_{i}}_{{t},{t^{\prime}}}$ and vice-versa. We need only note
that in any control state $\left({p,t_{1}}\right)$ of
$\mathcal{C}_{\emptyset}$, the corresponding state in $\mathcal{C}^{L}$ is
always $\left({p,{top_{1}}\mathord{\left({t_{1}}\right)}}\right)$. $\square$

###  E.3 Global Reachability

We provide an inductive proof of global reachability for ordered CPDS.

_Proof._ Take $A_{m}={Pre^{*}_{\mathcal{C}^{R}}}\mathord{\left({A}\right)}$
from Lemma 5.1 ($\mathcal{C}^{R}$ simulates $\mathcal{C}$). Furthermore, let
$A_{\perp}$ be the stack automaton accepting only $\perp_{n}$ from its initial
state. For each control state $p$, we have that
$\left({p,A_{\perp},\ldots,A_{\perp},A_{m}}\right)$ represents all
configurations $\langle{p},{\perp_{n},\ldots,\perp_{n},w_{m}}\rangle$ for
which there is a run to
$\langle{{p_{\text{out}}}},{\perp_{n},\ldots,\perp_{n}}\rangle$ when $A_{m}$
is restricted to have initial state $q_{p}$.

Hence, inductively assume for $i+1$ that we have a finite set of tuples $\chi$
such that for each configuration
$\langle{p},{\perp_{n},\ldots,\perp_{n},w_{i+1},\ldots,w_{m}}\rangle$ for
which there is a run to
$\langle{{p_{\text{out}}}},{\perp_{n},\ldots,\perp_{n}}\rangle$ there is a
tuple $\left({p,A_{\perp},\ldots,A_{\perp},A_{i+1},\ldots,A_{m}}\right)$ such
that $w_{j}$ is accepted by $A_{j}$ for each $j$.

Now consider any configuration
$\langle{p},{\perp_{n},\ldots,\perp_{n},w_{i},\ldots,w_{m}}\rangle$ that can
reach the final configuration. We know the run goes via some
$\langle{p^{\prime}},{\perp_{n},\ldots,\perp_{n},w^{\prime}_{i+1},\ldots,w^{\prime}_{m}}\rangle$
accepted by some tuple
$\left({p^{\prime},A_{\perp},\ldots,A_{\perp},A_{i+1},\ldots,A_{m}}\right)\in\chi$.
Furthermore, we know from the proof of correctness of the extended saturation
algorithm, that there is a run of the $i$ stack OCPDS
$\mathcal{C}_{\emptyset}$ from
$\langle{\left({p,t_{i+1},\ldots,t_{m}}\right)},{\perp_{n},\ldots,\perp_{n},w_{i}}\rangle$
to
$\langle{\left({p^{\prime},t^{\prime}_{i+1},\ldots,t^{\prime}_{m}}\right)},{\perp_{n},\ldots,\perp_{n}}\rangle$
where

  1. 1.

$t^{\prime}_{j}$ is the initial transition of $A_{j}$ accepting
$w^{\prime}_{j}$, and

  2. 2.

the sequence of stack operations to the $j$th stack $o_{1},\ldots,o_{\ell}$
connected to this run give
$w^{\prime}_{j}={o_{\ell}}\mathord{\left({\cdots{o_{1}}\mathord{\left({w_{j}}\right)}}\right)}$,
and

  3. 3.

$w_{j}$ can be accepted by first taking transition $t_{j}$ and thereafter only
transitions in $A_{j}$.

Thus, let $A_{i}$ be
${Pre^{*}_{\mathcal{C}_{\emptyset}}}\mathord{\left({A}\right)}$ where $A$
accepts
$\langle{\left({p^{\prime},t^{\prime}_{i+1},\ldots,t^{\prime}_{m}}\right)},{\perp_{n}}\rangle$.
Restrict $A_{i}$ to have initial state
$q_{\left({p,t_{i+1},\ldots,t_{m}}\right)}$ and let $A^{t_{j}}_{j}$ be the
automaton $A_{j}$ with the transition $t_{j}$ added from a new state, which is
designated as the initial state. Thus, for each configuration
$\langle{p},{\perp_{n},\ldots,\perp_{n},w_{i},\ldots,w_{m}}\rangle$, there is
a tuple
$\left({p,A_{\perp},\ldots,A_{\perp},A_{i},A^{t_{i+1}}_{i+1},\ldots,A^{t_{m}}_{m}}\right)$
such that $w_{i}$ is accepted by $A_{i}$ and $w_{j}$ is accepted by
$A^{t_{j}}_{j}$ for all $j>i$. This results in a finite set of tuples
$\chi^{\prime}$ satisfying the induction hypothesis.

Thus, after $i=1$ we obtain a finite set of tuples $\chi$ of the form
$\left({p,A_{1},\ldots,A_{m}}\right)$ representing all configurations that can
reach $\langle{{p_{\text{out}}}},{\perp_{n},\ldots,\perp_{n}}\rangle$, as
required. $\square$

###  E.4 Complexity

Assume $n>1$. Our control state reachability algorithm requires
$2\uparrow_{m(n-1)}\left({\ell}\right)$ time, where $\ell$ is polynomial in
the size of the OCPDS. Beginning with stack $m$, the saturation algorithm can
add at most
${\mathcal{O}}\mathord{\left({2\uparrow_{n-1}\left({\ell}\right)}\right)}$
transitions over the same number of iterations. Each of these iterations may
require analysis of some $\mathcal{C}_{\emptyset}$ which has
${\mathcal{O}}\mathord{\left({2\uparrow_{n-1}\left({\ell}\right)}\right)}$
control states and thus the stack-automaton constructed by saturation over
$\mathcal{C}_{\emptyset}$ may have up to
${\mathcal{O}}\mathord{\left({2\uparrow_{2(n-1)}\left({\ell}\right)}\right)}$
transitions. By continuing in this way, we have at most
${\mathcal{O}}\mathord{\left({2\uparrow_{(m-1)(n-1)}\left({\ell}\right)}\right)}$
control states when there is only one stack remaining, and thus the number of
transitions, and the total running time of the algorithm is
${\mathcal{O}}\mathord{\left({2\uparrow_{m(n-1)}\left({\ell}\right)}\right)}$.
This also gives us at most
${\mathcal{O}}\mathord{\left({2\uparrow_{mn}\left({\ell}\right)}\right)}$
tuples in the solution to the global reachability problem.

##  Appendix F Phase-Bounded CPDS

Phase-bounding [29] for multi-stack pushdown systems is a restriction where
each computation can be split into a fixed number of phases. During each
phase, characters can only be removed from one stack, but push actions may
occur on any stack.

######  Definition F.1 (Phase-Bounded CPDS)

Given a fixed number $\zeta$ of phases, an order-$n$ _phase-bounded CPDS_
($n$-PBCPDS) is an $n$-MCPDS with the restriction that each run $\sigma$ can
be partitioned into $\sigma_{1}\ldots\sigma_{\zeta}$ and for all $i$, if some
transition in $\sigma_{i}$ by $r\in\mathcal{R}_{j}$ on stack $j$ for some $j$
is consuming, then all consuming transitions in $\sigma_{i}$ are by some
$r^{\prime}\in\mathcal{R}_{j}$ on stack $j$.

We give a direct111For PDS, phase-bounded reachability can be reduced to
ordered PDS. We do not know if this holds for CPDS, and prefer instead to give
a direct algorithm. algorithm for deciding the reachability problem over
phase-bounded CPDSs. We remark that Seth [28] presented a saturation technique
for order-$1$ phase-bounded pushdown systems. Our algorithm was developed
independently of Seth’s, but our product construction can be compared with
Seth’s automaton $T_{i}$.

######  Theorem F.1 (Decidability of the Reachability Problems)

For $n$-PBCPDSs the control state reachability problem and the global control
state reachability problem are decidable.

In Appendix F.3 we show that our control state reachability algorithm will
require
${\mathcal{O}}\mathord{\left({2\uparrow_{m(n-1)}\left({\ell}\right)}\right)}$
time, where $\ell$ is polynomial in the size of the PBCPDS, and we have at
most ${\mathcal{O}}\mathord{\left({2\uparrow_{mn}\left({\ell}\right)}\right)}$
tuples in the solution to the global reachability problem.

#### Control State Reachability

A run of the PBCPDS will be $\sigma_{1}\ldots\sigma_{\zeta}$, assuming
(w.l.o.g.) that all phases are used. We can guess (or enumerate) the sequence
$p_{0}p_{1}\ldots p_{\zeta}$ of control states occurring at the boundaries of
each $\sigma_{i}$. That is, $\sigma_{i}$ ends with control state $p_{i}$,
$p_{\zeta}$ is the target control state, and $p_{0}$ is the initial control
state. We also guess for each $i$, the stack $\iota_{i}$ that may perform
consuming operations between $p_{i-1}$ and $p_{i}$. Our algorithm iterates
from $i=\zeta$ down to $i=0$.

We begin with the stack automata $A^{1}_{\zeta},\ldots,A^{m}_{\zeta}$ which
each accept $\langle{p_{\zeta}},{w}\rangle$ for all stacks $w$. Note we can
vary these automata to accept any regular set of stacks we wish.

Thus, $A^{1}_{i},\ldots,A^{m}_{i}$ will characterise a possible set of stack
contents at the end of phase $i$. We show below how to construct
$A^{1}_{i-1},\ldots,A^{m}_{i-1}$ given $A^{1}_{i},\ldots,A^{m}_{i}$. This is
repeated until we have $A^{1}_{0},\ldots,A^{m}_{0}$. We then check, for each
$j$, that $\langle{p_{0}},{\perp_{n}}\rangle$ is accepted by $A^{j}_{0}$. This
is the case iff we have a positive instance of the reachability problem.

We construct $A^{1}_{i-1},\ldots,A^{m}_{i-1}$ from
$A^{1}_{i},\ldots,A^{m}_{i}$. For each $j\neq\iota_{i}$ we build $A^{j}_{i-1}$
by adding to $A^{j}_{i}$ a brand new set of initial states $q_{p}$ and a
guessed transition
$t_{j}={q_{p_{i-1}}}\xrightarrow[Q_{col}]{a}\left({{Q_{1},\ldots,Q_{n}}}\right)$
with $Q_{col},Q_{1},\ldots,Q_{n}$ being states of $A^{j}_{i}$ and
$q_{p_{i-1}}$ being one of the new states. The idea is $t_{j}$ will be the
initial transition accepting $\langle{p_{i-1}},{w}\rangle$ where $w$ is stack
$j$ at the beginning of phase $i$. By guessing an accompanying
$t^{\prime}_{j}$ of $A^{j}_{i}$ we can build
$\mathcal{T}^{A^{j}_{i}}_{{t_{j}},{t^{\prime}_{j}}}$ (by instantiating
Definition 3.2 (Transition Automata) with $A=A^{j}_{i}$, $t=t_{j}$ and
$t^{\prime}=t^{\prime}_{j}$) for which there will be an accepting run if the
updates to stack $j$ during phase $i$ are concordant with the introduction of
transition $t_{j}$.

Thus, for each $j\neq\iota_{i}$ we have $A^{j}_{i-1}$ and
$\mathcal{T}^{A^{j}_{i}}_{{t_{j}},{t^{\prime}_{j}}}$. We now consider the
$\iota_{i}$th stack. We build a CPDS $\mathcal{C}_{i}$ that accurately models
stack $\iota_{i}$ and tracks each
$\mathcal{T}^{A^{j}_{i}}_{{t_{j}},{t^{\prime}_{j}}}$ in its control state. We
ensure that $\mathcal{C}_{i}$ has a run from $\langle{p_{i-1}},{w}\rangle$ to
$\langle{p_{i}},{w^{\prime}}\rangle$ for some $w$ and $w^{\prime}$ iff there
is a corresponding run over the $\iota_{i}$th stack of $\mathcal{C}$ that
updates the remaining stacks $j$ in concordance with each guessed $t_{j}$.
Thus, we define $A^{\iota_{i}}_{i-1}$ to be the automaton recognising
${Pre^{*}_{\mathcal{C}_{i}}}\mathord{\left({A^{\iota_{i}}_{i}}\right)}$
constructed by saturation. The construction of $\mathcal{C}_{i}$ (given below)
follows the standard product construction of a CPDS with several finite-state
automata.

Note $\mathcal{C}_{i}$ is looking for a run from $p_{i-1}$ to $p_{i}$
concordant with runs of $t_{j}$ to $t^{\prime}_{j}$ for each $j$. To let
$\mathcal{C}_{i}$ start in $p_{i-1}$ and finish in $p_{i}$, we have an initial
transition from $p_{i-1}$ to $\left({p_{i-1},t_{1},\ldots,t_{m}}\right)$.
Thereafter, the components are updated as in a standard product construction.
When $\left({p_{i},t^{\prime}_{1},\ldots,t^{\prime}_{m}}\right)$ is reached,
there is a final transition to $p_{i}$. To ease notation, we use dummy
variables
$t_{\iota_{i}}=t^{\prime}_{\iota_{i}}=t^{\iota_{i}}=t^{\iota_{i}}_{1}$ for the
transition automaton component of the $\iota_{i}$th stack (for which we do not
have a $t$ and $t^{\prime}$ to track).

In the definition below, the first line of the definition of $\mathcal{R}^{i}$
gives the initial and final transitions, the second line models rules
operating on stack $\iota_{i}$, and the final line models generating
operations occurring on the $j$th stack for $j\neq\iota_{i}$.

######  Definition F.2 ($\mathcal{C}_{i}$)

Given for all $1\leq j\neq\iota_{i}\leq m$ a transition automaton
$\mathcal{T}_{j}=\mathcal{T}^{A^{j}_{i}}_{{t_{j}},{t^{\prime}_{j}}}$ and a
phase-bounded CPDS
$\mathcal{C}=\left({\mathcal{P},\Sigma,\mathcal{R}_{1},\ldots,\mathcal{R}_{m}}\right)$
and control states $p_{i-1}$, $p_{i}$, we define the CPDS
$\mathcal{C}_{i}=\left({\left\\{{p_{i-1},p_{i}}\right\\}\cup\mathcal{P}^{i},\mathcal{R}^{i},\Sigma}\right)$
where, letting
$t_{\iota_{i}}=t^{\prime}_{\iota_{i}}=t^{\iota_{i}}=t^{\iota_{i}}_{1}$ be
dummy transitions for technical convenience, and letting $t^{j}$ for all
$j\neq\iota_{i}$ range over all states of $\mathcal{T}_{j}$, we have

  * •

$\mathcal{P}^{i}$ contains all states $\left({p,t^{1},\ldots,t^{m}}\right)$
where $p\in\mathcal{P}$, and

  * •

the rules $\mathcal{R}^{i}$ of $\mathcal{C}_{i}$ are

$\begin{array}[]{l}\left\\{{\left({{p_{i-1}},{a},{noop},{\left({p_{i-1},t_{1},\ldots,t_{m}}\right)}}\right),\left({{\left({p_{i},t^{\prime}_{1},\ldots,t^{\prime}_{m}}\right)},{a},{noop},{p_{i}}}\right)}\
\left|\ {a\in\Sigma}\right.\right\\}\ \cup\\\
\left\\{{\left({{\left({p,t^{1},\ldots,t^{m}}\right)},{a},{o},{\left({p^{\prime},t^{1}_{1},\ldots,t^{m}_{1}}\right)}}\right)}\
\left|\
{\begin{array}[]{l}\left({{p},{a},{o},{p^{\prime}}}\right)\in\mathcal{R}_{\iota_{i}}\\\
\forall j^{\prime}\neq j\ .\
t^{j^{\prime}}\xrightarrow{\left({{p},{\\_},{noop},{p^{\prime}}}\right)}t^{j^{\prime}}_{1}\end{array}}\right.\right\\}\
\cup\\\ \left\\{{\left({{p_{1}},{a},{o},{p_{2}}}\right)}\ \left|\
{\begin{array}[]{c}p_{1}=\left({p,t^{1},\ldots,t^{j},\ldots
t^{m}}\right)\land\par\par
p_{2}=\left({p^{\prime},t^{1}_{1},\ldots,t^{j}_{1},\ldots t^{m}_{1}}\right)\\\
\land\ \left({{p},{b},{o},{p^{\prime}}}\right)\in\mathcal{R}_{j}\land\par
t^{j}\xrightarrow{\left({{p},{b},{o},{p^{\prime}}}\right)}t^{j}_{1}\ \land\\\
\forall j^{\prime}\neq j\ .\
t^{j^{\prime}}\xrightarrow{\left({p,\\_,noop,p^{\prime}}\right)}t^{j^{\prime}}_{1}\end{array}}\right.\right\\}\
.\end{array}$

We state the correctness of our reduction, deferring the proof to Appendix
F.2.

######  Lemma F.1 (Simulation of a PBCPDS)

Given a phase-bounded CPDS $\mathcal{C}$ control states $p_{0}$ and
$p_{\zeta}$, there is a run of $\mathcal{C}$ from
$\langle{p_{0}},{w_{1},\ldots,w_{m}}\rangle$ to
$\langle{p_{\zeta}},{w^{\prime}_{1},\ldots,w^{\prime}_{m}}\rangle$ iff for
each $1\leq j\leq m$, we have that $\langle{p_{0}},{w_{j}}\rangle$ is accepted
by $A^{j}_{0}$.

###  F.1 Global Reachability

$A^{1}_{0},\ldots,A^{m}_{0}$ were obtained by a finite sequence of non-
deterministic choices ranging over a finite number of values. Let $\chi$ be
the therefore finite set of tuples $\left({p_{0},A_{1},\ldots,A_{m}}\right)$
for each sequence as above, where $A_{i}$ is $A^{i}_{0}$ with initial state
$q_{p_{0}}$. From Lemma F.1, we have a regular solution to the global control
state reachability problem as required.

###  F.2 Proofs for Control-State Reachability

In this section we prove Lemma F.1 (Simulation of a PBCPDS) via Lemma F.2 and
Lemma F.3 below.

###### Lemma F.2

Given a phase-bounded CPDS $\mathcal{C}$ control states $p_{0}$ and
$p_{\zeta}$, there is a run of $\mathcal{C}$ from
$\langle{p_{0}},{w_{1},\ldots,w_{m}}\rangle$ to
$\langle{p_{\zeta}},{w^{\prime}_{1},\ldots,w^{\prime}_{m}}\rangle$ only if for
each $1\leq j\leq m$, we have that $\langle{p_{0}},{w_{j}}\rangle$ is accepted
by $A^{j}_{0}$.

_Proof._ Take a run of $\mathcal{C}$ from
$\langle{p_{0}},{w^{1}_{0},\ldots,w^{m}_{0}}\rangle$ to
$\langle{p_{\zeta}},{w^{1}_{\zeta},\ldots,w^{m}_{\zeta}}\rangle$ and split it
into phases $\sigma_{1}\ldots\sigma_{\zeta}$. Let $p_{i}$ be the control state
at the end of each $\sigma_{i}$, and $p_{0}$ be the control state at the
beginning of $\sigma_{1}$. Similarly, let $w^{j}_{i}$ be the stack contents of
stack $j$ at the end of $\sigma_{i}$. We include, for convenience, the
transition from the end of $\sigma_{i}$ to the beginning of $\sigma_{i+1}$ in
$\sigma_{i+1}$. Thus, the last configuration of $\sigma_{i}$ is also the first
configuration of $\sigma_{i+1}$.

We proceed by induction from $i=\zeta$ down to $i=1$. In the base case we know
by definition that $\langle{p_{\zeta}},{w^{j}_{\zeta}}\rangle$ is accepted by
$A^{j}_{\zeta}$.

Hence, assume $\langle{p_{i+1}},{w^{j}_{i+1}}\rangle$ is accepted by
$A^{j}_{i+1}$. We show the case for $i$. First consider $\iota_{i}$. Take the
run

$\langle{p_{i}},{w^{1}_{i},\ldots,w^{m}_{i}}\rangle\longrightarrow\cdots\longrightarrow\langle{p_{i+1}},{w^{1}_{i+1},\ldots,w^{m}_{i+1}}\rangle\
.$

We want to find a run

$\langle{p_{i}},{w^{\iota_{i}}_{i}}\rangle\longrightarrow\langle{\left({p_{i},t_{1},\ldots,t_{m}}\right)},{w^{\iota_{i}}_{i}}\rangle\longrightarrow\cdots\longrightarrow\langle{\left({p_{i+1},t^{\prime}_{1},\ldots,t^{\prime}_{m}}\right)},{w^{\iota_{i}}_{i+1}}\rangle\longrightarrow\langle{p_{1}},{w^{\iota_{i}}_{i+1}}\rangle$

of $\mathcal{C}_{i}$, giving us that
$\langle{p_{i}},{w^{\iota_{i}}_{i}}\rangle$ is accepted by
$A^{\iota_{i}}_{i}$. This is almost by definition, except we need to prove for
each $j\neq\iota_{i}$ that there is a sequence $t^{0},\ldots,t^{\ell}$ that is
also the projection of the run of $\mathcal{C}_{i}$ to the $(j+1)$th component
(that is, the state of the $j$th transition automaton). In particular, we
require $t^{0}=t_{j}$ and $t^{\ell}=t^{\prime}_{j}$. The proof proceeds in
exactly the same manner as the case of
$\left({{p},{a},{{\mathcal{L}_{g}}},{p^{\prime}}}\right)$ in the proof of
Lemma C.1 (Completeness of $\Pi$) for ECPDS. Namely, from the sequence of
operations $o^{0},\ldots,o^{\ell}$ taken from the run $t^{0},\ldots,t^{\ell}$,
we obtain a sequence of stacks such that at each $z$ there is an accepting run
of the $z$th stack constructed from $t^{z}$ and thereafter only transitions of
$A^{j}_{i+1}$. Thus, since $t_{j}$ is added to $A^{j}_{i+1}$ to obtain
$A^{j}_{i}$, we additionally get an accepting run of $A^{j}_{i}$ over
$\langle{p_{i}},{w^{j}_{i}}\rangle$. We do not repeat the arguments here.

Finally, then, when $i$ reaches $1$, we repeat the arguments above to conclude
$\langle{p_{0}},{w^{j}_{0}}\rangle$ is accepted by $A^{j}_{0}$ for each $j$,
giving the required lemma. $\square$

###### Lemma F.3

Given a phase-bounded CPDS $\mathcal{C}$ control states $p_{0}$ and
$p_{\zeta}$, there is a run of $\mathcal{C}$ from
$\langle{p_{0}},{w_{1},\ldots,w_{m}}\rangle$ to
$\langle{p_{\zeta}},{w^{\prime}_{1},\ldots,w^{\prime}_{m}}\rangle$ whenever
for each $1\leq j\leq m$, we have that $\langle{p_{0}},{w_{j}}\rangle$ is
accepted by $A^{j}_{0}$.

_Proof._ Assume for each $1\leq j\leq m$, we have that
$\langle{p_{0}},{w_{j}}\rangle$ is accepted by $A^{j}_{0}$.

Thus, we can inductively assume for each $j$ we have
$\langle{p_{i}},{w^{j}_{i}}\rangle$ accepted by $A^{j}_{i}$ and a run of
$\mathcal{C}$ of the form

$\langle{p_{0}},{w_{1},\ldots,w_{m}}\rangle\longrightarrow\cdots\longrightarrow\langle{p_{i}},{w^{1}_{i},\ldots,w^{m}_{i}}\rangle\
.$

Taking $w^{j}_{0}=w_{j}$ trivially gives us the base case. We prove the case
for $(i+1)$.

From the induction hypothesis, we have in particular that
$\langle{p_{i}},{w^{\iota_{i}}_{i}}\rangle$ is accepted by $A^{\iota_{i}}_{i}$
and hence we have a run of $\mathcal{C}_{i+1}$ of the form

$\langle{p_{i}},{w^{\iota_{i}}_{i}}\rangle\longrightarrow\langle{\left({p_{i},t_{1},\ldots,t_{m}}\right)},{w^{\iota_{i}}_{i}}\rangle\longrightarrow\cdots\longrightarrow\langle{\left({p_{i+1},t^{\prime}_{1},\ldots,t^{\prime}_{m}}\right)},{w^{\iota_{i}}_{i+1}}\rangle\longrightarrow\langle{p_{1}},{w^{\iota_{i}}_{i+1}}\rangle$

such that $\langle{p_{1}},{w^{\iota_{i}}_{i+1}}\rangle$ is accepted by
$A^{\iota_{i}}_{i+1}$. From this run, due to the definition of
$\mathcal{C}_{i}$ we can build a run

$\langle{p_{i}},{w^{1}_{i},\ldots,w^{m}_{i}}\rangle\longrightarrow\cdots\longrightarrow\langle{p_{i+1}},{w^{1}_{i+1},\ldots,w^{m}_{i+1}}\rangle$

of $\mathcal{C}$ where for all $j\neq\iota_{i}$, we define
$w^{j}_{i+1}={o^{\ell}}\mathord{\left({\cdots{o^{1}}\mathord{\left({w^{j}_{i}}\right)}}\right)}$
where

$\left({{p^{0}},{a^{1}},{o^{1}},{p^{1}}}\right)\left({{p^{1}},{a^{2}},{o^{2}},{p^{2}}}\right)\ldots\left({{p^{\ell-1}},{a^{\ell}},{o^{\ell}},{p^{\ell}}}\right)$

is the sequence of labels on the run of
$\mathcal{T}^{A^{j}_{i}}_{{t_{j}},{t^{\prime}_{j}}}$. We have to prove for all
$j\neq\iota_{i}$ that $\langle{p_{i+1}},{w^{j}_{i+1}}\rangle$ is accepted by
$A^{j}_{i+1}$. For the proof observe that the introduction of $t_{j}$ to
$A^{j}_{i+1}$ to form $A^{j}_{i}$ followed the saturation technique for
extended CPDS for a rule
$\left({{p_{i}},{a},{{\mathcal{L}_{g}}},{p_{i+1}}}\right)$ where
${\mathcal{L}_{g}}$ is the language of possible sequences of the form above.
Thus, from the soundness of the saturation method for extended CPDS, we have
that there must be the required run of $A^{j}_{i+1}$ over
$\langle{p_{i+1}},{w^{j}_{i+1}}\rangle$ beginning with transition
$t^{\prime}_{j}$.

Alternatively, we can argue similarly to the proof of Lemma C.1 (Completeness
of $\Pi$), but in the reverse direction. That is, we start with the
observation that the accepting run of $\langle{p_{i}},{w^{j}_{i}}\rangle$ uses
$t_{j}=t^{0}$ for the first transition, and thereafter only transitions from
$A^{j}_{i+1}$. We prove this by induction for the stack obtained by applying
$o^{1}$ and $t^{1}$, then for the stack obtained by applying $o^{2}$ and
$t^{2}$. This continues until we reach $w^{j}_{i+1}$, and since
$t^{\ell}=t^{\prime}_{j}$ with $t^{\prime}_{j}$ being a transition of
$A^{j}_{i+1}$, we get the accepting run we need. We remark that this is how
the soundness proof for the standard saturation algorithm would proceed if we
were able to assume that each new transition is only used at the head of any
new runs the transition introduces (but in general this is not the case
because new transitions may introduce loops). We leave the construction of
this proof as an exercise for the interested reader, for which they may follow
the proof of the extended rule case for Lemma C.5 (Soundness of $\Pi$).

Thus, finally, by induction, we obtain a run to
$\langle{p_{\zeta}},{w_{1},\ldots,w_{m}}\rangle$ such that
$\langle{p_{\zeta}},{w_{j}}\rangle$ is accepted by $A^{j}_{\zeta}$. $\square$

###  F.3 Complexity

Assume $n>1$. Our control state reachability algorithm requires
$2\uparrow_{\zeta(n-1)}\left({\ell}\right)$ time, where $\ell$ is polynomial
in the size of the PBCPDS. Beginning with phase $\zeta$, the saturation
algorithm can add at most
${\mathcal{O}}\mathord{\left({2\uparrow_{n-1}\left({\ell}\right)}\right)}$
transitions over the same number of iterations to
$A^{\iota_{\zeta}}_{\zeta-1}$. Thus we assume each $A^{j}_{i}$ to have at most
${\mathcal{O}}\mathord{\left({2\uparrow_{(\zeta-i)(n-1)}\left({\ell}\right)}\right)}$
transitions. The largest automaton $A^{j}_{i-1}$ construction is when
$j=\iota_{i}$. For this we build a CPDS with
${\mathcal{O}}\mathord{\left({2\uparrow_{(\zeta-i)(n-1)}\left({\ell}\right)}\right)}$
control states and thus $A^{\iota_{i}}_{i-1}$ has at most
${\mathcal{O}}\mathord{\left({2\uparrow_{(\zeta-i+1)(n-1)}\left({\ell}\right)}\right)}$
transitions. Hence, when $i=0$, we have at most
${\mathcal{O}}\mathord{\left({2\uparrow_{\zeta(n-1)}\left({\ell}\right)}\right)}$
transitions, which also gives the run time of the algorithm. This also implies
we have at most ${\mathcal{O}}\mathord{\left({2\uparrow_{\zeta
n}\left({\ell}\right)}\right)}$ tuples in the solution to the global
reachability problem.

##  Appendix G Proofs for Scope-Bounded CPDS

###  G.1 Operations on Layer Automata

#### Shift of a Layer Automaton

The idea behind Shift is that all transitions in layer $i$ are moved up to
layer $(i+1)$ and transitions involving states in layer $\zeta$ are removed.
Intuitively this is because the stack elements in layer $\zeta$ will “go out
of scope” when the context switch corresponding to the Shift occurs. In more
detail, states of layer $i$ are renamed to become states of layer $(i+1)$,
with all states of layer $\zeta$ being deleted. Similarly, all transitions
that involved a layer $\zeta$ state are also removed.

We define ${\text{\tt Shift}}\mathord{\left({A}\right)}$ of an order-$n$
$\zeta$-layer stack automaton

$A=\left({\mathbb{Q}_{n},\ldots,\mathbb{Q}_{1},\Sigma,\Delta_{n},\ldots,\Delta_{1},\emptyset,\ldots,\emptyset}\right)$

to be

$A^{\prime}=\left({\mathbb{Q}^{\prime}_{n},\ldots,\mathbb{Q}^{\prime}_{1},\Sigma,\Delta^{\prime}_{n},\ldots,\Delta^{\prime}_{1},\emptyset,\ldots,\emptyset}\right)$

where defining

${\text{\tt Shift}}\mathord{\left({q}\right)}=\begin{cases}q&\text{if
$q\in\mathbb{Q}_{k}$, $n>k$ and $q$ is layer $i<\zeta$}\\\
q_{p}^{i+1}&\text{if $q=q_{p}^{i}\in\mathbb{Q}_{n}$ and $i<\zeta$}\\\
\text{undefined}&\text{otherwise}\end{cases}$

and extending Shift point-wise to sets of states, we have

$\Delta^{\prime}_{n}=\left\\{{{\text{\tt
Shift}}\mathord{\left({q}\right)}\xrightarrow{q^{\prime}}{\text{\tt
Shift}}\mathord{\left({Q}\right)}}\ \left|\
{q\xrightarrow{q^{\prime}}Q\in\Delta_{n}\text{ and $q$ is layer
$i<\zeta$}}\right.\right\\}$

and for all $n>k>1$

$\Delta^{\prime}_{k}=\left\\{{q\xrightarrow{q^{\prime}}{\text{\tt
Shift}}\mathord{\left({Q}\right)}}\ \left|\
{q\xrightarrow{q^{\prime}}Q\in\Delta_{k}\text{ and $q$ is layer
$i<\zeta$}}\right.\right\\}$

and

$\Delta^{\prime}_{1}=\left\\{{q\xrightarrow[{\text{\tt
Shift}}\mathord{\left({Q_{col}}\right)}]{q^{\prime}}{\text{\tt
Shift}}\mathord{\left({Q}\right)}}\ \left|\
{q\xrightarrow[Q_{col}]{q^{\prime}}Q\in\Delta_{1}\text{ and $q$ is layer
$i<\zeta$}}\right.\right\\}\ .$

In all cases above, transitions are only created if the applications of Shift
result in a defined state or set of states. This operation will erase all
layer $\zeta$ states, and all transitions that go to a layer $\zeta$ state.