C Broadbent

A Carayol

M Hague

O Serre

A Saturation Method for Collapsible Pushdown Systems ⋆

We introduce a natural extension of collapsible pushdown systems called annotated pushdown systems that replaces collapse links with stack annotations. We believe this new model has many advantages. We present a saturation method for global backwards reachability analysis of these models that can also be used to analyse collapsible pushdown systems. Beginning with an automaton representing a set of configurations, we build an automaton accepting all configurations that can reach this set. We also improve upon previous saturation techniques for higher-order pushdown systems by significantly reducing the size of the automaton constructed and simplifying the algorithm and proofs.

Introduction

Via languages such as C ++ , Haskell, Javascript, Python, or Scala, modern day programming increasingly embraces higher-order procedure calls. This is a challenge for software verification, which usually does not model recursion accurately, or models only first-order calls (e.g. SLAM [START_REF] Ball | The SLAM project: Debugging system software via static analysis[END_REF] and Moped [START_REF] Schwoon | Model-checking Pushdown Systems[END_REF]). Collapsible pushdown systems (collapsible PDS) are an automaton model of (higher-order recursion) schemes [START_REF] Damm | The IO-and OI-hierarchies[END_REF][START_REF] Ong | On model-checking trees generated by higher-order recursion schemes[END_REF], which allow reasoning about higher-order recursion.

Collapsible pushdown systems are a generalisation of higher-order pushdown systems (higher-order PDS). Higher-order PDS provide a model of schemes subject to a technical constraint called safety [START_REF] Maslov | Multilevel stack automata[END_REF][START_REF] Knapik | Higher-order pushdown trees are easy[END_REF] and are closely related to the Caucal hierarchy [START_REF] Carayol | The caucal hierarchy of infinite graphs in terms of logic and higher-order pushdown automata[END_REF]. These systems extend the stack of a pushdown system to allow a nested "stack-of-stacks" structure. Recently it has been shown by Parys that safety is a genuine constraint on definable traces [START_REF] Parys | Collapse operation increases expressive power of deterministic higher order pushdown automata[END_REF]. Hence, to model higher-order recursion fully, we require collapsible PDS, which -using an idea from panic automata [START_REF] Knapik | Unsafe grammars and panic automata[END_REF] -add additional collapse links to the stack structure. These links allow the automaton to return to the context in which a character was added to the stack.

These formalisms are known to have good model-checking properties. For example, it is decidable whether a given µ-calculus formula holds on the execution graph of a scheme [START_REF] Ong | On model-checking trees generated by higher-order recursion schemes[END_REF] (or collapsible PDS [START_REF] Hague | Collapsible pushdown automata and recursion schemes[END_REF]). Although, the complexity of such analyses is high -for an order-n collapsible PDS, reachability checking is complete for (n -1)-EXPTIME, while µ-calculus is complete for n-EXPTIME -the problem becomes PTIME if the arity of the recursion scheme, and the number of alternations in the formula, is bounded. The same holds true for collapsible PDS when the number of control states is bounded. Furthermore, when translating from a scheme to a collapsible PDS, it is the arity that determines the number of control states [START_REF] Hague | Collapsible pushdown automata and recursion schemes[END_REF]. It has been shown by Kobayashi [21] that these analyses can be performed in practice. For example, resource usage properties of programs of orders up to five can be verified in a matter of seconds.

Kobayashi et al.'s approach uses intersection types. In the order-1 case, an alternative approach called saturation has been successfully implemented by tools such as Moped [START_REF] Schwoon | Model-checking Pushdown Systems[END_REF] and PDSolver [START_REF] Hague | Analysing mu-calculus properties of pushdown systems[END_REF]. Saturation techniques begin with a small automaton -representing a set of configurations -and add new transitions as they become necessary until a fixed point is reached. These algorithms, then, naturally do not pay the worst case complexity immediately, and hence, represent ideal algorithms for efficient verification. Furthermore, they also provide a solution to the global model checking problem: that is, determining the set of all system states that satisfy a property. This is particularly useful when, for example, composing analyses. Furthermore, when testing reachability from a given initial state, we may terminate the analysis as soon as this state is found. That is, we do not need to compute the whole fixed point.

Our first contribution is a new model of higher-order execution called annotated pushdown systems (annotated PDS) 1 , which replace the collapse links of a collapsible PDS with annotations containing the stack the link pointed to. In addition to allowing a more straightforward definition of regularity and greatly simplifying the proofs of the paper, this model provides a more natural handling of collapse links, highlighting their connection with closures. In addition, configuration graphs of this model are isomorphic to those of collapsible PDS when restricted to configurations reachable from the initial configuration.

Our second contribution is a saturation method for backwards reachability analysis of annotated pushdown systems that can also be applied as-is to collapsible PDS. This is a global model-checking algorithm that is based on saturation techniques for higher-order pushdown automata [START_REF] Bouajjani | Symbolic Reachability Analysis of Higher-Order Context-Free Processes[END_REF][START_REF] Hague | Symbolic backwards-reachability analysis for higherorder pushdown systems[END_REF][START_REF] Seth | An alternative construction in symbolic reachability analysis of second order pushdown systems[END_REF]. Our algorithm handles alternating (or "two-player") as well as non-alternating systems.

In addition to the extension to annotated pushdown systems, the algorithm improves on Hague and Ong's construction for higher-order pushdown systems [START_REF] Hague | Symbolic backwards-reachability analysis for higherorder pushdown systems[END_REF] since the number of states introduced by the construction is no longer multiplied by the number of iterations it takes to reach a fixed point, potentially leading to a large reduction in the size of the automata constructed. In addition, both the presentation and the proofs of correctness are much less involved.

Related Work

In addition to the works mentioned above, solutions to global model checking problems have been proposed by Broadbent et al. [START_REF] Broadbent | Recursion schemes and logical reflection[END_REF]. Additionally, Salvati and Walukiewicz provide a global analysis technique for µ-calculus properties using a Krivine machine model of schemes [START_REF] Salvati | Krivine machines and higher-order schemes[END_REF]. However, there are currently no versions of these algorithms available that do not pay immediately the exponential blow up.

Extensions of schemes with pattern matching have also been considered by Ong and Ramsay [START_REF] Ong | Verifying higher-order functional programs with pattern-matching algebraic data types[END_REF]. A recent algorithm by Kobayashi speeds up his techniques using an over-approximating least fixed point computation to give an initial input to a greatest fixed point computation [START_REF] Kobayashi | A practical linear time algorithm for trivial automata model checking of higher-order recursion schemes[END_REF]. Like saturation this is a 'bottomup' approach and it would be interesting to see whether there are connections. Extensions of higher-order PDS to concurrent settings have also been considered by Seth [START_REF] Seth | Games on higher order multi-stack pushdown systems[END_REF].

The saturation technique has proved popular in the literature. It was introduced by Bouajjani et al. [START_REF] Bouajjani | Reachability analysis of pushdown automata: Application to model-checking[END_REF] and Finkel et al. [START_REF] Finkel | A direct symbolic approach to model checking pushdown systems[END_REF] and based on a string rewriting algorithm by Benois [START_REF] Benois | Parties rationnelles du groupe libre[END_REF]. It has since been extended to Büchi games [START_REF] Cachat | Games on Pushdown Graphs and Extensions[END_REF], parity and µ-calculus conditions [START_REF] Hague | Analysing mu-calculus properties of pushdown systems[END_REF], and concurrent systems [START_REF] Suwimonteerabuth | Symbolic context-bounded analysis of multithreaded java programs[END_REF][START_REF] Atig | Global model checking of ordered multi-pushdown systems[END_REF], as well as weighted pushdown systems [START_REF] Reps | Weighted pushdown systems and their application to interprocedural dataflow analysis[END_REF]. In addition to various implementations, efficient versions of these algorithms have also been developed [START_REF] Esparza | Efficient algorithms for model checking pushdown systems[END_REF][START_REF] Suwimonteerabuth | Efficient algorithms for alternating pushdown systems with an application to the computation of certificate chains[END_REF].

Preliminaries

Annotated Pushdown Systems

We define annotated stacks, their operations, and annotated pushdown systems.

Annotated stacks Let Σ be a set of stack symbols. We define a notion of annotated higher-order stack. Intuitively, an annotated stack of order-n is an order-n stack in which stack symbols have attached annotated stacks of order at most n. For the rest of the formal definitions, we fix the maximal order to n, and use k to range between n and 1. We simultaneously define for all 1 ≤ k ≤ n, the set Stacks n k of stacks of order-k whose symbols are annotated by stacks of order at most n. Note, we use subscripts to indicate the order of a stack.

Definition 1 (Annotated Stacks). The family of sets (Stacks n k ) 1≤k≤n is the smallest family (for point-wise inclusion) such that:

-for all 2 ≤ k ≤ n, Stacks n k is the set of all (possibly empty) sequences [w 1 . . . w ℓ ] k with w 1 , . . . , w ℓ ∈ Stacks n k-1 . -Stacks n
1 is all sequences [a 1 w1 . . . a ℓ w ℓ ] 1 with ℓ ≥ 0 and for all 1 ≤ i ≤ ℓ, a i is a stack symbol in Σ and w i is an annotated stack in 1≤k≤n Stacks n k .

Observe that the above definition uses a least fixed-point. This ensures that all stacks are finite; in particular a stack cannot contain itself as an annotation. When the maximal order n is clear, we simply write Stacks k instead of Stacks n k . We also write order-k stack to designate an annotated stack in Stacks n k . An order-n stack can be represented naturally as an edge-labelled tree over the alphabet {[ n-1 , . . . , [ 1 , ] 1 , . . . , ] n-1 } ⊎ Σ, with Σ-labelled edges having a second target to the tree representing the annotation. For technical convenience, a tree representing an order-k stack does not use [ k or ] k symbols (these appear uniquely at the beginning and end of the stack). An example order-3 stack is given below, with only a few annotations shown. The annotations are order-3 and order-2 respectively.

• • • • • • • • • • • • • • • • • [ 2 [ 1 a b ] 1 ] 2 [ 2 [ 1 c ] 1 ] 2 [ 1 d ] 1
Given an order-n stack w = [w 1 . . . w ℓ ] n , we define top n+1 (w) = w and

top n ([w 1 . . . w ℓ ] n ) = w 1 when ℓ > 0 top n ([] n ) = [] n-1 otherwise top k ([w 1 . . . w ℓ ] n ) = top k (w 1 ) when k < n and ℓ > 0 noting that top k (w) is undefined if top k ′ (w) is empty for any k ′ > 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 . . . v ℓ ] k then u : k v = [uv 1 . . . v ℓ ] k , and if v = [v 1 . . . v ℓ ] k ′ with k ′ > k, u : k v = [u : k v 1 , . . . , v ℓ ] k ′ .
This composition associates to the right. For example, the order-3 stack above can be written [[[a w b] 1 ] 2 ] 3 and also 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 Annotated Stacks

The following operations can be performed on an order-n stack. We say o ∈ O n is of order-k when k is minimal such that o ∈ O k . For example, push k is of order k.

O n = {pop 1 , . . . , pop n } ∪ {push 2 , . . . , push n } ∪ {collapse 2 , . . . , collapse n } ∪ push 1 a , . . . , push n a , rew a | a ∈ Σ We define each stack operation for an order-n stack w. Annotations are created by push k a , which add a character to the top of a given stack w annotated by top k+1 (pop k (w)). This gives a access to the context in which it was created. In Section 3.2 we give several examples of these operations.

We set pop

k (u : k v) = v. 2. We set push k (u : k v) = u : k u : k v. 3. We set collapse k a u ′ : 1 u : (k+1) v = u ′ : (k+1) v when u is order-k and n > k ≥ 1; and collapse n (a u : 1 v) = u when u is order-n. 4. We set push k b (w) = b u : 1 w where u = top k+1 (pop k (w)). 5. We set rew b (a u : 1 v) = b u : 1 v.

Annotated Pushdown Systems

We are now ready to define annotated PDS.

Definition 2 (Annotated Pushdown Systems

). An order-n alternating annotated pushdown system (annotated PDS) is a tuple C = (P, Σ, R) where P is a finite set of control states, Σ is a finite stack alphabet, and R ⊆ (P × Σ × O n × P)∪ P × 2 P is a set of rules.

We write configurations of an annotated PDS as a pair p, w where p ∈ P and w ∈ Stacks n . We write p, w -→ p ′ , w ′ to denote a transition from a rule (p, a, o, p ′ ) with top 1 (w) = a and w ′ = o(w). Furthermore, we have a transition p, w -→ { p ′ , w | p ′ ∈ P } whenever we have a rule p → P . A non-alternating annotated PDS has no rules of this second form. We write C to denote a set of configurations.

Collapsible Pushdown Systems Annotated pushdown systems are based on collapsible PDS. In this model, stacks do not contain order-k annotations, rather they have order-k links to an order-k stack occurring lower down in the top-most order-(k + 1) stack. We define the model formally in the appendix. We give an example below, where links are marked with their order.

• • • • • • • • • • • • • • • • [ 2 [ 1 a 3 b ] 1 ] 2 [ 2 [ 1 c 2 ] 1 [ 1 d 1 e ] 1 ] 2
The set O n is the same as in the annotated version. Collapse links are created by the push k a operation, which augments a with a link to pop k of the stack being pushed onto. A collapse k returns to the stack that is the target of the link.

Collapsible vs. Annotated To an order-n stack w with links, we associate a canonical annotated stack [[ w ]] where each link is replaced by the annotated version of the link's target. We inductively and simultaneously define [[ w ]] k which is the annotated stack representing top k (w).

   [[ [ ] k : k+1 v ]] k = [ ] k [[ u : k ′ +1 v ]] k = [[ u ]] k ′ : k ′ +1 [[ v ]] k where 0 < k ′ < k [[ a * : 1 v ]] k = a [[ collapse k ′ (a * :1v) ]] k ′ : 1 [[ v ]]
k where a * is a with an order-k ′ link For example, the order-

3 stack above becomes [[[a w1 b] 1 ] 2 [[c w2 ] 1 [d w3 e] 1 ] 2 ] 3 where w 1 = [[[c w2 ] 1 [d w3 e] 1 ] 2 ] 3 , w 2 = [[d w3 e] 1 ] 2 and w 3 = [e] 1 .
Note that some annotated stacks such as

[[a w ] 1 ] 2 with w = [[b []1
] 1 ] 2 do not correspond to any stacks with links. However for all order-n stacks with links w and for any operation o of order at most n, we have [[ o(w)

]] = o([[ w ]]).
Remark 1. The configuration graphs of annotated pushdown systems of order-n are isomorphic to their collapsible counter-part when restricted to configurations reachable from the initial configuration. This implies annotated pushdown automata generate the same trees as higher-order recursion schemes, as in [START_REF] Broadbent | Recursion schemes and logical reflection[END_REF].

Regularity of Annotated Stacks

We will present an algorithm that operates on sets of configurations. For this we use order-n stack automata, thus defining a notion of regular sets of stacks. These have a nested structure based on a similar automata model by Bouajjani and Meyer [START_REF] Bouajjani | Symbolic Reachability Analysis of Higher-Order Context-Free Processes[END_REF]. The handling of annotations is similar to automata introduced by Broadbent et al. [START_REF] Broadbent | Recursion schemes and logical reflection[END_REF], except we read stacks top-down rather than bottom-up.

Definition 3 (Order-n Stack Automata). An order-n stack automaton

A = (Q n , . . . , Q 1 , Σ, ∆ n , . . . , ∆ 1 , F n , . . . , F 1 )
is a tuple where Σ is a finite stack alphabet, and

1. for all n ≥ k ≥ 2, we have Q k is a finite set of states, ∆ k ⊆ Q k × Q k-1 × 2 Q k is a transition relation, and F k ⊆ Q k is a set of accepting states, and 2. Q 1 is a finite set of states, ∆ 1 ⊆ 2≤k≤n Q 1 × Σ × 2 Q k × 2 Q1 a transition relation, and F 1 ⊆ Q 1 a set of accepting states.
Stack automata are alternating automata that read the stack in a nested fashion. Order-k stacks are recognised from states in Q k . A transition (q, q ′ , Q) ∈ ∆ k from q to Q for some k > 1 can be fired when the top k-1 stack is accepted from q ′ ∈ Q (k-1) . The remainder of the stack must be accepted from all states in Q. At order-1, a transition (q, a, Q br , Q) is a standard alternating a-transition with the additional requirement that the stack annotating a is accepted from all states in Q br . A stack is accepted if a subset of F k is reached at the end of each order-k stack. In the appendix, we formally define the runs of a stack automaton. We write w ∈ L q (A) whenever w is accepted from a state q.

A (partial) run is pictured below, using

q 3 q2 -→ Q 3 ∈ ∆ 3 , q 2 q1 -→ Q 2 ∈ ∆ 2 and q 1 a --→ Q br Q 1 ∈ ∆ 1 .
The node labelled Q br begins a run on the stack annotating a.

q 3 q 2 q 1 Q 1 • • • Q 2 • • • Q 3 • • • Q br • • • [ 2 [ 1 a • • • ] 1 • • • ] 2 • • • • • • Remark 2.
In the appendix, we show several results on stack automata: membership testing is linear time; emptiness is PSPACE-complete; the sets of stacks accepted by these automata form an effective Boolean algebra (note that complementation causes a blow-up in the size of the automaton); and they accept the same family of collapsible stacks as the automata used by Broadbent et al. [START_REF] Broadbent | Recursion schemes and logical reflection[END_REF].

Algorithm

Given an annotated PDS C and a stack automaton A 0 with a state q p ∈ Q n for each control state p in C, we define P re * C (A 0 ) as the smallest set such that P re * C (A 0 ) ⊇ p, w w ∈ L qp (A 0 ) , and

P re * C (A 0 ) ⊇ p, w ∃ p, w -→ p ′ , w ′ with p ′ , w ′ ∈ P re * C (A 0 ) ∨ ∃ p, w -→ C and C ⊆ P re * C (A 0 )
recalling that C denotes a set of configurations. We build a stack automaton recognising P re * C (A 0 ). We begin with A 0 and iterate a saturation function denoted Γ -which adds new transitions to A 0 -until a 'fixed point' has been reached. That is, we iterate A i+1 = Γ (A i ) until A i+1 = A i . As the number of states is bounded, we eventually obtain this, giving us the following theorem.

Theorem 1. Given an alternating annotated pushdown system C and a stack automaton A 0 , we can construct an automaton A accepting P re * C (A 0 ).

The construction runs in n-EXPTIME for both alternating annotated PDS and collapsible PDS -which is optimal -and can be improved to (n -1)-EXPTIME for non-alternating collapsible PDS when the initial automaton satisfies a certain notion of non-alternation, again optimal. Correctness and complexity are discussed in subsequent sections.

Notation and Conventions

Number of Transitions

We assume for all q ∈ Q k and Q ⊆ Q k that there is at most one transition of the form q q ′ -→ Q ∈ ∆ k . This condition can easily be ensured on A 0 by replacing pairs of transitions q q1 -→ Q and q q2 -→ Q with a single transition q q ′ -→ Q, where q ′ accepts the union of the languages of stacks accepted from q 1 and q 2 . The construction maintains this condition.

Short-form Notation

We introduce some short-form notation for runs. Consider the example run in Section 2.2. In this case, we write q 3 a --→

Q br (Q 1 , Q 2 , Q 3 ), q 3 q1 -→ (Q 2 , Q 3 ), and q 3 q2 -→ (Q 3 ). In general, we write q a --→ Q br (Q 1 , . . . , Q k ) and q q ′ -→ (Q k ′ +1 , . . . , Q k ) .
In the first case, q ∈ Q k and there exist q k-1 , . . . , q 1 such that q

q k-1 ---→ Q k ∈ ∆ k , q k-1 q k-2 ---→ Q k-1 ∈ ∆ k-1 , . . . , q 1 a --→ Q br Q 1 ∈ ∆ 1 .
Thus, we capture nested sequences of initial transitions from q. Since we assume at most one transition between any state and set of states, the intermediate states q k-1 , . . . , q 1 are uniquely determined by q, a, Q br and Q 1 , . . . , Q k .

In the second case q ∈ Q k , q ′ ∈ Q k ′ , and there exist q k-1 , . . . , q k ′ +1 with q

q k-1 ---→ Q k ∈ ∆ k , q k-1 q k-2 ---→ Q k-1 ∈ ∆ k-1 , . . . , q k ′ +2 q k ′ +1 ---→ Q k ′ +2 ∈ ∆ k ′ +2 and q k ′ +1 q ′ -→ Q k ′ +1 ∈ ∆ k ′ +1 .
We lift the short-form transition notation to transitions from sets of states. We assume that state-sets Q n , . . . , Q 1 are disjoint. Suppose Q = {q 1 , . . . , q ℓ } and for all 1 ≤ i ≤ ℓ we have q i a --→

Q i br Q i 1 , . . . , Q i k . Then we have Q a --→ Q br (Q 1 , . . . , Q k ) where Q br = 1≤i≤ℓ Q i br and for all k, Q k = 1≤i≤ℓ Q i k .
Because an annotation can only be of one order, we insist that Q br ⊆ Q k for some k.

Finally, we remark that a transition to the empty set is distinct from having no transition.

Initial States

We say a state is initial if it is of the form q p ∈ Q n for some control state p or if it is a state q k ∈ Q k for k < n such that there exists a transition q k+1 q k -→ Q k+1 in ∆ k+1 . We make the assumption that all initial states do not have any incoming transitions and that they are not final 2Adding Transitions Finally, when we add a transition q a --→

Q br (Q 1 , . . . , Q n )
to the automaton, then for each n ≥ k > 1, we add q k q k-1 ---→ Q k to ∆ k (if a transition between q k and Q k does not already exist, otherwise we use the existing transition and state q k-1 ) and add q 1 a --→

Q br Q 1 to ∆ 1 .

The Saturation Function

Given an annotated PDS C = (P, Σ, R), we define the saturation function. Examples can be found below.

Definition 4 (The Saturation Function Γ ). Given an order-n stack automaton A we define

A ′ = Γ (A) such that A ′ is A plus, for each (p, a, o, p ′ ) ∈ R, 1. when o = pop k , for each q p ′ q k -→ (Q k+1 , . . . , Q n ) in A, add to A ′ q p a -→ ∅ (∅, . . . , ∅, {q k } , Q k+1 , . . . , Q n ) , 2. when o = push k , for all transitions q p ′ a --→ Q br (Q 1 , . . . , Q k , . . . , Q n ) and Q k a --→ Q ′ br (Q ′ 1 , . . . , Q ′ k ) in A, add to A ′ the transition q p a ------→ Q br ∪Q ′ br Q 1 ∪ Q ′ 1 , . . . , Q k-1 ∪ Q ′ k-1 , Q ′ k , Q k+1 , . . . , Q n , 3. when o = collapse k , when k = n, add q p a ----→ {q p ′ } (∅, .
. . , ∅), and when k < n,

for each transition q p ′ q k -→ (Q k+1 , . . . , Q n ) in A, add to A ′ the transition q p a ---→ {q k } (∅, . . . , ∅, Q k+1 , . . . , Q n ) , 4. when o = push k b for all transitions q p ′ b --→ Q br (Q 1 , . . . , Q n ) and Q 1 a --→ Q ′ br Q ′ 1 in A with Q br ⊆ Q k , add to A ′ the transition q p a --→ Q ′ br (Q ′ 1 , Q 2 , . . . , Q k ∪ Q br , . . . , Q n ) , 5. when o = rew b for each transition q p ′ b --→ Q br (Q 1 , . . . , Q n ) in A, add to A ′ the transition q p a --→ Q br (Q 1 , . . . , Q n ).
Finally, for every rule p → P , let

Q = { q p ′ | p ′ ∈ P }, then, for each Q a --→ Q br (Q 1 , . . . , Q n ), add a transition q p a --→ Q br (Q 1 , . . . , Q n ).
For convenience, the statesets of A ′ are defined implicitly from the states used in the transition relations.

Examples All examples except one use the order-2 stack w ′ , labelled by a run of a stack automaton, pictured below, where the sub-script indicates states in

Q 1 or Q 2 .
Recall that the first transition of the run can be written

q p ′ a --→ Q 2 br Q 1 1 , Q 1 2 . q p ′ q 1 Q 1 1 Q 1 2 Q 3 1 Q 4 1 Q 2 2 Q 1 br • • • Q 2 br • • • [ 1 a ] 1 [ 1 a ] 1 [ 1 [ 1
Example of (p, a, pop 2 , p ′ ) Consider the stack w pictured below with pop 2 (w) = w ′ . By the construction, we add a transition q p a -→ ∅ (∅, {q p ′ }) giving the run below labelling w, where q ′ 1 is the state labelling the new transition

q p ′ q ′ 1 -→ {q p ′ }. q p q ′ 1 ∅ ∅ q p ′ q 1 Q 1 1 Q 1 2 • • • Q 1 br • • • [ 1 a c ] 1 [ 1 a ] 1 [ 1 [ 1 Example of (p, a, push 2 , p ′ ) Consider the stack w below with push 2 (w) = w ′ . Take Q 1 2 a --→ Q 1 br Q 4 1 , Q 2 2 from the node labelled Q 1 2 in the run over w ′ . By the construction, we add q p a ------→ Q 1 br ∪Q 2 br Q 1 1 ∪ Q 4 1 , Q 2 2
and obtain a run over w

q p q ′ 1 Q 1 1 ∪ Q 4 1 Q 2 2 Q 1 br ∪ Q 2 br • • • . [ 1 a ] 1 [ 1
where q ′ 1 is the state used by the new transition. This run combines the runs over the top two order-1 stacks of w ′ , ensuring any stack accepted could appear twice on top of a stack already accepted. That is, push

2 (w) = w ′ is in P re * C (A 0 ).
Example of (p, a, collapse 2 , p ′ ) Consider the stack w below with collapse 2 (w) = w ′ . By the construction, we add a transition q p a ----→ {q p ′ } (∅, ∅); hence, we have the run below, where q ′ 1 is the state labelling the new transition q p ′ q ′ 1 -→ {∅}.

q p q ′ 1 ∅ ∅ ∅ ∅ ∅ q p ′ q 1 Q 1 1 Q 1 2 • • • Q 1 br • • • [ 1 a ] 1 [ 1 c ] 1 [ 1 a ] 1 [ 1 [ 1
Example of p, a, push 2 b , p ′ The stack of our running example is not constructible via a push 2 b operation. Hence, we use the following stack and run for w ′

q p ′ q 1 Q 1 1 Q 2 1 Q 1 2 Q 3 1 Q 4 1 Q 2 2 Q br Q 5 1 Q 6 1 Q 3 2 [ 1 b a ] 1 [ 1 a ] 1 [ 1 a ] 1 with q p ′ b --→ Q br Q 1 1 , Q 1 2 and Q 1 1 a -→ ∅ Q 2 1 . The construction adds q p a -→ ∅ Q 2 1 , Q 1 2 ∪ Q br .
This gives us a run on the stack w such that push 2 b (w) = w ′ , where q ′ 1 is the order-1 state labelling the new order-2 transition.

q p ′ q ′ 1 Q 2 1 Q 1 2 ∪ Q br Q 3 1 ∪ Q 5 1 Q 4 1 ∪ Q 6 1 Q 2 2 ∪ Q 3 2 [ 1 a ] 1 [ 1 a ] 1 4

Correctness and Complexity

Theorem 2. For a given C and A 0 , let A = A i where i is the least index such that

A i+1 = Γ (A i ). We have w ∈ L qp (A) iff p, w ∈ P re * C (A 0 ).
The proof is in the appendix. Completeness is by a straightforward induction over the "distance" to A 0 . Soundness is the key technical challenge. The idea is to 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 ∈ Q k , which is denoted w |= q.

Definition 5 (w |= q). For any Q ⊆ Q k and any order-k stack w, we write w |= Q if w |= q for all q ∈ Q, and we define w |= q by a case distinction on q.

1. q is an initial state in Q n . Then for any order-n stack w, we say that w |= q if q, w ∈ P re * C (A 0 ). 2. q is an initial state in Q k , labeling a transition q k+1 q -→ Q k+1 ∈ ∆ k+1 . Then for any order-k stack w, we say that w |= q if for all order-(k

+ 1) stacks v s.t. v |= Q k+1 , then w : (k+1) v |= q k+1 . 3. q is a non-initial state in Q k .
Then for any order-k stack w, we say that w |= q if A 0 accepts w from q.

We show the automaton constructed is sound with respect to this meaning. That is, for all q k a --→

Q br (Q 1 , . . . , Q k ),
we can place a u , for any u |= Q br , on top of any stack satisfying Q 1 , . . . , Q k and obtain a stack that satisfies q k . By induction over the length of the stack, this property extends to complete stacks. That is, a stack is accepted from a state only if it is in its meaning. Since states q p are assigned their meaning in P re * C (A 0 ), we obtain soundness of the construction. The construction is also sound for collapsible stacks. That is, p, w belongs to P re * C (A 0 ) where C is a collapsible PDS and A 0 accepts collapsible stacks iff p, [[ w ]] n belongs to P re * C (A 0 ) where C and A 0 are interpreted over annotated stacks. This is due to the commutativity of [[ o(w)

]] = o([[ w ]]).
Proposition 1. The saturation construction for an alternating order-n annotated PDS C and an order-n stack automaton A 0 runs in n-EXPTIME, which is optimal.

Proof. Let 2 ↑ 0 ℓ = ℓ and 2 ↑ i+1 ℓ = 2 2↑iℓ . The number of states of A is bounded by 2 ↑ (n-1) ℓ where ℓ is the size of C and A 0 : each state in Q k was either in A 0 or comes from a transition in ∆ 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 ↑ n ℓ transitions can be added. Since the reachability problem for alternating higher-order pushdown systems is complete for n-EXPTIME [START_REF] Hague | Symbolic backwards-reachability analysis for higherorder pushdown systems[END_REF], our algorithm is optimal.

It is known that the complexity of reachability for non-alternating collapsible PDS is in (n -1)-EXPTIME. The cause of the additional exponential blow up is in the alternation of the stack automata. In the appendix we show that, for a suitable notion of non-alternating stack automata, our algorithm can be adapted to run in (n -1)-EXPTIME, when the collapsible PDS is also non-alternating.

Furthermore, the algorithm is PTIME for a fixed order and number of control states. If we obtained C from a scheme, the number of control states is given by the arity of the scheme [START_REF] Hague | Collapsible pushdown automata and recursion schemes[END_REF]. Since the arity and order are expected to be small, we are hopeful that our algorithm will perform well in practice.

Perspectives

There are several avenues of future work. First, we intend to generalise our saturation technique to computing winning regions of parity conditions, based on the order-1 case [START_REF] Hague | A saturation method for the modal µ-calculus over pushdown systems[END_REF]. This will permit verification of more general specifications. We also plan to design a prototype tool to test the algorithm in practice An important direction is that of counter example generation. When checking safety property, it is desirable to provide a trace witnessing a violation of the property. This can be used to repair the bug and as part of a counter-example guided abstraction refinement (CEGAR) loop enabling efficient verification algorithms. However, finding shortest counter examples -due to its tight connection with pumping lemmas -will present a challenging and interesting problem.

Saturation techniques have been extended to concurrent order-1 pushdown systems [START_REF] Suwimonteerabuth | Symbolic context-bounded analysis of multithreaded java programs[END_REF][START_REF] Atig | Global model checking of ordered multi-pushdown systems[END_REF]; concurrency at higher-orders would be interesting.

It will also be interesting to study notions of regularity of annotated stacks. In our notion of regularity, the forwards reachability set is not regular, due to the copy operation push k . This problem was addressed by Carayol for higher-order stacks [START_REF] Carayol | Regular sets of higher-order pushdown stacks[END_REF]; adapting these techniques to annotated PDS is a challenging problem.

A Collapsible Pushdown Systems

We give the definition of higher-order collapsible stacks and their operations, before giving the definition of collapsible pushdown systems.

A.1 Higher-Order Collapsible Stacks

Higher-order collapsible stacks are built from a stack alphabet Σ and form a nested "stack-of-stacks" structure. Furthermore, each stack character contains a pointer -called a "link" -to a position lower down in the stack. When building stacks from the stack operations defined below, copies of sub-stacks will be made. The link is intuitively a pointer to the context in which the stack character was first created. We define collapse links formally below.

Definition 6 (Order-n Collapsible Stacks). Given a finite set of stack characters Σ, an order-0 stack is simply a character a ∈ Σ. An order-n stack is a sequence w = [w 1 . . . w ℓ ] n such that each w i is an order-(n -1) stack and each character on the stack is augmented with a collapse link. Let Stacks n denote the set of order-n stacks.

An order-n stack can be represented naturally as an edge-labelled word-graph over the alphabet {[ n-1 , . . . , [ 1 , ] 1 , . . . , ] n-1 } ⊎ Σ, with additional collapse-links pointing from a stack character in Σ to the beginning of the graph representing the target of the link. An example order-3 stack is given below, with only a few collapse links shown. The collapse links range from order-3 to order-1 respectively.

• • • • • • • • • • • • • • • • [ 2 [ 1 a b ] 1 ] 2 [ 2 [ 1 c ] 1 [ 1 d e ] 1 ] 2
Given an order-n stack [w 1 . . . w ℓ ] n , we define

top n ([w 1 . . . w ℓ ] n ) = w 1 when ℓ > 0 top n ([] n ) = [] n-1 otherwise top k ([w 1 . . . w ℓ ] n ) = top k (w 1 ) when k < n and ℓ > 0 noting that top k (w) is undefined if top k ′ (w) is empty for any k ′ > k.
We also remove the top portion of a top k stack using

bot i n ([w 1 . . . w ℓ ] n ) = [w ℓ-i+1 . . . w ℓ ] n when i ≤ ℓ and ℓ > 0 bot i k ([w 1 . . . w ℓ ] n ) = [bot i k (w 1 )w 2 . . . w ℓ ] n when k < n and ℓ > 0 .
Formally, then, a collapse link is a pair (k, i) where 1 ≤ k ≤ n and i > 0. For top 1 (w) = a where a has the link (k, i), the destination of the link is bot i k (w). We disallow collapse links where bot i k does not lead to a valid stack. The example stack above is thus [[[a (3,1) (1,1) e] 1 ] 2 ] 3 , where collapse links are denoted as superscripts. Often, we will omit these superscripts for readability.

b] 1 ] 2 [[c (2,1) ] 1 ] 2 [[d

A.2 Operations on Order-n Collapsible Stacks

The following operations may be performed on an order-n collapsible stack.

O n = {pop 1 , . . . , pop n } ∪ {push 2 , . . . , push n } ∪ {collapse 2 , . . . , collapse n } ∪ push 1 a , . . . , push n a , rew a | a ∈ Σ We say o ∈ O n is of order-k when k is minimal such that o ∈ O k . For example, push k is of order k.
The collapse k operation is non-standard in the sense of Hague et al. [START_REF] Hague | Collapsible pushdown automata and recursion schemes[END_REF] and has the semantics of a normal collapse, with the additional constraint that the top character has an order-k link. The standard version of collapse can be simulated with a non-deterministic choice on the order of the stack link. In the other direction, we can store in the stack alphabet the order of the collapse link attached to each character on the stack.

We define each stack operation in turn for an order-n stack w. Collapse links are created by the push k a operations, which add a character to the top of a given stack w with a link pointing to pop k (w).

1. We set pop k (w) = v when w decomposes into u : k v for a non-empty u.

We set push

k (w) = u : k u : k v when w = u : k v. 3. We set collapse k (w) = bot i k (w) where top 1 (w) = a (k,i) for some i. 4. We set push k b (w) = b (k,ℓ-1) : 1 w where top k+1 (w) = [w 1 . . . w ℓ ] k+1 . 5. We set rew b (w) = b (k,i) : 1 v where w = a (k,i) : 1 v.
Note that, for a push k operation, links outside of u = top k (w) point to the same destination in both copies of u, while links pointing within u point within the respective copies of u. For full introduction, we refer the reader to Hague et al. [START_REF] Hague | Collapsible pushdown automata and recursion schemes[END_REF]. In Section 3.2 we give several example stacks and show how the stack operations affect them.

A.3 Collapsible Pushdown Systems

We are now ready to define alternating collapsible pushdown systems.

Definition 7 (Collapsible Pushdown Systems

). An alternating order-n collapsible pushdown system (collapsible PDS) is a tuple C = (P, Σ, R) where P is a finite set of control states, Σ is a finite stack alphabet, and R ⊆ (P × Σ × O n × P)∪ P × 2 P is a set of rules.

We write configurations of a collapsible PDS as a pair p, w where p ∈ P and w ∈ Stacks n . We write p, w -→ p ′ , w ′ to denote a transition from a rule (p, a, o, p ′ ) with top 1 (w) = a and w ′ = o(w). Furthermore, we have a transition p, w -→ { p ′ , w | p ′ ∈ P } whenever we have a rule p → P . A non-alternating collapsible PDS has no rules of this second form. We write C to denote a set of configurations.

B Stack Automata

We present omitted proofs and definitions for stack automata. We remark that both the definition of a run, and the test for membership, can easily be adapted to collapsible stacks by simply following the collapse links rather than the annotations.

B.1 Additional Notation

For n ≥ k > 1, we write Q 1 Q ′ -→ Q 2 to
denote an order-k transition from a set of states whenever Q 1 = {q 1 , . . . , q ℓ } and for each 1

≤ i ≤ ℓ we have q i q ′ i -→ Q i and Q ′ = {q ′ 1 , . . . , q ′ ℓ } and Q 2 = 1≤i≤ℓ Q i .
The analogous notation at order-1 is a special case of the short-form notation defined in Section 3.1.

B.2 Runs of Stack Automata

Formally, fix a stack automaton

A = (Q n , . . . , Q 1 , Σ, ∆ n , . . . , ∆ 1 , F n , . . . , F 1 ) .
We say a node contains a character if its exiting edge is labelled by the character. Recall the tree view of an annotated stack, an example of which is given below.

• • • • • • • • • • • • • • • • • [ 2 [ 1 a b ] 1 ] 2 [ 2 [ 1 c ] 1 ] 2 [ 1 d ] 1
Some stack (tree) w is accepted by A from states Q 0 ⊆ Q k -written w ∈ L Q0 (A) -whenever the nodes of the tree can be labelled by elements of

1≤k ′ ≤n 2 Q k ′ such that
1. Q 0 is a subset of the label of the node containing the first [ k-1 character of the word, or if k = 1, the first character a ∈ Σ, and 2. for any node containing a character [ k ′ labelled by Q, then for all q 1 ∈ Q, there exists some transition (q 1 , q 2 , Q 1 ) ∈ ∆ k ′ +1 such that q 2 appears in the label of the succeeding node and Q 1 is a subset of the label of the node succeeding the matching ] k ′ character, and 3. for any node containing a character ] k ′ , the label Q is a subset of F k ′ , and the final node of an order-k stack is labelled by Q ⊆ F k , and 4. for any node containing a character a ∈ Σ, labelled by Q, for all q ′ ∈ Q, there exists some transition (q ′ , a, Q br , Q ′ ) ∈ ∆ 1 such that Q br is a subset of the label of the node annotating a, and Q ′ is a subset of the label of the succeeding node.

That is, a stack automaton is essentially a stack-and annotation-aware alternating automaton, where annotations are treated as special cases of the alternation.

Proposition 2 (Stack Automata Membership). Membership order-n stack automata can be tested in linear time in the size of the input stack and stack automaton.

Proof. Take a stack w and let

A = (Q n , . . . , Q 1 , Σ, ∆ n , . . . , ∆ 1 , F n , . . . , F 1 ) .
The membership algorithm iterates from the bottom (end) of the stack and its annotations to the top (beginning). Take the graph representing w. We start by labelling the final node with the set F n . It is easy to verify at all stages that if the label of a node contains a state q, then the stack from that node is in L q (A). Now, suppose we have labelled up to a given node. For convenience, we will refer to nodes by their labelled state set, and we show, by cases, how to label the preceding node with a state-set Q 0 .

In the first case, we have node

Q 1 connected to Q 0 by a ] k character. That is Q 0 Q 1 • • • ] k
where Q 0 is the set F k . This is because Q 0 labels the end of an order-k stack.

In the next case the connection is by a character a with an annotation and we have

Q 0 Q 1 • • • Q br • • • . a where Q 0 = q q a --→ Q ′ br Q ′ 1 ∈ ∆ 1 ∧ Q ′ 1 ⊆ Q 1 ∧ Q ′ br ⊆ Q br .
Thus, any state in Q 0 has a transition to states from which the remainder of the stack is accepted.

In the final case we have

Q 0 Q 1 • • • Q 2 • • • [ k ] k where ] k matches [ k . We define Q 0 = q q q ′ -→ Q ∈ ∆ k+1 ∧ q ′ ∈ Q 1 ∧ Q ⊆ Q 2 .
Thus, there is a state q ∈ Q 0 whenever there is a transition q q ′ -→ Q such that the next order-k stack is accepted from q ′ and the remainder of the stack is accepted from Q.

Thus, after this labelling, we can test whether w ∈ L Q0 (A) for Q 0 ⊆ Q k by checking whether Q 0 ⊆ Q where Q labels the node containing the first [ k-1 character of the word, or if k = 1, the first character a ∈ Σ.

We now show that emptiness checking is PSPACE-complete.

Proposition 3 (Emptiness of Stack Automata). Given an order-n stack automaton A and a state q of A, deciding if there exists some annotated stack

w ∈ L q (A) is PSPACE-complete.
The problem is already PSPACE-hard for alternating word automata which correspond to the order-1 case [START_REF] Ashok | [END_REF]. We now establish the upperbound.

Let A = (Q n , . . . , Q 1 , Σ, ∆ n , . . . , ∆ 1 , F n , . . . , F 1 ) be a stack automaton. We use a fixed point to compute the set

Q ac := { q ∈ Q k | L q (A) = ∅ }.
For this, we take Q 0 to be the set of all final states. For all i ≥ 0, we define Q i+1 by adding to Q i all states q ∈ Q k such that:

-for k > 1, there exists a transition q

q ′ -→ Q ∈ ∆ k with Q ⊆ Q i and q ′ ∈ Q i . -for k = 1, there exists a transition q a --→ Q br Q ∈ ∆ 1 with Q, Q br ⊆ Q i .
As the sequence of the Q i is increasing (for inclusion), we have Q j+1 = Q j for some index j ≥ 0. We claim that Q j is the set Q ac . A straightforward induction shows that Q i ⊆ Q ac and hence Q j ⊆ Q ac . Assume toward a contradiction, that the converse inclusion does not hold. Let w be smallest stack accepted by a state q ∈ Q k \ Q j . If k = 1, then w = a u : 1 w and there exists a transition q a --→ Q br Q ∈ ∆ 1 with w ′ accepted from Q and u is accepted from Q br . As q does not belongs to Q j , then either u or w ′ is accepted from a state not in Q j . As u and w ′ are both smaller than w, this contradictes the definition of w. The case k > 1 is similar.

The algorithm to test emptiness from a given state p ∈ Q n consists of computing Q j by iteratively computing the Q i and then checking if p belongs to Q j .

B.3 Comparison with Broadbent et al. [6]

We show that our notion of stack automata, when viewed as acceptors of collapsible stacks, accept the same family of stacks as the automata introduced by Broadbent et al. in LICS 2010 [START_REF] Broadbent | Recursion schemes and logical reflection[END_REF]. We begin by defining these models, which for the purposes of comparison, we will call bottom-up stack automata. Let

Σ ′ = {[ n-1 , . . . , [ 1 , ] 1 , . . . , ] n-1 } ⊎ Σ. Definition 8 (Bottom-up Stack Automata). A bottom-up stack automa- ton B is a tuple (Q, Σ ′ , q in , F , ∆) where Q is a finite set of states, Σ ′ is a finite input alphabet, q in ∈ Q is the initial state and ∆ : (Q × Σ ′ )∪(Q × Σ ′ × Q) → Q is a deterministic transition function.
Representing collapsible stacks as word graphs, a run of a bottom-up stack automaton is a labelling of the graph with states in Q such that 1. The rightmost (final) node is labelled by q in . 2. The leftmost (initial) node is labelled by q ∈ F . 3. Whenever we have for any a ∈ Σ ′ , and pair of labelled nodes with an edge

• • • q q ′ • • • a then q = ∆(q ′ , a).
4. Whenever we have for any ∈ Σ ′ , and triple of labelled nodes with an edge

• • • q q ′ • • • q br • • • a then q = ∆(q ′ ,
a, q br ).

An example run over an order-2 stack is given below

q f q 1 q 1 1 q 2 1 q 1 2 q 3 1 q 4 1 q 5 1 q in [ 1 a b ] 1 [ 1 a b ] 1
where q f ∈ F . We prove the following proposition.

Proposition 4 (Equivalence of Stack Automata). For every order-n stack automaton A with initial state q, there is a bottom-up stack automaton B with initial state q ′ such that L q (A) = L q ′ (B) and vice-versa.

There are two directions. We begin by constructing a stack automaton from a bottom-up stack automaton. Intuitively this construction implements the membership algorithm as a bottom up automaton. This labels each position of a candidate stack bottom-up (right-to-left) with sets of states from which the topdown automaton would have an accepting run. The states of the bottom-up automaton will therefore be sets of states of the top-down version, creating at worst an exponential blow-up. Definition 9 (Bottom-Up Automata to Stack Automata). Given a bottomup stack automaton B = (Q, Σ ′ , q in , F , ∆), we define

A B = (Q n , . . . , Q 1 , Σ, ∆ n , . . . , ∆ 1 , F n , . . . , F 1 ) .
First we stratify the states of Q into

F ′ k = { q ∈ Q | ∃q ′ ∈ Q. q = ∆(q ′ , ] k ) } where 1 ≤ k < n F ′ n = {q in } and Q ′ k = { q ∈ Q | ∃q ′ ∈ Q. q = ∆(q ′ , a, [ k-1 ) } ∪ F ′ k when 1 < k ≤ n Q ′ 1 = { q ∈ Q | ∃q ′ , q br ∈ Q, a ∈ Σ. q = ∆(q ′ , a, q br ) } ∪ F ′ 1 .
Then we define the states of A B to be

Q k = Q ′ k × • • • × Q ′ n for all 1 ≤ k < n and Q n = Q ′ n ∪ {q 0 } where q 0 is a fresh state, with F n = F ′ n ∪ { q 0 | q in ∈ F } and F k = { (q k , q k+1 , . . . , q n ) | q k = ∆(q k+1 , ] k ) } for all 1 ≤ k < n.
That is, we have to keep track of where to return to after the completion of a stack. We need to keep complete information when handling the collapse links.

then have the transition relations

∆ 1 = (q 1 , q 2 , . . . , q n ) a -----------→
{(q br ,q k+1 ,...,qn)} {(q ′ 1 , q 2 , . . . , q n )} q 1 = ∆(q ′ 1 , a, q br ) ∧ q br ∈ Q ′ k and when 1 < k < n we have ∆ k =    (q k , q k+1 , . . . , q n ) (qk-1,q ′ k ,q k+1 ,...,qn)

-------------→ {(q ′ k , q k+1 , . . . , q n )}

q k = ∆(q k-1 , [ k-1 ) ∧ q ′ k ∈ Q ′ k    and ∆ n = q n (qn-1,q ′ n ) ------→ {q ′ n } | q n = ∆(q n-1 , [ n-1 ) ∧ q ′ n ∈ Q ′ n ∪ q 0 (qn-1,q ′ n ) ------→ {q ′ n } | ∃q n = ∆(q n-1 , [ n-1 ) ∧ q n ∈ F ∧ q ′ n ∈ Q ′ n
We then have Lemma 1 (Correctness of A B ). For a given bottom-up stack automaton B with initial state q in , for every order-n collapsible stack w we have

w ∈ L qin (B) iff [[ w ]] ∈ L q0 (A B ).
Proof. There two directions: take an accepting run of B and show how to construct an accepting run of A B , then consider the opposite direction.

1. Take the run graph R over any accepted stack w. We take an unlabelled graph of w which we will label with an accepting run of A B , proceeding from left to right. In the case when w is empty, R has a single node labelled q in . For this to be accepting, q in must be final. Hence q 0 is final, and we build the run graph whose single node is labelled q 0 . Otherwise, we label the leftmost node q 0 and we have in R the labelling

q n [n-1
---→ q n-1 with q n = ∆(q n-1 , [ n-1 ) and q n ∈ F . Let q ′ n be the labelling in R after the matching ] n-1 . We use the transition q 0 (qn-1,q ′ n ) ------→ {q ′ n } ∈ ∆ n to extend the run of A B . We thus maintain the invariant that a node is labelled by (q k , q k+1 , . . . , q n ) where q k labels the corresponding node in R and q k+1 , . . . , q n are the labels in R occurring immediately after the next ] k , . . . , ] n-1 respectively. Suppose from the current node we have q k

[ k-1 ---→ q k-1 in R with q k = ∆(q k-1 , [ k-1 ). Let q ′
k be the labelling in R immediately after the matching ] k-1 . From the invariant we extend the run being built from (q k , q k+1 , . . . , q n ). We use the transition (q k , q k+1 , . . . , q n ) (qk-1,q ′ k ,q k+1 ,...,qn)

-------------→ {(q ′ k , q k+1 , . . . , q n )} to do so, which maintains the invariant. In the next case, we have in R

q 1 q ′ 1 • • q br • • • . a
and the node in the run we're constructing is labelled by (q 1 , q 2 , . . . , q n ). We use the transition (q 1 , q 2 , . . . , q n ) a -----------→ {(q br ,q k+1 ,...,qn)} {(q ′ 1 , q 2 , . . . , q n )} which maintains the invariant.

Finally, when we have in R the edge q 1 ] k -→ q 2 , then our current node is labelled (q k , q k+1 , . . . , q n ) with q k = ∆(q k+1 , ] k ), hence the labelling is in F k . This means the current stack is accepted, and from the above we know the next node is labelled by (q k+1 , . . . , q n ) as required to maintain the invariant. The rightmost node of the run constructed is necessarily labelled q in , giving us an accepting run as required. 2. Next, we take an accepting run over any w of A B and construct an accepting run of B. The proof relies on a key observation: the labelling of each node may consist of a single state only. We prove this by backwards induction over the run graph R of A B . The rightmost node is necessarily labelled q 0 for empty w or q in otherwise. Since the former case is trivial, assume the label is q in . This is the unique labelling such that acceptance can occur.

Now, induct right to left. Assume we have

Q ] k-1
---→ (q k , . . . , q n ) where the label (q k , . . . , q n ) is the unique label from which the rest of the run can be accepting. From the determinism of B, there is one q k-1 = ∆(q k , ] k-1 ). Thus we must have Q = {(q k-1 , q k , . . . , q n )} being the only possible labelling of the new node. In the next case we have in R Q (q ′ 1 , q 2 , . . . , q n ) • • • (q br , q k+1 , . . . , q n ) • • • . a noting that the labellings must be consistent in q k+1 , . . . , q n . (This can be checked by following this induction.) From the determinism of B, there is a unique q 1 = ∆(q ′ 1 , a, q br ). This implies Q can only be {(q 1 , q 2 , . . . , q n )}. In the next case we have the case of Q

[ k -→ q k , q ′
k+1 , q k+2 , . . . , q n . From the determinism of B we have a unique q k+1 = ∆(q k , [ k ). Hence, it must be the case that Q = {(q k+1 , q k+2 , . . . , q n )}.

Finally, we look at the leftmost node. We have q 0 [n-1 ---→ (q n-1 , q ′ n ) and we know there is q n ∈ F such that q n = ∆(q n-1 , [ n-1 ). Thus, we construct an accepting run of B by taking the labelling of R and projecting it to the first component of each tuple, labelling the leftmost node with q n . Now we consider the translation from stack automata to bottom-up stack automata.

(Stack Automata to Bottom-Up Automata). Given an order-n stack automaton

A = (Q n , . . . , Q 1 , Σ, ∆ n , . . . , ∆ 1 , F n , . . . , F 1 )
and q in ∈ Q n , we construct a bottom-up stack automaton

B A = (Q, Σ ′ , F n , F , ∆) where F = { Q ⊆ Q n | q in ∈ Q } and Q = 1≤k≤n 2 Q k × • • • × 2 Qn .
This structure is needed to flatten the nested structure of the automaton.

We define ∆ to be the smallest set containing

1. For all 1 < k ≤ n and Q k ⊆ Q k , . . . , Q n ⊆ Q n we have the transition ((F k-1 , Q k , . . . , Q n ) , ] k-1 , (Q k , . . . , Q n ))
. Note Q k is stored to know which transitions to use on reading the matching [ k-1 , and 2. For all a ∈ Σ,

1 ≤ k ≤ n and Q 2 ⊆ Q 2 , . . . , Q n ⊆ Q n and Q br ⊆ Q k we have the transition Q 1 , Q 2 , . . . , Q n , a, (Q br , Q k+1 , . . . , Q n ) , Q 2 , Q 2 , . . . , Q n where Q 1 is maximal such that Q 1 a --→ Q ′ br Q ′ and Q ′ br ⊆ Q br and Q ′ ⊆ Q 2 , and 3. For all 1 ≤ k < n and Q k ⊆ Q k , . . . , Q n ⊆ Q n we have that there is a transition ((Q, Q k+2 , . . . , Q n ) , [ k , (Q k , Q k+1 , Q k+2 , . . . , Q n )) whenever Q is maximal such that Q Q ′ k --→ Q ′ k+1 ∈ ∆ k+1 with Q ′ k ⊆ Q k and Q ′ k+1 ⊆ Q k+1 .
We then have Lemma 2 (Correctness of B A ). For a given order-n stack automaton A and state q in ∈ Q n , for every order-n collapsible stack w we have w ∈ L qin (A) iff w ∈ L Fn (A B ).

Proof. There are two directions -first we translate an accepting run of A over any w into an accepting run of B A , then vice-versa.

1. Take any stack w and an accepting run R of A. From R we construct an accepting run of B A . We proceed by induction from the rightmost node of R, which we label with F n . We now consider the inductive cases.

Suppose from the current node we have

Q k-1 ] k-1 ---→ Q k in R. By induc- tion, assume the node corresponding to Q k in the run being constructed is labelled (Q r k , . . . , Q r n ) where Q r k ⊇ Q k , . . . , Q r n ⊇ Q n , where Q k , . . . , Q n are the labels in R immediately following the next ] k-1 , . . . , ] n-1 charac- ters respectively. From the construction of B A , we have a transition F k-1 = ∆((Q r k , . . . , Q r n ) , ] k-1 ) and since R is accepting, we know F k-1 ⊇ Q k-1 . Hence, we label the node corresponding to Q k-1 with (F k-1 , Q r k , . . . , Q r n )
, maintaining the induction hypothesis. In the next case, we have in R

Q ′ 1 Q 1 • • Q br • • • a
for some order-k link and the latter two corresponding nodes in the run we're constructing are labelled by

(Q r 1 , Q r 2 , . . . , Q r n ) and Q r br , Q r k+1 , . . . , Q r n with Q r 1 ⊇ Q 1 , . . . , Q r n ⊇ Q n where Q 2 , .
. . , Q n are the labels in R immediately following the next ] k-1 , . . . , ] n-1 characters respectively and Q r br ⊇ Q br . From the construction, we have the transition

(Q, Q r 2 , . . . , Q r n ) , a, Q r br , Q r k+1 , . . . , Q r n , (Q r 1 , Q r 2 , . . . , Q r n )
where, since Q is maximal, we have

Q ⊇ Q ′ 1 . Finally, when we have in R the edge Q k+1 [ k -→ Q k we
know by induction that the node corresponding to the latter node is labelled by Q r k , Q r k+1 , . . . , Q r n with the superset property as in the previous cases. From the construction, we have the transition

Q, Q r k+2 , . . . , Q r n , [ k , Q r k , Q r k+1 , Q r k+2 , . . . , Q r n and since Q is maximal, we have Q ⊇ Q k+1 .
Thus, when we reach the leftmost node, we have a label Q with q in ∈ Q.

Hence, Q ∈ F and the run is accepting. 2. Take any stack w and an accepting run R of B A . For any node whose label has the first component Q, we prove for any state q ∈ Q there is an accepting run of A from the node. The run begins with q.

We proceed by induction. In the base case, take the rightmost node. This is labelled by F n , hence the result is immediate. We now consider the inductive cases. Suppose we have

(Q k-1 , Q k , . . . , Q n ) ] k-1 ---→ (Q k , . . . , Q n ) in R.
From the construction of B A , we have Q k-1 = F k-1 thus an accepting run from all states in F k-1 (by definition of accepting runs from states in Q k-1 , there is nothing more to satisfy). In the next case, we have in R

(Q ′ 1 , Q 2 , . . . , Q n ) (Q 1 , Q 2 , . . . , Q n ) • • • (Q br , Q k+1 , . . . , Q n ) • • • a for some order-k link. For every q ∈ Q ′ 1 we have q a --→ Q ′ br Q ′′ 1 ∈ ∆ 1 ,

and accepting runs from all states in

Q ′ br ⊆ Q br and Q ′′ 1 ⊆ Q ′ 1 .
Thus, we have an accepting run from q. Finally, when we have in R the edge

(Q, Q k+2 , . . . , Q n ) [ k -→ (Q k , Q k+1 , Q k+2 , . . . , Q n )
we know by construction of B A that the node occurring after the matching ] k is labelled (Q k+1 , . . . , Q n ). Also by construction of B A we know for all ∈ Q that we have a transition q

q ′ -→ Q ′ with q ′ ∈ Q k and Q ′ ⊆ Q k+1 .
By induction, we have accepting runs from q ′ and Q ′ , giving an accepting run from q. Thus, when we reach the leftmost node, we have a label Q ∈ F , hence q in ∈ Q. Hence, we have an accepting run of A from q in . B.4 Effective Boolean Algebra Proposition 5 (Effective Boolean Algebra for Languages of Stack Automata). The set of annotated stacks accepted by stack automata form an effective Boolean algebra.

Proof (sketch). The automata constructions follow standard techniques. Fix a stack automaton

A = (Q n , . . . , Q 1 , Σ, ∆ n , . . . , ∆ 1 , F n , . . . , F 1 ) .
There are three cases.

1. Take any two states q 1 and q 2 both elements of the same Q k . We can introduce a new state q that accepts the intersection of q 1 and q 2 . At order-1, we make q ∈ F 1 iff q 1 , q 2 ∈ F 1 . Then, for each

{q 1 , q 2 } a --→ Q br Q, introduce a transition q a --→ Q br Q.
At order-k for 1 < k ≤ n, we can permit transitions q Q ′ -→ Q by constructing a state q ′ accepting the intersection of the states in Q ′ and introducing the transition q q ′ -→ Q. Thus, to form the intersection of q 1 and q 2 we set q ∈ F k iff q 1 , q 2 ∈ F k and for each transition

{q 1 , q 2 } Q ′ -→ Q, add the transition q Q ′ -→ Q. 2.
To form the union of q 1 and q 2 , we again introduce a new state q.

At order-1 we set q ∈ F 1 iff q 1 ∈ F 1 or q 2 ∈ F 1 , then for each transition

q 1 a --→ Q br Q or q 2 a --→ Q br Q, add the transition q a --→ Q br Q. At order-k for 1 < k ≤ n we set q ∈ F k iff q 1 ∈ F k or q 2 ∈ F k , then for each transition q 1 q ′ -→ Q or q 2 q ′ -→ Q, add the transition q q ′ -→ Q. 3.
Finally, to negate an automaton, we introduce for every state q it's negation q. We also introduce q * k states which accept any stack of order-k. For q ∈ Q 1 , we set q ∈ F 1 iff q / ∈ F 1 . Then, for every a, let q a --→

Q 1 br Q 1 , . . . , q a --→ Q ℓ br
Q ℓ be the transitions over a from q. We take each subset I ⊆ {1, . . . , ℓ} in turn and for every Q br and Q such that -if i ∈ I, then there is some

q br ∈ Q i br ∩ Q k ′ (for some k ′ ) with either q br ∈ Q br or q * k ′′ ∈ Q br where k ′′ = k ′ , and -if i / ∈ I, then there is some q ′ ∈ Q i with q ′ ∈ Q,
we introduce a transition q a Q br Q when Q br is coherent with respect to the order of the annotation. That is, every transition from q either rejects by the annotation branch (by being of the wrong order, or the right order, but the wrong shape), or by the remainder of the order-1 stack. Finally, when q ∈ Q k for 1 < k ≤ n, we set q ∈ F k iff q / ∈ F k . Then, let q

q ′ 1 -→ Q 1 , . . . , q q ′ ℓ
-→ Q ℓ be the transitions from q. Next, for every subset I ⊆ {1, . . . , ℓ} and for every Q ′ and Q such that

-if i ∈ I, then q ′ i ∈ Q ′ , and -if i / ∈ I, then there is some q ′ ∈ Q i with q ′ ∈ Q, we introduce a transition q Q ′ -→ Q.
That is, every transition from q either rejects by the top order-(k -1) stack, or by the remainder of the order-k stack.

C Soundness

In this section, all stack automata are such that their initial states are not final. This is assumed for the automaton A 0 in Section 3.1. This property is preserved by the saturation function Γ .

We start by assigning 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 ∈ Q k , which is denoted w |= q. Definition 11 (w |= q). For any Q ⊆ Q k and any order-k stack w, we write w |= Q if w |= q for all q ∈ Q, and we define w |= q by a case distinction on q.

1. q is an initial state in Q n . Then for any order-n stack w, we say that w |= q if q, w ∈ P re * C (A 0 ). 2. q is an initial state in Q k , labeling a transition q k+1 q -→ Q k+1 ∈ ∆ k+1 . Then for any order-k stack w, we say that w |= q if for all order-(k + 1) stacks s.t. v |= Q k+1 , then w : (k+1) v |= q k+1 . 3. q is a non-initial state in Q k . Then for any order-k stack w, we say that w |= 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 ∈ Q k with q q k -→ (Q k+1 , . . . , Q n ) if for any order-(k+1) stack w k+1 |= Q k+1 , . . . , and any order-n stack

w n |= Q n , we have w k : (k+1) • • • : n w n |= q. Definition 12 (Soundness of transitions). A transition q a --→ Q br (Q 1 , . . . , Q k )
is sound if for any order-1 stack w 1 |= Q 1 , . . . , and any order-k stack w k |= Q k and any stack u |= Q br , we have a u :

1 w 1 : 2 • • • : k w k |= q. Lemma 3. If q p a --→ Q br (Q 1 , . . . , Q n ) is sound, then any transition q k a --→ Q br (Q 1 , . . . , Q k )
contained within the transition from q p is sound.

The proof is by induction over k. In the base case, k = n, then q k = q p and the result is immediate. Otherwise, assume q k+1 a --→

Q br (Q 1 , . . . , Q k+1 ) is sound -where q k+1 or q k+2 q k+1 ---→ (Q k+2 , . . . , Q n ) -and q k+1 q k -→ Q k+1 . We need to show q k a --→ Q br (Q 1 , . . . , Q k ) is sound. Hence, take any w 1 |= Q 1 , . . . , w k |= Q k and u |= Q br . By definition of |=, we have a u : 1 w 1 : 2 • • • : k w k |= q k if, for all w k+1 |= Q k+1 , we have a u : 1 w 1 : 2 • • • : (k+1) w k+1 |= q k+1 . Since w 1 |= Q 1 , . . . , w k+1 |= Q k+1 and q k+1 a --→ Q br (Q 1 , . . . , Q k+1 ) is sound, we have a u : 1 w 1 : 2 • • • : (k+1) w k+1 |= q k+1 and hence a u : 1 w 1 : 2 • • • : k w k |= q k . Thus, q k a --→ Q br (Q 1 , . . . , Q k ) is sound.
Definition 13 (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 p a --→ Q br (Q 1 , . . . , Q k ) for k < n is sound.
Unsurprisingly, if some order-n stack w is accepted by a sound stack automaton A from a state q p then p, w belongs to P re * C (A 0 More generally, we have the following result. Lemma 4. Let A be a sound stack automaton A and let w be an order-k stack. If A accepts w from a state q ∈ Q k then w |= q. In particular, if A accepts an order-n stack w from a state q p ∈ Q n then p, w belongs to P re * C (A 0 ). Proof. We proceed by induction on the size of the stack (where the size of an annotated stack is defined to be the size of a tree representing the stack).

Let w be an order-k stack accepted from a state q ∈ Q k . We assume that the property holds for any smaller stack.

If w is empty then q is a final state. Recall that by assumption final states are not initial. Hence, q is not initial and therefore q is a final state of A 0 . It follows that the empty stack is accepted from q in A 0 and hence w |= q.

If w is a not empty stack of order-1. The stack w can be decompose as a u : 1 v. As w is accepted by A from q, there exists a transition q a --→ Q br (Q) such that v is accepted from Q and u is accepted from Q br . By induction hypothesis (both u and v are smaller than w), we have u |= Q br and v |= Q br . As the transition q

a --→ Q br (Q) is sound, we have that w |= q.
If w is a not empty stack of order-k. The stack w can be decompose as u : k+1 v. As w is accepted by A from q, there exists a transition q q ′ -→ Q such that v is accepted from Q and u is accepted from q ′ . By induction hypothesis, we have u |= q ′ and v |= Q. By definition of the satisfiability wrt the (initial) state q ′ , we have w |= q ′ . We first establish that the initial automaton A 0 is sound.

Lemma 5 (Soundness of A

0 The automaton A 0 is sound. Proof. Let q a --→ Q br (Q 1 , . . . , Q k ) for k ≤ n.
As we required in Section 3.1 that no initial states of A 0 has an incoming transition, the sets Q i , i ∈ [1, k] and the set Q br do not contain any initial states.

By Lemma ??, it is only necessary to prove the property for k = n or for k < n with q being non-initial.

First assume that k < n and that q is not initial. For any order-1 stack w 1 |= Q 1 , . . . , and any order-k stack w k |= Q k and any stack u |= Q br , we have to show that w = a u :

1 w 1 : 2 • • • : k w k |= q.
As q is not initial, we need to show that A 0 accepts w from q. As for all i ∈ [1, k], we have A 0 accepts w i from the set of states Q i and the stack u from the set Q br , we easily derive an accepting run of A 0 from q on reading w. Now assume that k = n. For any order-1 stack w 1 |= Q 1 , . . . , and any orderk stack w k |= Q n and any stack u |= Q br , we have to show that w = a u : 1 w 1 : 2 • • • : n w n |= q. It suffices to show that A 0 accepts w from q (as if q is equal to q p for some control state p, this implies that q p , w belongs P re * C (A 0 )). As for all i ∈ [1, n], we have A 0 accepts w i from the set of states Q i and the stack u from the set Q br , we easily derive an accepting run of A 0 from q on reading w.

We are now ready to prove that the stack automaton produced by our algorithm is sound.

Lemma 6 (Automaton Soundness). The automaton A constructed by saturation with Γ and C from A 0 is sound.

Proof. The proof is by induction on the number of iterations of Γ . The base case is the automaton A 0 and the result was established in Lemma ??.

The inductive step is by case distinction on the rule (p, a, o, p ′ ) that led to the introduction of each new transition.

1. Assume that o = pop k , that we had a transition q p ′ q k -→ (Q k+1 , . . . , Q n ) and that we added the transition

q p a -→ ∅ (∅, . . . , ∅, {q k } , Q k+1 , . . . , Q n ) .
To establish soundness of this latter transition, we have to prove that for any w 1 |= ∅, . . ., any w k-1 |= ∅, any w k |= q k , any w k+1 |= Q k+1 , . . ., any w n |= Q n and any u |= ∅, one has w = a u : 1 w 1 : 2 • • • : n w n |= q p . For this, it suffices to show that pop k (w) |= q p ′ . Indeed, as q p and q p ′ are initial states in Q n , w |= q p means that p, w ∈ P re * C (A 0 ) and pop k (w) |= q p ′ means that p ′ , pop k (w) ∈ P re * C (A 0 ): as we have the rule (p, a, pop k , p ′ ), we will have the result as required. Since w k |= q k and w k+1 |= Q k+1 , . . . , w n |= Q n , we know from the definition of |= and

q p ′ q k -→ (Q k+1 . . . , Q n ) that pop k (w) = w k : (k+1) • • • : n w n |= q p ′
and we are done.

Assume that o = push k , that we had the sound transitions

q p ′ a --→ Q br (Q 1 , . . . , Q n ) and Q k a --→ Q ′ br (Q ′ 1 , . . . , Q ′ k )
and that we added

q p a ------→ Q br ∪Q ′ br Q 1 ∪ Q ′ 1 , . . . , Q k-1 ∪ Q ′ k-1 , Q ′ k , Q k+1 , . . . , Q n .
To establish soundness of this latter transition, we have to prove that for any

w 1 |= Q 1 ∪ Q ′ 1 , . . ., any w k-1 |= Q k-1 ∪ Q ′ k-1 , any w k |= Q ′ k , any w k+1 |= Q k+1 , . . ., any w n |= Q n and any u |= Q br ∪ Q ′ br , we have that w = a u : 1 w 1 : 2 • • • : n w n |= q p .
For this it suffices to show push k (w) |= q p ′ . Indeed, as q p and q p ′ are initial states in Q n , w |= q p means that p, w ∈ P re * C (A 0 ) and push k (w) |= q p ′ means that p ′ , push k (w) ∈ P re * C (A 0 ): as we have the rule (p, a, push k , p ′ ), we will have the result as required.

Let v = top k (w) = a u : 1 w 1 : 2 • • • : (k-1) w k-1 . From the soundness of Q k a --→ Q ′ br (Q ′ 1 , . . . , Q ′ k ) and as u |= Q ′ br , w 1 |= Q ′ 1 , . . . , w k |= Q ′ k , we have v : k w k |= Q k . Then, from w 1 |= Q 1 , . . . , w k-1 |= Q k-1 , and v : k w k |= Q k , and w k+1 |= Q k+1 , . . . , w n |= Q n and u |= Q br and the soundness of q p ′ a --→ Q br (Q 1 , . . . , Q n ) we get push k (w) = v : k v : k w k : (k+1) • • • : n w n |= q p ′ as required.
3. Assume that o = collapse k , that k < n and that we had a transition q p ′ q k -→ (Q k+1 , . . . , Q n ) and we added

q p a ---→ {q k } (∅, . . . , ∅, Q k+1 , . . . , Q n ) .
To establish soundness of this latter transition, we have to prove that for any w 1 |= ∅, . . ., any w k |= ∅, any w k+1 |= Q k+1 , . . ., any w n |= Q n and any u |= q k , that we have w = a u : 1 w 1 : 2 • • • : n w n |= q p . For this it suffices to show collapse k (w) |= q p ′ . Indeed, as q p and q p ′ are initial states in Q n , w |= q p means that p, w ∈ P re * C (A 0 ) and collapse k (w) |= q p ′ means that p ′ , collapse k (w) ∈ P re * C (A 0 ): as we have the rule (p, a, collapse k , p ′ ), we will have the result as required. Since u |= q k and w k+1 |= Q k+1 , . . . , w n |= Q n , we know from the definition of |= and

q p ′ q k -→ (Q k+1 , . . . , Q n ) that collapse k (w) = u : (k+1) w k+1 : (k+2) • • • : n w n |= q p ′
hence, we are done.

Assume now that o = collapse k , that k = n and that we added q p a ----→ {q p ′ } (∅, . . . , ∅). To prove that this latter transition is sound, we have to prove that for any w 1 |= ∅, . . . , any w n |= ∅ and any u |= q p ′ , we have w = a u : 1 w 1 : 2 • • • : n w n |= q p . We immediately know collapse k (w) = u |= q p ′ , and we conclude using the same argument as in the first subcase.

Assume that o = push

b , that we had the sound transitions

q p ′ b --→ Q br (Q 1 , . . . , Q n ) and Q 1 a --→ Q ′ br (Q ′ 1 )
and that we added

q p a --→ Q ′ br (Q ′ 1 , Q 2 , . . . , Q k ∪ Q br , . . . , Q n ) .
To prove that this later transition is sound, we have to prove that for any

w 1 |= Q ′ 1 , any w 2 |= Q 2 , . . ., any w k-1 |= Q k-1 , any w k |= Q k ∪ Q br , any w k+1 |= Q k+1 , . . ., any w n |= Q n and any u |= Q ′ br , that we have w = a u : 1 w 1 : 2 • • • : n w n |= q p .
For this it suffices to show push k b (w) |= q p ′ . Indeed, as q p and q p ′ are initial states in Q n , w |= q p means that p, w ∈ P re * C (A 0 ) and push k b (w) |= q p ′ means that p ′ , push k b (w) ∈ P re * C (A 0 ): as we have the rule p, a, push k b , p ′ , we will have the result as required. From the soundness of

Q 1 a --→ Q ′ br (Q ′ 1 ) and as u |= Q ′ br and w 1 |= Q ′ 1 we have a u : 1 w 1 |= Q 1 . Then, from a u : 1 w 1 |= Q 1 , w 2 |= Q 2 , . . . , w n |= Q n , and top k+1 (pop k (w)) = w k |= Q br , and the soundness of q p ′ b --→ Q br (Q 1 , . . . , Q n ), we get push k b (w) = b w k : 1 a u : 1 w 1 : 2 • • • : n w n |= q p ′ as required.
5. Assume that o = rew b , that we had the sound transition

q p ′ b --→ Q br (Q 1 , . . . , Q n )
and that we added

q p a --→ Q br (Q 1 , . . . , Q n ) .
To prove that this later transition is sound, we have to prove that for any w 1 |= Q 1 , . . . , for any w n |= Q n and any u |= Q br , we have that w = a u : 1 w 1 : 2 • • • : n w n |= q p . For this it suffices to show rew b (w) |= q p ′ . Indeed, as q p and q p ′ are initial states in Q n , w |= q p means that p, w ∈ P re * C (A 0 ) and rew b (w) |= q p ′ means that p ′ , rew b (w) ∈ P re * C (A 0 ): as we have the rule (p, a, rew b , p ′ ), we will have the result as required. From w 1 |= Q 1 , . . . , w n |= Q n , and u |= Q br , and the soundness of

q p ′ b --→ Q br (Q 1 , . . . , Q n ), we get rew b (w) = b u : 1 w 1 : 2 • • • : n w n |= q p ′ as required.
The final case is when a transition was added due to an alternating transition p

→ P . Letting Q = { q p ′ | p ′ ∈ P } we added a rule q p a --→ Q br (Q 1 , . . . , Q n ) from the sound transition Q a --→ Q br (Q 1 , . . . , Q n ).
To prove that this later transition is sound, we have to prove that for any w 1 |= Q 1 , . . . , any w n |= Q n and any u |= Q br , we have that w = a u : 1 w 1 : 2 • • • : n w n |= q p . For this it suffices to show w |= Q. Indeed, as q p and Q are initial states in Q n , w |= q p means that p, w ∈ P re * C (A 0 ) and w |= Q means that p ′ , w ∈ P re * C (A 0 ) for all p ′ ∈ P : as we have the rule p → P , we will have the result as required.

--→ Q br (Q 1 , . . . , Q n ), we immediately get w = a u : 1 w 1 : 2 • • • : n w n |= Q as required.

D Completeness

We know show that the automaton constructed by Γ is complete for annotated stacks. The intuition behind the completeness proof is well illustrated by the examples in Section 3.2, hence we encourage the reader to consult these examples when reading the proof.

Lemma 7 (Completeness of Γ ). Given an annotated PDS C and an order-n stack automaton A 0 , the automaton A constructed by saturation with Γ is such that p, w ∈ P re * C (A 0 ) implies w ∈ L qp (A).

Proof. We begin with a definition of P re * C (A 0 ) that permits an inductive proof of completeness. Thus, let P re * C (A 0 ) = α<ω P re α C (A 0 ) where

P re 0 C (A 0 ) = p, w w ∈ L qp (A 0 ) P re α+1 C (A 0 ) = p, w ∃ p, w -→ p ′ , w ′ ∈ P re α C (A 0 ) ∨ ∃ p, w -→ C ⊆ P re α C (A 0 )
The proof is by induction over α. In the base case, we have w ∈ L qp (A 0 ) and the existence of a run of A 0 , and thus a run in A comes directly from the run of A 0 . There are two cases. In the first, inductively assume p, w -→ p ′ , w ′ and an accepting run of w ′ from q p ′ of A via a rule (p, top 1 (w), o, p ′ ). Hence w ′ = o(w).

1. When o = pop k , let q p ′ q k -→ (Q 1 , . . . Q k+1 ) be the order-n to order-k part of the initial transition accepting w ′ . We know, from the construction, we have the transition

q p a -→ ∅ (∅, . . . , ∅, {q k } , Q k+1 , . . . , Q n ). Let w = u k-1 : k u k : (k+1) • • • : n u n . We know w ′ = u k : (k+1) • • • : n u n
and the run from q k over w ′ is accepting. Hence, via the transition from q p we get an accepting run of w which labels all nodes in w ′ with the same nodes as the accepting run of w

′ from q k . 2. When o = push k , let w = u k-1 : k • • • : n u n . We know w ′ = u k-1 : k u k-1 : k u k : (k+1) • • • : n u n . Let q p ′ a --→ Q br (Q 1 , . . . , Q k , . . . Q n ) and Q k a --→ Q ′ br (Q ′ 1 , . . . , Q ′ k )
be the initial transitions used on the run of w ′ (where the transition from Q k reads the second copy of u k-1 ). From the construction we the have a transition

q p a ------→ Q br ∪Q ′ br Q 1 ∪ Q ′ 1 , . . . , Q k-1 ∪ Q ′ k-1 , Q ′ k , Q k+1 , . . . , Q n . Since we know u k : • • • : n u n is accepted from Q ′ k via Q k+1 , .
. . , Q n , and we know that u k-1 is accepted from Q 1 , . . . , Q k-1 and Q ′ 1 , . . . , Q ′ k-1 via a-transitions labelling annotations with Q br and Q ′ br respectively, we obtain an accepting run of w.

When

o = collapse k , let w = a u : 1 u k : (k+1) • • • : n u n where w ′ = u : (k+1) u k+1 : (k+1) • • • : n u n . Let q p ′ q k -→ (Q k+1 , . . . , Q n ) in A
be the initial transition on the accepting run of w ′ (or take q k = q p ′ if k = n). We know from the construction that we have the transition q p a ---→

{q k } (∅, . . . , ∅, Q k+1 , . . . , Q n ).
We know the run from q k via Q k+1 , . . . , Q n over w ′ is accepting. Hence, via the transition from q p we get an accepting run of w which labels all nodes in w ′ with the same nodes as the accepting run of w ′ from q k (we label u k with empty sets).

When

o = push k b , let w = u k-1 : k u k : k+1 • • • : n u n . We know w ′ = push k b (w) is b u k : 1 u k-1 : k • • • : n u n . Let q p ′ b --→ Q br (Q 1 , . . . , Q n ) and Q 1 a --→ Q ′ br Q ′ 1
be the first transitions used on the accepting run of w ′ . From the construction we introduce a transition

q p a --→ Q ′ br (Q ′ 1 , Q 2 , . . . , Q k ∪ Q br , .
. . , Q n ) from which we can construct an accepting run of w (which is w ′ without the first b on top of the top order-1 stack). A run from Q k ∪ Q br exists since u k is also the annotation of b.

When

o = rew b let q p ′ b --→ Q br (Q 1 , . . . , Q n ) be
the first transition on the accepting run of w ′ = b u : 1 v for some v and u. From the construction we know we have a transition q p a --→ Q br (Q 1 , . . . , Q n ), from which we get an accepting run of w = a u : 1 v as required.

The second case is when we have a branching transition p, w -→ C (where C is a set of configurations) via a rule p → P . In this case, let

Q = { q p ′ | p ′ ∈ P } and Q a --→ Q br (Q 1 , . . . , Q n ) be
the accumulation of all initial transitions from states in Q. By construction, we have a rule q p a --→ Q br (Q 1 , . . . , Q n ) from which an accepting run over w can easily be built.

Hence, for every p, w ∈ P re * C (A 0 ) we have w ∈ L qp (A).

E Complexity of collapsible PDS Model Checking

In this section we show that the complexity of the algorithm can be improved to (n -1)-EXPTIME when analysing non-alternating collapsible pushdown systems, matching the known (n-1)-completeness of the problem. The cause of the exponential blow up is the alternation in the automaton constructed. Hence, we introduce a notion of non-alternation at order-n. Note that the automata are alternating both via transitions to Q with |Q| > 1, and via collapse links.

Definition 14 (Non-Alternation at Order-n). An order-n stack automaton A is non-alternating at order-n whenever, for all stacks w ∈ L q (A) for some state q of A, there is an accepting run of A over the graph of w such that no node is labelled by Q ⊆ Q n and |Q| > 1.

For example, take a run over an example order-2 collapsible stack

q p ′ q 1 Q 1 1 Q 2 1 Q 1 2 Q 3 1 Q 4 1 Q 5 1 Q 2 2 • • • . [ 1 a b ] 1 [ 1 a b ] 1 [ 1
This is non-alternating at order-n whenever Q 1 2 ≤ 1 and Q 2 2 ≤ 1. Note, for example, that a stack automaton that does not follow collapse links, and has no alternating transitions in ∆ n , is trivially non-alternating at order-n. Similarly, we may allow q a --→ Q br (∅, . . . , ∅) when Q br ⊆ Q n and |Q br | ≤ 1.

Observe that, since annotations are always independent of each other, it is not clear how to define a similar notion for annotated PDS, since combining runs due to a push n cannot exploit that the collapse links "pointed to the same stack".

We then define Γ ′ to be the saturation function Γ with the additional constraint that a transition q a --→

Q br (Q 1 , . . . , Q n ) is not added if |Q n | > 1.
Clearly saturation by Γ ′ remains sound, since it contains a subset of the transitions of the automaton produced by saturation with Γ . Hence, we only need to prove that the automaton remains complete. We have the following lemma. Intuitively, the automaton remains correct because a collapse link at order-n can only be used once, whereas, at lower orders, a push k operation may make different copies of a link (with different targets). Hence, lower order links need alternation to keep track of the different uses of the link throughout the run.

Lemma 8 (Completeness of Γ ′ ). Given a non-alternating collapsible PDS C and an order-n stack automaton A 0 that is non-alternating at order-n, the automaton A constructed by saturation with Γ ′ is such that p, w ∈ P re * C (A 0 ) implies w ∈ L qp (A).

Proof. The proof is by induction over α such that p, w ∈ P re α C (A 0 ). We prove simultaneously during the induction that all p, w ∈ P re * C (A 0 ) have an accepting run from q p of A over the graph of w such that no node is labelled by Q ⊆ Q n and |Q| > 1.

Henceforth, for convenience, we will refer to non-alternation at order-n as simply non-alternation.

In the base case, we have w ∈ L qp (A 0 ) and the existence of a non-alternating run of A 0 , and thus a run in A comes directly from the non-alternating run of A 0 .

Hence, inductively assume p, w -→ ′ , w ′ and a non-alternating accepting run of w ′ from q p ′ of A via a rule (p, top 1 (w), o, p ′ ). Hence w ′ = o(w).

1. When o = pop k , let q p ′ q k -→ (Q 1 , . . . , Q k+1 ) be the order-n to order-k part of the initial transition accepting w ′ . We know, from the construction, we have the transition q p a -→ ∅ (∅, . . . , ∅, {q k } , Q k+1 , . . . , Q n ). Let w = u k-1 : k u k : (k+1) • • • : n u n . We know w ′ = u k : (k+1) • • • : n u n and the run from q k over w ′ is accepting and non-alternating. Hence, via the transition from q p we get an accepting run of w which labels all nodes in w ′ with the same nodes as the accepting run of w ′ from q k . Since the transitions reading u k-1 are all to the empty-set, this gives us a run over w that remains non-alternating. 2. When o = push k , let w = u k-1 : k • • • : n u n . We know

w ′ = u k-1 : k u k-1 : k u k : (k+1) • • • : n u n . Let q p ′ a --→ Q br (Q 1 , . . . , Q k , . . . , Q n ) and Q k a --→ Q ′ br (Q ′ 1 , . . . , Q ′ k )
be the initial transitions used on the run of w ′ (where the transition from Q k reads the second copy of u k-1 ). From the construction we the have a transition

q p a ------→ Q br ∪Q ′ br Q 1 ∪ Q ′ 1 , . . . , Q k-1 ∪ Q ′ k-1 , Q ′ k , Q k+1 , . . . , Q n .
Since we know u k : (k+1) • • • : n u n is accepted from Q ′ k via Q k+1 , . . . Q n , and we know that u k-1 is accepted from Q 1 , . . . , Q k-1 and Q ′ 1 , . . . , Q ′ k-1 via a-transitions with collapse links Q br and Q ′ br respectively, we obtain an accepting run of w. Since we know that the destinations of the collapse links that go outside of u k-1 (in particular, the order-n links) always point to the same stacks in both copies of u k-1 in the non-alternating accepting run of w ′ , we know that the run thus defined from q p is both accepting and non-alternating. We remark that, while this is always the case for order-n links, it is not always the case for order-k links with k < n, and hence, alternation is needed at orders lower than n. -→ (Q k+1 , . . . , Q n ) in A be the initial transition on the accepting run of w ′ . We know from the construction that we have the transition q p a ---→ {q k } (∅, . . . , ∅, Q k+1 , . . . , Q n ).

We know the run from q k via Q k+1 , . . . , Q n over w ′ is accepting and nonalternating. Hence, via the transition from q p we get an accepting run of w which labels all nodes in w ′ with the same nodes as the accepting run of w ′ from q k (by following the collapse link). Since the transition reading u 1 k-1 is to the empty set, this immediately allows us to label u 2 k-1 , . . . , u ℓ k-1 with empty sets, giving us a run over w that remains non-alternating.

When o = push k b , let w = u k-1 : k u k : k+1 • • • : n u n . We know

w ′ = push k b (w) is b u k : 1 u k-1 : k • • • : n u n . Let q p ′ b --→ Q br (Q 1 , . . . , Q n ) and Q 1 a --→ Q ′ br Q ′ 1
be the first transitions used on the accepting, non-alternating run of w ′ . From the construction we have q p a --→

Q ′ br (Q ′ 1 , Q 2 , . . . , Q k ∪ Q br , .
. . , Q n ) from which we can construct an accepting run of w (which is w ′ without the first b on top of the top order-1 stack). To see that the run is non-alternating, we observe that Q k ∪Q br results in the same labelling on the nodes of the graph of w as in corresponding run over w ′ . Apart from the labelling of the initial nodes (which label the beginning of each top k stack), the run over w is identical to the run over w ′ , and hence, non-alternating. This gives us a algorithm running in (n -1)-EXPTIME, since by avoiding alternation at order-n, we reduce the size of the automaton by a single exponential. Proposition 6. The saturation construction using Γ ′ for a non-alternating ordern collapsible PDS C and an order-n stack automaton A 0 that is non-alternating at order-n terminates in (n -1)-EXPTIME.

w 1

 1 |= Q 1 , . . . , w n |= Q n , and u |= Q br , and the soundness of Q a

3 .

 3 When o = collapse k , let w = u 1 k-1 : k • • • : k u ℓ k-1 : k u k : (k+1) • • • : n u n where w ′ = u k : (k+1) • • • : n u nis the stack pointed to by the order-k collapse link of top 1 (w). Let q p ′ q k

5 .

 5 When o = rew b let q p ′ b --→ Q br (Q 1 , . . . , Q n ) bethe first transition on the nonalternating accepting run of w ′ = b : 1 v for some v. From the construction we know we have a transition q p a --→ Q br (Q 1 , . . . , Q n ), from which we get an accepting, non-alternating run of w = a : 1 v as required.Hence, for every p, w ∈ P re * C (A 0 ) we have w ∈ L qp (A) via a non-alternating run.

Kartzow and Parys have independently introduced a similar model[START_REF] Kartzow | Parys Strictness of the Collapsible Pushdown Hierarchy[END_REF].

Hence automata cannot accept empty stacks from initial states. This can be overcome by introducing a bottom-of-stack symbol.

⋆ This work was supported by the Fondation Sciences Mathématiques de Paris and by the following projects: AMIS (ANR 2010 JCJC 0203 01 AMIS), FREC (ANR 2010 BLAN 0202 02 FREC) and VAPF (Région Île de France).