Jérôme Leroux

M Praveen

Grégoire Sutre

Hyper-Ackermannian Bounds for Pushdown Vector Addition Systems

This paper studies the boundedness and termination problems for vector addition systems equipped with one stack. We introduce an algorithm, inspired by the Karp & Miller algorithm, that solves both problems for the larger class of well-structured pushdown systems. We show that the worst-case running time of this algorithm is hyper-Ackermannian for pushdown vector addition systems. For the upper bound, we introduce the notion of bad nested words over a well-quasi-ordered set, and we provide a general scheme of induction for bounding their lengths. We derive from this scheme a hyper-Ackermannian upper bound for the length of bad nested words over vectors of natural numbers. For the lower bound, we exhibit a family of pushdown vector addition systems with finite but large reachability sets (hyper-Ackermannian).

I. INTRODUCTION

Vector addition systems (VAS) are an important class of well-structured transition systems. They are powerful enough to model concurrent infinite-state systems but still many important properties are decidable, like boundedness, termination and reachability. Adding more power to VAS while retaining decidability is an active area of research (see, e.g., [START_REF] Dufourd | Reset nets between decidability and undecidability[END_REF], [START_REF] Finkel | A well-structured framework for analysing Petri net extensions[END_REF], [START_REF] Reinhardt | Reachability in petri nets with inhibitor arcs[END_REF], [START_REF] Demri | The covering and boundedness problems for branching vector addition systems[END_REF], [START_REF] Ganty | Algorithmic verification of asynchronous programs[END_REF], [START_REF] Atig | Approximating petri net reachability along context-free traces[END_REF]). Techniques developed for VAS are often extended to the more general class of well-structured systems. In this work, we extend the power of VAS by adding one stack. We give decidability and complexity results, and show how these fit in the general scheme of well-structured systems.

It is well known that a finite-state machine equipped with two stacks is Turing powerful. Replacing one of the stacks by multiple stacks over a singleton stack alphabet (and without bottom test) will result in VAS with one stack, which we study here. This model is close to the border of undecidability and very little is known about the decidability of many problems. Here we prove that the boundedness and termination problems are decidable for this model. The basis of these results is the reduced reachability tree, which is also the basis for many results about VAS and well-structured systems. Our main contributions are twofold.

First, we introduce well-structured pushdown systems, of which pushdown VAS are an important class. We extend the well-known reduced reachability tree technique for wellstructured transition systems [START_REF] Finkel | Reduction and covering of infinite reachability trees[END_REF] to the pushdown case. The reduced reachability tree allows us to decide the boundedness and termination problems for well-structured pushdown systems.

Second, we give hyper-Ackermannian upper and lower bounds for the size of the reduced reachability trees of pushdown VAS. For the upper bound, we introduce the notion of bad nested words over a well-quasi-ordered set, and we provide a general scheme of induction for bounding their lengths. We derive from this scheme a hyper-Ackermannian upper bound for the length of bad nested words over vectors of natural numbers. For the lower bound, we exhibit a family of pushdown vector addition systems with finite but large reachability sets (hyper-Ackermannian).

Many decidability results about well-structured systems depend on the behavior of well-quasi-orders. In the presence of a stack, making these work require new insights, as done in our results mentioned above. While results like Dickson's lemma and Higman's lemma can prove decidability of some algorithms, deriving complexity bounds for such algorithms has recently received attention [START_REF] Chambart | The ordinal recursive complexity of lossy channel systems[END_REF], [START_REF] Figueira | Ackermannian and primitive-recursive bounds with Dickson's lemma[END_REF], [START_REF] Haase | The power of priority channel systems[END_REF]. Such bounds help to compare the power of different models and understand the structure of the models under study. Again, making these work in the presence of a stack require substantial extensions, as we have done for deriving bounds for the size of the reduced reachability tree. In particular, we extend the framework for deriving bounds on bad sequences [START_REF] Figueira | Ackermannian and primitive-recursive bounds with Dickson's lemma[END_REF] to bad nested sequences [START_REF] Alur | Adding nesting structure to words[END_REF].

The upper and lower bounds that we derive in this paper for the size of the reduced reachability tree do not apply for the complexity of the problems themselves, since there may be better algorithms. The best known lower bound is the nonelementary lower bound given by [START_REF] Lazic | The reachability problem for vector addition systems with a stack is not elementary[END_REF]. Very few upper bounds are known and none of them match this lower bound. Closing these gaps are challenging open problems.

Related work. In [START_REF] Bouajjani | Analysis of recursively parallel programs[END_REF], a model called RVASS is introduced, which allows vector additions during stack operations. However, the semantics of this model resembles that of branching VAS [START_REF] Demri | The covering and boundedness problems for branching vector addition systems[END_REF] rather than that of a VAS with a stack. In [START_REF] Cai | Well-structured pushdown systems[END_REF], a different version of well-structured pushdown systems are introduced, which are systems where both the set of control states and the stack alphabet can be infinite and are wellquasi-ordered. They consider the coverability problem for subclasses. In contrast, the model we consider here has a finite stack alphabet and we consider termination and boundedness for the whole class. In [START_REF] Abdulla | Push-down automata with gap-order constraints[END_REF], the authors introduce a model called pushdown automata with data and prove that the control state reachability problem is decidable. In this model again, the set of messages that can be pushed onto the stack can be infinite. The authors introduce a well-quasi-order on this set to decide control state reachability. It is not clear whether the techniques developed for models with infinite stack alphabet can be used in our model and vice-versa. A general framework for wellstructured transition systems with auxiliary storage has been introduced in [START_REF] Chadha | Decidability results for well-structured transition systems with auxiliary storage[END_REF]. Decidability is shown for the coverability problem in some subclasses that have a ranking function compatible with the transition relation. Our focus on the other hand is specifically on reduced reachability trees and deriving upper bounds for algorithms based on them. The authors of [START_REF] Chadha | Decidability results for well-structured transition systems with auxiliary storage[END_REF] extend their work in [START_REF] Chadha | Deciding branching time properties for asynchronous programs[END_REF] to decide some branching properties of asynchronous programs. They prove that termination and other problems are decidable for our model, provided counters are decreased only when the stack is empty. A similar restriction is imposed by the authors of [START_REF] Sen | Model checking multithreaded programs with asynchronous atomic methods[END_REF] on their model called multiset pushdown systems, closely related to our model. We do not impose such restrictions. The fundamental techniques used for deriving Ackermannian and hyper-Ackermannian bounds are developed mostly in [START_REF] Figueira | Ackermannian and primitive-recursive bounds with Dickson's lemma[END_REF], [START_REF] Schmitz | Multiply-recursive upper bounds with Higman's lemma[END_REF], on top of which we develop techniques for working with the stack.

Outline. We present in Section III our reduced reachability tree technique1 for well-structured pushdown systems. Section IV provides a general scheme of induction for bounding the length of bad nested words. Basic notions on fast growing functions are recalled in Section V. We derive in Section VI a multiply-recursive upper bound for the length of bad nested sequences over N d . Section VII shows that the worst-case size of the reduced reachability tree is hyper-Ackermannian for pushdown VAS.

II. PRELIMINARIES

A quasi-order on a set S is a binary relation on S that is reflexive and transitive. As usual, we write s ≺ t when s t and t s. A partial-order is an antisymmetric quasi-order.

A well-quasi-order (wqo) on S is a quasi-order such that every infinite sequence s 0 , s 1 , s 2 , . . . in S contains an infinite nondecreasing subsequence

s i0 s i1 s i2 • • • (with i 0 < i 1 < i 2 • • • ).
The concatenation of a finite sequence (resp. word) σ with a finite or infinite one w is denoted by σ, w (resp. σ • w). The length of a finite sequence or word σ is denoted |σ|.

III. WELL-STRUCTURED PUSHDOWN SYSTEMS

A pushdown system is a 4-tuple P = S, s init , Γ, ∆ where S is a set of states, s init ∈ S is the initial state, Γ is a finite stack alphabet, and ∆ ⊆ S × Op × S is a set of rules. The set Op of operations is given by Op = {ε} ∪ {push(γ), pop(γ) | γ ∈ Γ}. Observe that we do not require S to be finite. Informally, a rule (s, op, t) means that the pushdown system can move from state s to state t by performing the operation op on the stack. We say that P is finitely-branching if the set {(op, t) | (s, op, t) ∈ ∆} is finite for every state s ∈ S. A simulation relation for P is any binary relation R on S satisfying the following condition: for every (s, op, t) ∈ ∆ and s ′ ∈ S such that (s, s ′ ) ∈ R, there exists t ′ ∈ S such that (s ′ , op, t ′ ) ∈ ∆ and (t, t ′ ) ∈ R.

We define the operational semantics of a pushdown system P = S, s init , Γ, ∆ as follows. A configuration is a pair χ = (s, σ) where s ∈ S is a state and σ ∈ Γ * is a word denoting the contents of the stack. The initial configuration is χ init = (s init , ε). The transition relation is the least binary relation → ⊆ (S × Γ * ) × (S × Γ * ) satisfying the following rules:

(s, ε, t) ∈ ∆ (s, σ) → (t, σ) (s, push(γ), t) ∈ ∆ (s, σ) → (t, σ • γ) (s, pop(γ), t) ∈ ∆ (s, σ • γ) → (t, σ)
A run is a (finite or infinite) sequence χ 0 , χ 1 , χ 2 , . . . of configurations such that χ 0 = χ init and χ i-1 → χ i for every index i > 0 of the sequence. The reachability set is the set of all configurations that occur on some run.

We investigate two verification questions on pushdown systems, namely termination and boundedness. The former asks whether all runs of a given pushdown system are finite, and the latter asks whether its reachability set is finite. Recall that these questions are decidable for pushdown systems with finitely many states. In our setting, the set of states may be infinite (e.g., Q×N d for pushdown vector addition systems with states, see Section VII). By extending well-known techniques from the theory of well-structured transition systems [START_REF] Finkel | Reduction and covering of infinite reachability trees[END_REF], [START_REF] Abdulla | Algorithmic analysis of programs with well quasi-ordered domains[END_REF], [START_REF] Finkel | Well-structured transition systems everywhere![END_REF], we obtain a class of pushdown systems for which termination and boundedness are decidable.

Definition III.1. A well-structured pushdown system is a finitely-branching pushdown system P = S, s init , Γ, ∆ equipped with a well-quasi-order ⊆ S × S on states such that is a simulation relation for P.

Remark III.2. The monotonicity condition of Definition III.1 matches the one given in [START_REF] Abdulla | Algorithmic analysis of programs with well quasi-ordered domains[END_REF] for infinite-state labeled transition systems. In our setting, the labels of [START_REF] Abdulla | Algorithmic analysis of programs with well quasi-ordered domains[END_REF] are operations op ∈ Op. More general monotonicity conditions have been proposed in [START_REF] Finkel | Well-structured transition systems everywhere![END_REF] for unlabeled infinite-state transition systems. The condition of Definition III.1 corresponds to the strong compatibility requirement of [START_REF] Finkel | Well-structured transition systems everywhere![END_REF].

The reachability tree of a well-structured pushdown system P = S, s init , Γ, ∆, is the directed unordered tree defined as follows. Nodes of the tree are labeled by configurations of P. The root r is labeled by the initial configuration χ init , written r : χ init . Each node n : χ has one child m : ψ for each configuration ψ such that χ → ψ. Note that the reachability tree of P is finitely branching.

The reachability tree is usually infinite for well-structured pushdown systems. We show how to truncate it while preserving enough information to decide termination and boundedness. A node n : (s, σ) subsumes a node m : (t, τ ) if n is a proper ancestor of m, s t and σ is a prefix of σ ′ for every node n ′ : (s ′ , σ ′ ) on the path from n to m. The reduced reachability tree of P is the largest prefix of the reachability tree such that every subsumed node has no child.

Proposition III.3. The reduced reachability tree of any wellstructured pushdown system is finite.

Proof. Consider a well-structured pushdown system P = S, s init , Γ, ∆, . By contradiction, assume that its reduced reachability tree T is infinite. Recall that this tree is finitely branching. By König's lemma, T contains an infinite branch n 0 : (s 0 , σ 0 ) → n 1 : (s 1 , σ 1 ) → n 2 : (s 2 , σ 2 ) → • • • . Observe that σ 0 = ε since n 0 is the root of the tree. We extract from n 0 , n 1 , n 2 , . . . an infinite subsequence n i0 , n i1 , n i2 , , . . . defined as follows:

i 0 = 0 i k+1 = min {i > i k | ∀j > i k , |σ i | ≤ |σ j |} By definition, |σ i k | ≤ |σ j | for all j, k ∈ N with i k ≤ j.
It follows from the operational semantics of pushdown systems that σ i k is a prefix of σ j for all j, k ∈ N with i k ≤ j. Since is a well-quasi-order, there exists k < l such that s i k s i l . We obtain that the node n i k subsumes the node n i l . This entails that n i l has no child in T , which is impossible.

Proposition III.4. A well-structured pushdown system P has an infinite run if, and only if, its reduced reachability tree contains a subsumed node.

Proof. If P has an infinite run, then its reachability tree contains an infinite branch. Since the reduced reachability tree of P is finite, this infinite branch necessarily contains a subsumed node. Hence, the reachability tree of P contains a subsumed node, and so does its reduced reachability tree. For the converse, assume that the reachability tree of P contains a subsumed node. The path from the root to this subsumed node yields a run

(s 0 , σ 0 ) op 1 --→ • • • op k --→ (s k , σ k ) op k+1 ----→ • • • op l --→ (s l , σ l )
such that k < l, s k s l and σ k is a prefix of σ j for all k ≤ j ≤ l. Here, we have decorated each transition of the run with its associated operation. Let z k , . . . , z l be the words satisfying

σ j = σ k • z j for all k ≤ j ≤ l. Define (t k , τ k ) = (s l , σ l ).
Since s k t k and is a simulation relation for P, we derive that there exists t k+1 , . . . , t l such that, for every k < j ≤ l, s j t j and (t j-1 , op j , t j ) ∈ ∆. Observe that the sequence of operations op k+1 , . . . , op l never pops from σ k . Hence, we may also perform op k+1 , . . . , op l starting from σ l = τ k • z k . So the above run may be extended by appending

(s l , σ l ) = (t k , τ k • z k ) op k+1 ----→ • • • op l --→ (t l , τ k • z l )
We obtain an infinite run by repeating this construction.

The boundedness problem requires stronger monotonicity requirements. A well-structured pushdown system P = S, s init , Γ, ∆, is called strict when is a partial order and ≺ is a simulation relation. Similarly, in the reachability tree of P, a node n : (s, σ) strictly subsumes a node m : (t, τ ) if n subsumes m, and s ≺ t or |σ| < |τ |.

Proposition III.5. A strict well-structured pushdown system P has an infinite reachability set if, and only if, its reduced reachability tree contains a strictly subsumed node.

Proof. Assume that P has an infinite reachability set. Let T be the largest prefix of its reachability tree such that, on each branch, all nodes have distinct labels. The tree T is infinite since every configuration in the reachability set is the label of some node in T . By König's lemma, it follows that the reachability tree of P contains an infinite branch where all nodes have distinct labels. Since the reduced reachability tree of P is finite, this infinite branch necessarily contains two nodes n : (s, σ) and m : (t, τ ), both contained in the reduced reachability tree, such that n subsumes m. Recall that (s, σ) = (t, τ ). If |σ| < |τ | then n strictly subsumes m. Otherwise, σ = τ since σ is a prefix of τ . It follows that s = t, which entails that s ≺ t as is a partial order. We get, again, that n strictly subsumes m.

For the converse, assume that the reduced reachability tree of P contains a strictly subsumed node. The path from the root to this subsumed node yields a run

(s 0 , σ 0 ) op 1 --→ • • • op k --→ (s k , σ k ) op k+1 ----→ • • • op l --→ (s l , σ l ) such that k < l, s k s l , σ k is a prefix of σ j for all k ≤ j ≤ l, and s k ≺ s l or |σ k | < |σ l |.
With the same arguments as in the proof of Proposition III.4, we extend this run into an infinite one by iterating the sequence of operations op k+1 , . . . , op l . If s k ≺ s l then the resulting infinite run visits infinitely many states (as is a partial order). If |σ k | < |σ l | then it visits infinitely many stack contents. In both cases, we obtain that P has an infinite reachability set.

IV. BAD NESTED SEQUENCES OVER A WQO SET

Nested words [START_REF] Alur | Adding nesting structure to words[END_REF] offer a convenient formalism to study some properties of pushdown systems. Since we are dealing with sets of reachable configurations, our notation is slightly different from that of [START_REF] Alur | Adding nesting structure to words[END_REF], where the main concern is the theory of languages. For us, an alphabet S is usually the set of states of a pushdown system, and the content of the stack is abstracted by its length.

Definition IV.1. A nested sequence over a set S is a (finite or infinite) sequence (s 0 , h 0 ), (s 1 , h 1 ), . . . of elements in S × N satisfying h 0 = 0 and h j ∈ h j-1 + {-1, 0, 1} for every index j > 0 of the sequence.

Example IV.2. The empty sequence is a nested sequence. The nested sequence (a, 0), (b, 1), (c, 2), (d, 1) over {a, b, c, d} can be depicted as follows: [START_REF] Alur | Adding nesting structure to words[END_REF]. In a well-structured pushdown system, every run can be seen as a nested sequence, by mapping each configuration (s, σ) to the pair (s, |σ|). Similarly, every branch of the reachability tree can be seen as a nested sequence.

2- c 1- b d 0-a Remark IV.
Definition IV.4. A nested sequence (s 0 , h 0 ), (s 1 , h 1 ), . . . over a quasi-ordered set (S, ) is said to be good if there exists i < j such that s i s j and h i+1 , . . . , h j ≥ h i . A bad nested sequence is one that is not good.

Example IV.5. The following nested sequence over (N, ≤) is bad:

3- 0 2- 1 0 0 1- 2 1 1 0 0 0-3 2 1 0
Remark IV.6. A nested sequence (s 0 , 0), (s 1 , 0), . . . is good iff s i s j for some i < j. Hence good/bad nested sequences are generalizations of good/bad (non-nested) sequences [START_REF] Figueira | Ackermannian and primitive-recursive bounds with Dickson's lemma[END_REF].

Remark IV.7. Consider a branch in the reachability tree of some well-structured pushdown system. The nested sequence associated with the branch is good if, and only if, the branch contains a subsumed node.

Lemma IV.8. Bad nested sequences over a wqo are finite.

Proof. Similar to the proof of Proposition III.3.

The finiteness of the reduced reachability tree presented in the previous section relies on the finiteness of bad nested sequences. In order to derive complexity arguments, bounds on these sequences must be obtained. Normed wqo sets provide a framework for deriving such bounds. We first present some simple examples of (non-nested) bad sequences that motivate normed wqo sets.

The following nested sequence shows that the length of bad nested sequences over a wqo cannot be bounded since there exist bad nested sequences over (N, ≤) of length n for every n. 0-100 99 98 . . . 1 0 Hence, the initial element must be bounded somehow. In the algorithms presented in the previous section, nested sequences starts from the same element, the initial state of the wellstructured pushdown system. However, even if the initial element is fixed, the problem is not yet solved as shown by the following bad nested sequence over (N 2 , ≤).

0-(0, 1) (100, 0) (99, 0) (98, 0) . . . (1, 0) (0, 0)
This problem appears because the second element of the sequence is arbitrarily large compared to the first one. In order to control the growth of values in a nested sequence, we use the notion of normed wqo sets. Example IV.10. The wqo set (N d , ≤) is normed by the function that maps any vector to its largest component.

Definition IV.11. A nested sequence (s 0 , h 0 ), (s 1 , h 1 ), . . . over a normed wqo set (S, , ||.||) is said to be n-controlled for some n ∈ N if ||s j || ≤ n + j for every index j of the sequence.

While there exist bad nested sequences of arbitrarily long lengths, König's lemma shows that there exists a maximal length for n-controlled bad nested sequences. Indeed, these sequences can be organized in a forest where nodes are labeled by elements in S × N. By definition of the norm function, this forest is finite branching and the number of roots is finite. Hence, if the forest is infinite, the König's lemma shows that it contains an infinite branch. Since infinite nested sequences are good we get a contradiction.

Let BAD S (n) be the set of n-controlled bad nested sequences over S. This set is non empty since it contains the empty sequence. The maximal length function L S : N → N is defined as follows:

L S (n) = max{|w| | w ∈ BAD S (n)}
The maximal length function L S satisfies a recurrence relation that we call the descent equation. For this, we need the set S| ≤n defined as follows:

S| ≤n = {s ∈ S | ||s|| ≤ n}
Given s ∈ S| ≤n , let us denote by BAD S,s (n) the set of ncontrolled bad nested sequences starting from (s, 0). This set is non-empty since it contains (s, 0). Let L S,s (n) be the number defined as follows:

L S,s (n) = max{|w| | w ∈ BAD S,s (n)}
The following equality is immediate for every n ∈ N such that S| ≤n is non empty:

L S (n) = max s∈S| ≤n L S,s (n)
Let (S/s, , ||.||) be the normed wqo set where S/s (called the quotient of S by s ∈ S) is defined as S/s = {t ∈ S | s t}. In the following, we prove the following equality, called the descent equation for every n ∈ N and for every s ∈ S| ≤n :

L S,s (n) = 1 + L S/s (n + 1) + L S/s (n + 1 + L S/s (n + 1))
Let us first prove that L S,s (n) is bounded by the above term. We pick a n-controlled bad nested sequence w over S starting from (s, 0) with s ∈ S| ≤n . The nested sequence w can be decomposed into w = (s, 0)w ′ where w ′ is a sequence of elements in S × N. Since w is bad, w ′ is in fact a sequence of elements in (S/s)×N. Let us introduce the maximal prefix w ′′ of w ′ such that w ′′ is a sequence of elements in S × (N\{0}). Let us show that |w ′ | ≤ L S/s (n + 1). The sequence w ′′ can be decomposed into w ′′ = (s 1 , h 1 ), . . . , (s k , h k ) where k = |w ′′ |. Note that (s 1 , h 1 -1), . . . , (s k , h k -1) is a (n + 1)controlled bad nested sequence over the wqo set S/s. Thus, |w ′′ | ≤ L S/s (n + 1). Now, let us consider the sequence w ′′′ such that w ′ = w ′′ , w ′′′ . Let us prove that |w ′′′ | ≤ L S/s (n + 1 + k). Observe that if w ′′′ is empty the relation is immediate. So, let us assume that w ′′′ is non empty. By maximality of w ′′ , we deduce that w ′′′ starts with an element in S × {0}. Thus w ′′′ is a (n + 1 + k)-controlled bad nested sequence over S/s. We get |w ′′ | ≤ L S/s (n + 1 + k). Since L S/s is monotonic and k ≤ L S/s (n + 1), we deduce that |w ′′′ | is bounded by L S/s (n + 1 + L S/s (n + 1)). Hence |w| is bounded by 1+L S/s (n+1)+L S/s (n+1+L S/s (n+1)). We have proved one inequality of the descent equation, namely that L S,s (n) is bounded by 1 + L S/s (n + 1) + L S/s (n + 1 + L S/s (n + 1)) for every n ∈ N and for every s ∈ S| ≤n .

To prove the converse inequality, we need to concatenate bad nested sequences. The concatenation will be possible thanks to the following lemma.

Lemma IV.12. Every w ∈ BAD S (n) with |w| = L S (n) is either empty or the last element is in S × {0}.

Proof. If L S (n) = 0, then the proof is immediate. Assume that L S (n) > 0 and let us consider a n-controlled bad nested sequence w such that |w| = L S (n). Let (s, h) be the last element of w. By contradiction, suppose that h > 0.

It is readily seen that the sequence obtained by appending (s, h -1) to w is also a n-controlled bad nested sequence. This contradicts the maximality of w. We derive that h = 0, which concludes the proof of the lemma.

Let us now complete the proof of the descent equation, by showing that 1 + L S/s (n + 1) + L S/s (n + 1 + L S/s (n + 1)) is bounded by L S,s (n) for every n ∈ N and for every s ∈ S| ≤n . Pick n ∈ N and s ∈ S| ≤n . Let n 1 = L S/s (n + 1). There exists w 1 ∈ BAD S/s (n + 1) with |w 1 | = n 1 . According to Lemma IV.12, if n 1 > 0 then the last element of w 1 is in S × {0}. Let n 2 = L S/s (n + 1 + n 1 ). By definition, there exists w 2 in BAD S/s (n+1+n 1 ) with |w 2 | = n 2 . We introduce the nested sequence w = (s, 0), w ′ 1 , w 2 where w ′ 1 is obtained from w 1 by replacing every occurrence of (t, h) ∈ S × N by (t, h + 1). Observe that w is a bad nested sequence that is n-controlled. Since w ∈ BAD S,s (n), we get L S,s (n) ≥ |w|. It follows that 1 + L S/s (n + 1) + L S/s (n + 1 + L S/s (n + 1)) is bounded by L S,s (n), which concludes the proof of the descent equation.

In order to simplify the presentation of the descent equation, we introduce the function K S : N → N defined for every n ∈ N as follows:

K S (n) = n + L S (n)
Intuitively, K S (n) explicitly accounts for the starting value n by adding it to L S (n). It is understood that, like L S , the function K S is parametrized by a normed wqo set (S, , ||.||). Now, just observe that for every n ∈ N and every s ∈ S| ≤n , the descent equation entails that:

n + L S,s (n) = n + 1 + L S/s (n + 1) + L S/s (n + 1 + L S/s (n + 1)) = K S/s (K S/s (n + 1))
In particular, if S| ≤n is non empty, we obtain that:

K S (n) = n + L S (n) = n + max s∈S| ≤n L S,s (n) = max s∈S| ≤n n + L S,s (n) = max s∈S| ≤n K S/s (K S/s (n + 1))
We have proved the following theorem.

Theorem IV.13. For every normed wqo set (S, , ||.||) and for every n ∈ N, we have:

K S (n) = max s∈S| ≤n K S/s (K S/s (n + 1)) if S| ≤n = ∅ n otherwise V. FAST GROWING FUNCTIONS
The next sections classify the maximal length function in the fast-growing hierarchy [START_REF] Löb | Hierarchies of number-theoretic functions[END_REF]. We shall work with set-theoretic ordinals less than ω ω , written in Cantor's Normal Form. Each limit ordinal λ has a canonical fundamental sequence

(λ n ) n∈N , satisfying λ 0 < λ 1 < • • • < λ n < λ n+1 < • • • , with
λ being the supremum of this sequence. For limit ordinals below ω ω , this fundamental sequence is given by

(ω d . a d + • • • + ω r . a r ) n = ω d . a d + • • • + ω r+1 . a r+1 + ω r . (a r -1) + ω r-1 . (n + 1)
assuming d ≥ r and a r > 0.

The family of fast growing functions (F α ) α , indexed by ordinals α ≤ ω ω , is defined as follows:

F 0 (n) = n + 1, F α+1 (n) = F n+1 α (n) = n+1 times F α (F α (• • • F α (n) • • • )) F λ (n) = F λn (n) if λ < ω ω is a limit ordinal F ω ω (n) = F ω n+1 (n)
The value F 1 (n) is linear in n, F 2 (n) is exponential in n, and F 3 (n) is a tower of exponential of height n. The function F ω is an Ackermannian function. This function is defined by diagonalization over the ordinals α < ω, since F ω (n) = F n+1 (n). The hyper-Ackermannian function F ω ω used in this paper is defined in the same fashion, by diagonalization over the ordinals α < ω ω .

Example V.1. The above definition induces:

F ω 2 .4 (8) = F ω 2 .3+ω.9 (8) = F ω 2 .3+ω.8+9 (8) = F ω 2 .3+ω.8+8 (• • • (F ω 2 .3+ω.8+8 9 times (8)) • • • )
In addition to the usual linear order ≤ on ordinals, we will also use a partial order, called embedding in [START_REF] Chambart | The ordinal recursive complexity of lossy channel systems[END_REF], and defined as follows. For two ordinals α, β such that α

= ω d . a d + • • • + ω 0 . a 0 and β = ω d . b d + • • • + ω 0 . b 0 , α embeds in β if a i ≤ b i
for all i ∈ {0, . . . , d}. We write α ⊑ β when α embeds in β. We will use the following monotonicity properties of fast growing functions. These properties are shown by induction over ordinals (see, for instance, Lemmas 2.1 and 2.2 in [START_REF] Chambart | The ordinal recursive complexity of lossy channel systems[END_REF]). Lemma V.2 (Monotonicity, [START_REF] Chambart | The ordinal recursive complexity of lossy channel systems[END_REF]). For all ordinals α, β < ω ω and for all natural numbers m, n ∈ N,

α ⊑ β and m ≤ n ⇒ m < F α (m) ≤ F β (n) VI. BAD NESTED SEQUENCES OVER N d
In this section, we derive upper bounds for the length of bad nested sequences over multiple disjoint copies of N d . The sum of c ∈ N distinct copies of N d is the Cartesian product {1, . . . , c} × N d , denoted by c × N d . This set naturally corresponds to states of vector addition systems with c locations and d counters ranging over the natural numbers. The set c × N d is equipped with the wqo c×N d defined by (p, u) c×N d (q, v) if p = q and u ≤ v, and the norm ||.|| c×N d defined by ||(q, v)|| c×N d = ||v|| ∞ , where ||v|| ∞ maps v to its largest component (to zero for the empty vector). In this section, we prove the following theorem.

Theorem VI.1. For every c, d ≥ 1 and n ≥ 2, we have:

L c×N d (n) ≤ F ω d .c (d.n)
Remark VI.2. The previous theorem requires d ≥ 1. When d = 0, the norm of any element in c × N 0 is zero, so the value L c×N 0 (n) does not depend on n. Let us denote by k c this value. As the quotient of c × N 0 by an element v ∈ c × N 0 is equal to (c-1)×N 0 , Theorem IV. [START_REF] Figueira | Ackermannian and primitive-recursive bounds with Dickson's lemma[END_REF] shows that k c = 2k c-1 +1 for every c ≥ 1. From k 0 = 0, we derive k c = 2 c -1 which proves the following equality:

L c×N 0 (n) = 2 c -1
The rest of this section is the technical part for proving Theorem VI.1. In particular, we assume that d ≥ 1. Our approach is based on the descent equation introduced in Theorem IV. [START_REF] Figueira | Ackermannian and primitive-recursive bounds with Dickson's lemma[END_REF]. This approach introduces sums of multiple disjoint copies of sets N i for various dimensions i ∈ {0, . . . , d}. Let us show this property on the normed wqo set N d (no multiple copy). The descent equation introduces the quotients N d /v where v ∈ N d . A vector x in such a quotient satisfies x(j) ∈ {0, . . . v(j)-1} for some index j. Hence, the quotient N d /v can be embedded into (v(1) +

• • • + v(d)) × N d-1
. By applying recursively the descent equation, starting from c × N d , finite sums of disjoint copies of sets N i for various dimensions i ∈ {0, . . . , d} are introduced.

Those finite sums are denoted formally thanks to the notion of types introduced in [START_REF] Figueira | Ackermannian and primitive-recursive bounds with Dickson's lemma[END_REF]. We refer to this paper for further explanations. A type is a function τ : {0, . . . , d} → N, also viewed as a multiset. We associate to a type τ the set N τ defined as follows:

N τ = d i=0 τ (i) × N i
The set N τ is equipped with a wqo τ and a norm ||.|| τ by observing that the sets τ (i) × N i are pairwise disjoint. More formally, the wqo τ on N τ is defined by u τ v if there exists i such that u, v ∈ τ (i) × N i and u τ (i)×N i v, and the norm ||.|| τ is defined by

||v|| τ = ||v|| τ (i)×N i where i is such that v ∈ τ (i) × N i .
Since the structure (N τ , τ , ||.|| τ ) is a normed wqo, the function K N τ is well defined. To simplify notations, we denote this function by K τ . In the sequel, we assume that the reader is familiar with multiset notations. In particular, since a type is a multiset of natural numbers in {0, . . . , d}, we denote by ∅ the empty type that maps any i on zero. Given a type τ such that τ (i) ≥ 1, we denote by τ -{i} the type ̺ defined by

̺(i) = τ (i) -1 and ̺(j) = τ (j) if j = i.
Following the approach introduced in [START_REF] Figueira | Ackermannian and primitive-recursive bounds with Dickson's lemma[END_REF] (explained in the beginning of this section on the quotients N d /v), the quotients N τ /v, where v ∈ N τ , can be embedded into N ̺ for types ̺ derived from τ and v. These types are defined as follows. Given a type τ , a dimension i ∈ {0, . . . , d} such that τ (i) ≥ 1 and a natural number n ≥ 0, the derivation type ∂ i n (τ ) is defined by:

∂ i n (τ ) = τ -{i} + n. 0≤j<i {j}
We obtain the following lemma, whose proof (which can be found in the appendix) is similar to that of [13, Lemma A.3]:

Lemma VI.3. It holds that:

K N τ /v (m) ≤ K ∂ i d.n (τ ) (m
) for every type τ , for every i ∈ {1, . . . , d}, for every v ∈ τ (i) × N i , for every n ≥ ||v|| τ , and for every m ∈ N.

Combining this lemma with Theorem IV.13 and the fact that K τ is monotonic for all τ , we get the following inequalities, which hold for every natural number n ≥ 0, and for every type τ = ∅:

K τ (n) ≤ max i:τ (i)≥1 {K ∂ i d.n (τ ) (K ∂ i d.n (τ ) (n + 1
))} For a type τ , we denote by F τ the function defined by:

F τ = F ω d .τ (d)+•••+ω 0 .τ (0)
We associate to a type τ = ∅ and a natural number n ∈ N the type τ n = ∂ i n (τ ) where i is the minimal index such that τ (i) > 0. An immediate induction shows the following equality for every type τ = ∅:

F τ (n) = F n+1 τn (n)
In the sequel, we prove that for every type τ , for every n ≥ 2 we have:

K τ (n) ≤ F τ (d. n) (1)
Note that Theorem VI.1 is a direct consequence of this inequality with the type τ = c.{d}. We write τ ⊑ ̺ if τ (i) ≤ ̺(i) for all i. We will use the lexicographic order < on types, with τ (i + 1) being more significant than τ (i) for all i. This is a well-founded linear order, which is the same as the order used for types in [START_REF] Dershowitz | Proving termination with multiset orderings[END_REF], [START_REF] Figueira | Ackermannian and primitive-recursive bounds with Dickson's lemma[END_REF]. We first prove some results on the family (F τ ).

Lemma VI.4. For every type τ , for every i ∈ {0, . . . , d} such that τ (j) > 0 implies j ≥ i, and for every n ≥ 0:

F τ +{i} (n) ≥ F τ (2n)
Proof. The case n = 0 comes from F ̺ (0) = 1 for every type ̺ (the equality is obtained by induction on ̺ with the lexicographic order) . We introduce ̺ = τ +{i}. Since τ (j) > 0 implies j ≥ i, we have

̺ n = τ + n.({i -1} + • • • + {0}). Lemma V.2 provides F n ̺n (n) ≥ F n ∅ (n) = 2n. We have: F ̺ (n) = F n+1 ̺n (n) ≥ F ̺n (F n ∅ (n)) [Lemma V.2] ≥ F τ (2n) [Lemma V.2]
This concludes the proof of the lemma.

Notice that for every type τ = ∅ and for every n ≥ 0, the type τ n is equal to ∂ i n (τ ) where i is the minimal index such that τ (i) > 0. The following lemma shows that if we consider a larger index, we get a smaller value.

Lemma VI.5. For every type τ = ∅, for every i such that τ (i) > 0, and for every n ≥ 2, for every k ≥ n, we have:

F ∂ i n (τ ) (k) ≤ F τn (k) Proof. We decompose τ into τ = τ ′ + ̺ such that τ ′ (j) = 0 if j < i and ̺(j) = 0 if j ≥ i. Observe that ∂ i n (τ ) = τ ′ n + ̺. If ̺ = ∅ then i is the minimal index such that τ (i) > 0.
In this case the lemma is immediate. So, we can assume that ̺ = ∅. In this case

τ n = τ ′ + ̺ n . If ̺ n = ∅ then ̺ = {0} and F τn (k) = F τ ′ (k). Thus F ∂ i n (τ ) (k) = F τ ′ n +̺ (k) = F τ ′ n +{0} (k) = F k+1 τ ′ n (k) ≤ F k+1 τ ′ k (k) [Lemma V.2] = F τ ′ (k) = F τn (k)
Hence, we can assume that ̺ n = ∅. We introduce the norms

||̺ n || 1 = d j=0 ̺ n (j) and ||̺|| 1 = d j=0 ̺(j). Thus ||̺ n || 1 ≥ 1. Lemma VI.4 and Lemma V.2 show by induction that F τn (k) ≥ F τ ′ (m) where m = k.2 ||̺n||1 . Note that m ≥ k.(1 + ||̺ n || 1 ) ≥ k + (k -1).||̺ n || 1 + ||̺ n || 1 ≥ k + 1 + ||̺ n || 1 from k -1 ≥ 1 and ||̺ n || 1 ≥ 1. As ||̺ n || 1 ≥ ||̺|| 1 -1, we get m ≥ k + ||̺|| 1 . Now, just observe that F τ ′ (m) = F m+1 τ ′ m (m) ≥ F τ ′ m (k) from Lemma V.2. For every j < i, we have ∂ i n (τ )(j) = τ (j) + n = ̺(j) + n ≤ ||̺|| 1 + k ≤ m = τ ′ m (j). Hence we infer that ∂ i n (τ ) ⊑ τ ′ m and so Lemma V.2 provides F ∂ i n (τ ) (k) ≤ F τ ′ m (k).
The lemma follows from this inequality, and the inequalities

F τ ′ (m) ≥ F τ ′ m (k) and F τn (k) ≥ F τ ′ (m) previously proved.
Lemma VI.6. x.F τ (n) + y ≤ F τ (x.n + x -1 + y) for every x ≥ 1, y, n ≥ 0, and for every type τ .

Proof. The lemma is proved by induction on types, with the lexicographic order. The base case τ = ∅ is immediate since

x.F ∅ (n) + y = x(1 + n) + y = 1 + x.n + x -1 + y = F ∅ (x.n + x -1 + y).
Induction case for a type τ = ∅. We have x.F τ (n) + y = x.F n+1 τn (n) + y. Since τ n < τ , and F τn is monotonic, by induction on r ≥ 0, we get for every k ≥ 0:

x.F r τn (k) + y = F r τn (x.k + r(x -1) + y)

By introducing m = x.n + x -1 + y, we get:

x.F n+1 τn (n) + y ≤ F n+1 τn (m + n.(x -1)) ≤ F n+1 τm (m + n.(x -1)) [Lemma V.2] Notice that F n.(x-1) ∅ (m) = m + n.(x -1). Thus m + n.(x - 1) ≤ F n.(x-1) τm (m) from Lemma V.2. As m -n = n.(x -1) + x -1 + y ≥ 0, we deduce that F n.(x-1) τm (m) ≤ F m-n τm (m) from Lemma V.2.
Combined with the previous relations, we get:

x.F n+1 τn (n) + y ≤ F n+1+m-n τm (m) [Lemma V.2] = F m+1 τm (m) = F τ (m) = F τ (x.n + x -1 + y)
We have proved the induction.

Lemma VI.7. We have

K τ (n) ≤ F τ (d.n) for every n ≥ 2.
Proof. We prove the lemma by induction on types with the lexicographic order. The base case τ = ∅ is immediate. Let us consider the case τ = {0}. In this case

K τ (n) ≤ K ∅ (K ∅ (n + 1)) = n + 1. Since F τ (d.n) ≥ F ∅ (d.n) = d.n + 1,
we are done. Let us prove the induction step with a type τ such that τ = ∅ and τ = {0}. Let n ≥ 2 and i be an index such that

K τ (n) ≤ K ∂ i d.n (τ ) (K ∂ i d.n (τ ) (n + 1)
). We have:

K τ (n) ≤ F ∂ i d.n (τ ) (d.F ∂ i d.n (
F dn-1 τ d.n (dn) ≥ 2 dn-1 (dn + 1) -1 ≥ dn(dn + 1) -1 ≥ 2d(dn + 1) -1 ≥ d 2 .(n + 1) + d -1 Therefore K τ (n) ≤ F τ d.n (F τ d.n (F d.n-1 τ d.n (d.n))) = F d.n+1 τ d.n (d.n) = F τ (d.n).
We have proved the induction step.

Since L τ (n) ≤ K τ (n) ≤ F τ (dn), Theorem VI.1 is proved.

VII. APPLICATION TO PUSHDOWN VASS

We now apply the results of the previous sections to vector addition systems with states (VASS) extended with a pushdown stack. Consider a dimension d ∈ N, with d ≥ 1. A pushdown VASS is a 5-tuple A = Q, q init , v init , Γ, ∆ where Q is a finite set of locations, q init ∈ Q is the initial location, v init ∈ N d is the initial vector, Γ is a finite stack alphabet, and ∆ ⊆ Q × Z d × Op × Q is a finite set of transition rules. As before, the set Op of operations is given by Op = {ε} ∪ {push(γ), pop(γ) | γ ∈ Γ}. Informally, a pushdown VASS can be viewed as a pushdown automaton equipped with d counters ranging over natural numbers. Operations on counters are limited to translations. A rule (q, a, op, r) means that the pushdown VASS can move from location q to location r by performing the operation op on the stack and adding the vector a to its counters, provided that they remain nonnegative.

The operational semantics of a pushdown VASS A is defined in two steps. First, we associate with A the pushdown system P A = S A , s A init , Γ, ∆ A given by:

S A = Q × N d s A init = (q init , v init ) ((q, u), op, (r, v)) ∈ ∆ A ⇔ (q, v -u, op, r) ∈ ∆
Note that P A is finitely-branching. Second, we define the operational semantics of A to be the operational semantics of P A (see Section III). Let us introduce the partial-order A on S A defined by (q, v) A (q ′ , v ′ ) when q = q ′ and v ≤ v ′ . This partial-order makes P A a well-structured pushdown system (see Definition III.1). According to Propositions III.3, III.4 and III.5, the termination and boundedness problems for pushdown VASS can be solved by constructing the reduced reachability tree, which is finite. We show in this section that the worst-case size of this tree is hyper-Ackermannian.

For the remainder of this section, we restrict ourselves to pushdown VASS such that ||a|| ∞ ≤ 1 for each rule (q, a, op, r). The hyper-Ackermannian upper bound that we obtain below can be extended to the general case by splitting each rule (q, a, op, r) into ||a|| ∞ basic ones. The size of a pushdown VASS A = Q, q init , v init , Γ, ∆ is defined as

|A| = d + |Q| + d • ||v init || ∞ + |Γ| + d • |∆|
According to Remark IV.3, every run of P A can be seen as a nested sequence over

(S A , A ). Let us introduce the norm ||.|| S A on (S A , A ), defined by ||(q, v)|| S A = ||v|| ∞ . This nested sequence is n-controlled, for n = ||v init || ∞ + 2,
since the initial state of P A is (q init , v init ) and ||a|| ∞ ≤ 1 for each rule (q, a, op, r). Recall that every subsumed node in the reduced reachability tree of P A is necessarily a leaf. It follows from Remark IV.7 that the height of this tree is bounded by the maximal length of n-controlled bad nested sequences, namely

L S A (n). Note that (S A , A , ||.|| S A ) is isomorphic to (|Q| × N d , |Q|×N d , ||.|| |Q|×N d ). Since Q = ∅, d ≥ 1 and n ≥ 2,
we get from Theorem VI.1 that the height of the reduced reachability tree is at most

F ω d .|Q| (d • n). Each node B i 0 ≤ i < d A 0 A α+1 A i λ 0 < i < d q 2 q 3 q 1 q 0 q init q f r↓, κ ++ d-1 r↑ push(F ) r -- r ++ pop(F ) push(I i ) κ -- i r↓, κ ++ i-1 , push(D i-1 ) push(F ) r↑ A i λ pop(F ) push(I 0 ) κ -- 0 r↓, push(F ) r↑ A α+1 pop(F ) r ++ A 0 pop(I i ), κ ++ i pop(D i ), κ -- i B i Figure 1. Pushdown VASS A d (n) that weakly computes F ω d (n).
of the reduced reachability tree can have at most |∆| children. We derive the following upper bound on its size.

Theorem VII.1. The reduced reachability tree of a pushdown VASS A has at most F ω ω (|A|) nodes.

Remark VII.2. For classical VASS (i.e., op = ε for each rule (q, a, op, r)), the reduced reachability tree has at most F ω (|A|) nodes [START_REF] Mcaloon | Petri nets and large finite sets[END_REF], [START_REF] Figueira | Ackermannian and primitive-recursive bounds with Dickson's lemma[END_REF]. For pushdown finite-state systems, it follows from Remark VI.2 that its size is bounded by |∆| 2 |Q| . We next give an almost matching lower bound for the above-mentioned size of the reduced reachability tree. We introduce a pushdown VASS A d (n), depicted in Figure 1, that is parametrized by a "target" dimension d ≥ 1 and an initial value n ∈ N. The lower bound is obtained as follows. First, we show that A d (n) computes, in a weak sense, the value F ω d (n). This computation requires, in A d (n), a run of length at least F ω d (n). Second, we prove that all runs of A d (n) are finite. Therefore, its reduced reachability tree is identical to its reachability tree, and so its height is at least F ω d (n). The remainder of this section presents these ideas in detail. To simplify notation, we will shortly write A d when the parameter n is understood from the context. The dimension of A d is d + 2. But, for clarity, we will use counter names to refer to individual coordinates of the vectors in the configurations of A d . The parameter n is the initial value of the first counter, called r, which will also contain the result at the end. For intermediate steps, we use the counters r, κ 0 , . . . , κ d-1 . The notation r↓ in Figure 1 is short for r --, r ++ , i.e., a decrement of r followed by an increment of r. Similarly, the notation r↑ is short for r ++ , r --, i.e., an increment of r followed by a decrement of r. The stack alphabet is Γ = {F, D 0 , I 0 , . . . , D d-1 , I d-1 }. Intuitively, the stack and counters of A d are used to represent the recursive definition of F ω d (n). As expected, the stack is used to store the pending recursive calls. The innermost F α (m) computation is encoded as α = ω d-1 . κ d-1 + • • • + ω 0 . κ 0 and r = m + 1. For example, F ω2 .3+ω.5+2 [START_REF] Chadha | Deciding branching time properties for asynchronous programs[END_REF] is represented by having F on top of the stack, κ 2 = 3, κ 1 = 5, κ 0 = 2 and r = 9. The stack symbols D i , I i are used to restore the calling context (i.e., the counters κ i ) of pending recursive calls.

The initial location of A d is q init , and its initial vector is v init = (n, 0, . . . , 0). This means that the initial value of the counter r is n and all other counters have initial value 0. First, we increment r by one and move to q 0 . The loop at q 0 allows us to increment κ d-1 to the value n + 1 and the loop at q 1 allows us to set r back to n + 1. Then we push F on the stack and reach q 2 . At this point, the stack contents is σ = F , the counters κ d-1 , . . . , κ 0 contain n+1, 0, . . . , 0, respectively, and r = n + 1. This configuration represents F w d-1 .(n+1) (n), which is equal to F ω d (n), i.e., the number that we want to compute. From the location q 2 , A d can either execute A i λ or A α+1 or A 0 or B i to reach q 3 . From the location q 3 , A d can either go back to q 2 to continue the computation, or move to the final location q f . At q 2 , if the top of the stack is F and κ 0 = 0, then it represents F ω d-1 .κ d-1 +•••+ω i .κi (r -1), assuming that κ i > 0 and κ i-1 = • • • = κ 0 = 0. In that case, the purpose of A i λ is to replace the top of the stack with something that represents F ω d-1 .κ d-1 +•••+ω i .(κi-1)+ω i-1 .r (r -1). Accordingly, A i λ first pops F from the stack. Then it decrements κ i and pushes I i on the stack to "shield" the part of the stack below from this decreased value of κ i . Then A i λ increments the counter κ i-1 r times, also pushing the symbol D i-1 each time. The purpose of D i-1 is to "guard" the part of the stack below from this increased value of κ i-1 . Finally, A i λ pushes F on the stack, restores the value of r and exits.

At q 2 , if the top of the stack is F and κ 0 > 0, then it represents F α+1 (r -1), where α

= ω d-1 . κ d-1 +• • •+ω 0 . (κ 0 -1).
In that case, the purpose of A α+1 is to replace the top of the stack with something that represents F r α (r -1). Accordingly, A α+1 first pops F from the stack. Then it decrements κ 0 and pushes I 0 on the stack to "shield" the part of the stack below from this decreased value of κ 0 . Then it pushes r copies of the symbol F , restores the value of r and exits.

At q 2 , if the top of the stack is F and κ d-1 = • • • = κ 0 = 0, then it represents F 0 (r -1). Accordingly, A 0 simply pops F from the stack, increments r and exits.

At q 2 , if the top of the stack is I i or D i , then sometime back, either 1) A i λ decremented κ i , pushed one I i to shield the bot-tom part of the stack from this decrement, incremented κ i-1 n times and pushed n copies of D i-1 to guard the bottom part of the stack from these increments, or 2) i = 0, n = 0, A α+1 decremented κ 0 once and pushed one I 0 to shield the bottom part of the stack from this decrement. The purpose of B 0 , . . . , B d-1 is to backtrack and access the bottom part of the stack by removing guards and shields, and restoring the counter values. Accordingly, B i either pops the symbol D i from the top of the stack, decrements κ i and exits, or it pops I i , increments κ i and exits.

Lemma VII.3. Suppose A d is in location q 2 , F is on the top of the stack and the counter r has value m + 1. Then there is a partial 2 run in A d that reaches q 3 , removes F from the top of the stack, sets the counter r to the value

F ω d-1 .κ d-1 +•••+ω 0 .κ0 (m) + 1
, and does no other change.

Corollary VII.4. There is a run in A d (n) that reaches q f with the empty stack and the counter r having the value F ω d (n).

Proof. A witnessing run is provided in the table below. The partial run from q 2 to q 3 is derived from Lemma VII.3.

Loc. r κ d-1 Stack (q init , n, 0, ε) r ++ --→ (q 0 , n + 1, 0, ε) (r↓,κ ++ d-1 ) n+1 --------→ (q 1 , 0, n + 1, ε) (r↑) n+1 push(F ) ----------→ (q 2 , n + 1, n + 1, F ) → * (q 3 , F ω d-1 .(n+1) (n) + 1, n + 1, ε) r -- ---→ (q f , F ω d-1 .(n+1) (n), n + 1, ε)
The observation that F ω d (n) = F ω d-1 .(n+1) (n) concludes the proof of the corollary.

Next, we prove that all runs of A d are finite. The intuition is to measure, by an ordinal, the "size" of both the stack contents and the values of the counters κ d-1 , . . . , κ 0 , and prove that the size decreases at each step. Consider a vector

v = (v d-1 , . . . , v 0 ) in N d . The ordinal associated with v is defined as Ord(v) = ω d-1 . v d-1 + • • • + ω 0 . v 0 . Let σ ∈ Γ *
be a string over the stack alphabet. The ordinal associated with σ and v is defined as follows, by induction on |σ|.

Ord(ε, v) = 0 Ord(σF, v) = Ord(σ, v) + ω Ord(v) Ord(σI i , v) = Ord(σ, v + e i ) Ord(σD i , v) = undefined if v i = 0 Ord(σ, v -e i ) if v i > 0
The ordered pair dr(σ, v) = (Ord(σ, v), |σ|) is the depth of remaining recursion associated with a configuration of A d whose stack contents is σ and where the counter values of κ d-1 , . . . , κ 0 form the vector v. We use the lexicographic order on ordered pairs to compare depths of remaining recursion.

Lemma VII.5. Every partial run of A d (n) that starts and ends in q 2 , but does not visit q 2 in between, makes the depth of remaining recursion strictly decrease.

Corollary VII.6. All runs of A d (n) are finite.

Proof. By contradiction, suppose that there is an infinite run. It is readily seen that, after a finite prefix, the run must stay within q 2 , q 3 , A i λ , A α+1 , A 0 and B i . Upon entering into A i λ , A α+1 , A 0 or B i , the run must exit after a finite number of steps, since the loops inside these can only be executed finitely many times for each entry. Hence, the run must visit q 2 infinitely often. Now from Lemma VII.5, we infer that there is an infinite strictly decreasing sequence of depths of remaining recursion, which is a contradiction.

We obtain the following lower bound on the size of the reduced reachability tree for pushdown VASSs.

Theorem VII.7. For every n ∈ N, there exists a pushdown VASS A n , of size quadratic in n, such that the reduced reachability tree of A n has at least F ω ω (n) nodes.

Proof. Corollary VII.6, combined with Proposition III.4, shows that the reachability tree of A n+1 (n) contains no subsumed node. Therefore, the reachability tree of A n+1 (n) coincides with its reduced reachability tree, which is finite according to Proposition III.3. The height of this tree is at least

F ω ω (n) = F ω n+1 (n) by Corollary VII.4. It is readily seen that |A n+1 (n)| is quadratic in n.
Remark VII.8. The hyper-Ackermannian lower and upper bounds of Theorems VII.1 and VII.7 also apply to the reachability set when it is finite.

VIII. CONCLUSION

Reachability sets of bounded VASS (without stack) are known to be Ackermannian large. The lower-bound was provided by [START_REF] Mayr | The complexity of the finite containment problem for petri nets[END_REF] thanks to a family of VASS with finite, but large reachability sets (Ackermannian). The upper-bound was first derived in [START_REF] Mcaloon | Petri nets and large finite sets[END_REF] from bounds on the length of bad sequences of vectors of natural numbers. However, the boundedness problem for VASS is decidable in exponential space. This complexity was proved by Rackoff in [START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF] by observing that unboundedness of a VASS can be witnessed by finite runs of length at most doubly exponential.

In this paper, reachability sets of bounded pushdown VASS are shown to be hyper-Ackermannian large. The lower-bound is obtained thanks to a family of bounded pushdown VASS with finite, but large reachability sets (hyper-Ackermannian). The upper-bound is derived from a precise complexity analysis of an adaptation of the Karp & Miller algorithm. Based on this algorithm, we deduce that the unboundedness of pushdown VASS can be witnessed by finite runs. We think that the precise complexity of the boundedness problem can be obtained by bounding the length of these witnesses. However, adapting Rackoff's techniques to pushdown VASS is a difficult and challenging problem. Note that witnesses have a length that is at least a tower of exponentials, i.e., a length in F 3 (n), where n is the size of the pushdown VASS. Such a lower-bound can be easily obtained by adapting [START_REF] Lazic | The reachability problem for vector addition systems with a stack is not elementary[END_REF]. The complexity gap between the lower-bound F 3 (n) and the upper-bound F ω ω (n) is an open problem.

Since each node of T can have at most |∆| children, we obtain that T has at most |∆| h+1 nodes. To reduce clutter in the inequations below, we introduce n = |A|, α = ω n . n + • • • + ω 0 . n, and β = ω d . |Q|. Observe that n ≥ |Q| and n ≥ d ≥ 1. It follows that α ⊒ β and α ⊒ ω. Recall also that, according to Lemma V.2, for each ordinal γ < ω ω , F γ is monotonic and F γ (m) ≥ m for all m ∈ N. We derive that:

F ω ω (n) = F ω n+1 (n) = F ω n .(n+1) (n) = F ω n .n+•••+ω 1 .n+ω 0 .(n+1) (n) = F α+1 (n) = F n+1 α (n) ≥ F n α (F β (n)) [α ⊒ β] ≥ F α (F β (n)) [n ≥ 1] ≥ F ω (F β (n)) [α ⊒ ω] ≥ (F β (n)) F β (n)+1 [Lemma A.1] ≥ (F β (n)) h+1 [F β (n) ≥ h] ≥ |∆| h+1 [F β (n) ≥ n ≥ |∆|]
We conclude that T has at most F ω ω (n) nodes.

Lemma VII.3. Suppose A d is in location q 2 , F is on the top of the stack and the counter r has value m + 1. Then there is a partial3 run in A d that reaches q 3 , removes F from the top of the stack, sets the counter r to the value F ω d-1 .κ d-1 +•••+ω 0 .κ0 (m)+ 1, and does no other change.

Proof. By assumption, the starting value of r is m + 1, and the starting location is q 2 . Let c d-1 , . . . , c 0 denote the starting values of the counters κ d-1 , . . . , κ 0 , respectively. The proof is by induction on the ordinal ω d-1 . c d-1 + • • • + ω 0 . c 0 . We write configurations as tuples enclosed in parentheses, with the location as first element, followed by the values of r, κ d-1 , . . . , κ 0 , and finally the stack content.

• ω d-1 . c d-1 + • • • + ω 0 . c 0 = 0. Recall that F 0 (m) = m + 1.

(q 2 , r = m + 1, 0, . . . , 0, σF ) A0 --→ (q 3 , r = m + 2, 0, . . . , 0, σ)

• ω (q 2 , m + 1, c d-1 , . . . , c i , 0, σF )

A i λ --→ (q 3 , m + 1, c d-1 , . . . , c i -1, m + 1, σI i D m+1 i-1 F ) → (q 2 , m + 1, c d-1 , . . . , c i -1, m + 1, σI i D m+1 i-1 F ) → IH (q 3 , F λm (m) + 1, c d-1 , . . . , c i -1, m + 1, σI i D m+1 i-1 ) → (q 2 , F λ (m) + 1, c d-1 , . . . , c i -1, m + 1, σI i D m+1 i-1 )

B i-1
---→ (q 3 , F λ (m) + 1, c d-1 , . . . , c i -1, m, σI i D m i-1 ) → . . . m times (q 3 , F λ (m) + 1, c d-1 , . . . , c i -1, 0, σI i ) → (q 2 , F λ (m) + 1, c d-1 , . . . , c i -1, 0, σI i )

B i --→ (q 3 , F λ (m) + 1, c d-1 , . . . , c i , 0, σ)
This concludes the proof of the lemma.

Lemma VII.5. Every partial run of A d (n) that starts and ends in q 2 , but does not visit q 2 in between, makes the depth of remaining recursion strictly decrease.

Proof. By case analysis on whether the partial run executes A i λ , A α+1 , A 0 or B i . We use the following properties of ordinals.

α ≥ 0, β < γ ⇒ α + β < α + γ α = 0, β < γ ⇒ α. β < α. γ α > 1, β < γ ⇒ α β < α γ
In the following, we denote by v = (v d-1 , . . . , v 0 ) the vector of natural numbers formed by the values of the counters κ d-1 , . . . , κ 0 . The contents of the stack is denoted by σ.

• A i λ :

(σF, v) = dr(σD i , v)

We have shown that, in all cases, the partial run makes the depth of remaining recursion strictly decrease.

Definition IV. 9 .

 9 A norm for a wqo set (S, ) is a function ||.|| : S → N such that {s ∈ S | ||s|| ≤ n} is finite for every n. The structure (S, , ||.||) is called a normed wqo.

  τ ) (d.(n + 1))) [IH and Lemma V.2] ≤ F τ d.n (d.F τ d.n (d.(n + 1))) [Lemma VI.5 and Lemma V.2] ≤ F τ d.n (F τ d.n (d 2 .(n + 1) + d -1)) [Lemma VI.6 and Lemma V.2] Since τ = ∅ and τ = {0}, we deduce that τ d.n = ∅. With an immediate induction, and Lemma VI.4, we get:

  -1 . c d-1 + • • • + ω 0 . c 0 = α + 1, a successor ordinal. This means that c 0 > 0. Recall that F α+1 (m) = F m+1 α (m). State r κ d-1 • • • κ 1 κ 0 Stack (q 2 , m + 1, c d-1 , . . . , c 1 , c 0 , σF ) Aα+1 ---→ (q 3 , m + 1, c d-1 , . . . , c 1 , c 0 -1, σI 0 F m+1 ) → (q 2 , m + 1, c d-1 , . . . , c 1 , c 0 -1, σI 0 F m+1 ) → * IH (q 3 , F α (m) + 1, c d-1 , . . . , c 1 , c 0 -1, σI 0 F m ) → (q 2 , F α (m) + 1, c d-1 , . . . , c 1 , c 0 -1, σI 0 F m ) → * IH (q 3 , F 2 α (m) + 1, c d-1 , . . . , c 1 , c 0 -1, σI 0 F m-1 ) → . . . (m -1) times (q 3 , F m+1 α (m) + 1, c d-1 , . . . , c 1 , c 0 -1, σI 0 ) → (q 2 , F α+1 (m) + 1, c d-1 , . . . , c 1 , c 0 -1, σI 0 ) B 0 --→ (q 3 , F α+1 (m) + 1, c d-1 , . . . , c 1 , c 0 , σ) • ω d-1 . c d-1 + • • • + ω 0 . c 0 = λ,a limit ordinal. Suppose c i > 0 and c i-1 = • • • = c 0 = 0, with i > 0. Then, by definition of the canonical fundamental sequence, λ m = ω d-1 . c d-1 + • • • + ω i . (c i -1) + ω i-1 . (m + 1). Recall that F λ (m) = F λm (m). State r κ d-1 • • • κ i κ i-1 Stack

  (σI i D m i-1 F, ve i + m. e i-1 ), with m ∈ N, i > 0, v i > 0 dr(σI i D m i-1 F, ve i + m. e i-1 ) = (Ord(σI i D m i-1 , ve i + m. e i-1 ) + ω Ord(v-ei+m.ei-1) , |σI i D m i-1 F |) = (Ord(σ, v) + ω Ord(v-ei+m.ei-1) , |σI i D m i-1 F |) < (Ord(σ, v) + ω Ord(v) , |σF |) = (Ord(σF, v), |σF |) = dr(σF, v) • A α+1 : (σF, v) Aα+1 ---→ (σI 0 F m , ve 0 ), with m ∈ N, v 0 > 0 dr(σI 0 F m , ve 0 ) = (Ord(σI 0 F m , ve 0 ), |σI 0 F m |) = (Ord(σ, v) + ω Ord(v-e0) . m, |σI 0 F m |) < (Ord(σ, v) + ω Ord(v-e0) . ω, |σF |) = (Ord(σ, v) + ω Ord(v) , |σF |) = (Ord(σF, v), |σF |) = dr(σF, v) • A 0 : (σF, v) A0 --→ (σ, v) dr(σ, v) = (Ord(σ, v), |σ|) < (Ord(σ, v) + ω Ord(v) , |σF |) = (Ord(σF, v), |σF |)= dr(σF, v)• B i with I i on top:(σI i , v) B i --→ (σ, v + e i ) dr(σ, v + e i ) = (Ord(σ, v + e i ), |σ|) < (Ord(σ, v + e i ), |σI i |) = (Ord(σI i , v), |σI i |) = dr(σI i , v) • B i with D i on top: (σD i , v) B i --→ (σ, ve i ),with v i > 0 dr(σ, ve i ) = (Ord(σ, ve i ), |σ|) < (Ord(σ, ve i ), |σD i |) = (Ord(σD i , v), |σD i |)

This section motivates the developments of the following sections, but its results are only used in Section VII.

By partial run, we mean a run that is not required to start from the initial configuration.

By partial run, we mean a run that is not required to start from the initial configuration.

APPENDIX

A. Proofs of Section IV Lemma IV.8. Bad nested sequences over a wqo are finite.

Proof. We consider an infinite sequence (s 0 , h 0 ), (s 1 , h 1 ), . . . of elements in S × N with h 0 = 0. From the infinite sequence h i0 , h i1 , h i2 , . . . we extract an infinite sequence i 0 , i 1 , i 2 , . . . defined as follows:

By definition h i+k ≤ h j By definition, h i k ≤ h j for all j, k ∈ N with i k ≤ j. Since is a well-quasi-order, there exists k < l such that s i k s i l . Thus the sequence (s 0 , h 0 ), (s 1 , h 1 ), . . . is good.

B. Proofs of Section VI

Lemma VI.3. It holds that:

for every type τ , for every i ∈ {1, . . . , d}, for every v ∈ τ (i) × N i , for every n ≥ ||v|| τ , and for every m ∈ N.

Proof. Since v ∈ τ (i) × N i there exist q ∈ {1, . . . , τ (i)} and v ∈ N i such that v = (q, v). By adapting the following proof, we can assume without loss of generality that q = τ (i). Since τ (i) > 0, the derivation type ̺ = ∂ i d.n (τ ) is well defined. We introduce the projection function π r : N i → N i-1 that removes the component indexed by r, and formally defined as follows:

π r (u) = (u(1), . . . , u(r -1), u(r + 1), . . . , u(i))

Let us observe that for every u ∈ N i /v there exists a minimal r ∈ {1, . . . , i} such that u(r) < v(r). We denote by µ(u) this minimal index r. Since ||v|| ∞ ≤ n we deduce that u(r) ∈ {0, . . . , n -1}. Notice that this set can be empty if n = 0.

We introduce the function ν : N τ /v → N ̺ defined for every u = (p, u) ∈ τ (j) × N j by:

Observe that if (u 0 , h 0 ) . . . , (u k , h k ) is a m-controlled bad nested sequence in N τ /v then (ν(u 0 ), h 0 ), . . . , (ν(u k ), h k ) is a m-controlled bad nested sequence in N ̺ . We have proved the lemma.

C. Proofs of Section VII

Lemma A.1. For every n ∈ N, F ω (n) ≥ n n+1 .

Proof. We first show that F 2 2 (n) ≥ n n+1 for every n ∈ N. Observe that F 1 (n) = 2n + 1 for all n ∈ N. An easy induction on k shows that

2), we obtain that:

Let us now prove the statement of the lemma, namely that F ω (n) ≥ n n+1 for all n ∈ N. It is readily seen that this inequality holds for n ≤ 1, since F ω (0) = F 1 (0) = 1 and F ω (1) = F 2 (1) = 7. Assume for the remainder of the proof that n ≥ 2. By Lemma V.2, we get that

, which concludes the proof of the lemma. Theorem VII.1. The reduced reachability tree of a pushdown VASS A has at most F ω ω (|A|) nodes.

Proof. Consider a pushdown VASS A = Q, q init , v init , Γ, ∆ , and let T denote its reduced reachability tree. Recall that d ≥ 1 and

The case where ∆ is empty is trivial, since F ω ω (n) = F ω n+1 (n) > n for every n ∈ N (by Lemma V.2), and T contains only one node if ∆ = ∅. So we assume for the remainder of the proof that ∆ = ∅.

We have shown in the main text preceding the theorem that the height h of T satisfies h ≤ F


Foreword

This report explains how to upgrade an Ar.Drone 2 [1] for swarming and services hosting. In other words, it gives the technical information required to easily create a swarm of Ar.Drone 2 sharing a Wi-Fi network. Moreover, it describes the process to install new services and applications on the drone.

To achieve this process, it is necessary to perform several core modifications inside the Ar.Drone 2 operating system.

The authors decline all responsibility in case of any damage or any problem on any device used in the process, and on the usage of the resulting systems.

1 Requirements

Hardware requirements

To put in practice the operations described in this document, several pieces of hardware are required:

• an Ar.Drone 2 [1];

• a Linux base station [2];

• a USB flash drive with at least 8 GB of memory;

• a IEEE 802.11 chip with g/n Wi-Fi and ad-hoc mode support [3].

The specific items used throughout this report are:

• an Ar.Drone 2;

• a computer with a Debian Wheezy Linux distribution [4];

• a Kingston DataTraveler G3 USB key with 8GB of memory [START_REF]DataTraveler G[END_REF];

• an Asus WL-167G Wi-Fi key [6].

Software requirements

Several third-party software packages need to be installed:

• a partition manager like Parted [START_REF] Gnu | [END_REF] that will be used to create a suitable partitions table;

• the partition formatting tools contained in E2fsprogs [START_REF] Ts | E2fsprogs[END_REF] and Dosfstools [START_REF] Baumann | Dosfstools[END_REF];

• the Debootstrap tool [10] that will enable to create a Linux root file system;

• a local DHCP/DNS server/relay like Dnsmasq [START_REF] Kelley | Dnsmasq[END_REF];

• a telnet client that will be used to communicate with the drones;

• the wireless-tools software suite [START_REF] Hp | Linux Wireless Tools[END_REF] to manage the Wi-Fi settings.

Ar.Drone Base System to ArDroneXT

In order to enable an Ar.Drone 2 to be part of a swarm, it is necessary to modify its operating system. To prevent any damage or alteration of the original drone operating system, we will setup the new one on a dedicated USB flash drive. We call ArDroneBS, the original Ar.Drone 2 operating system, and ArDroneXT the version that will be installed on the USB flah drive.

Ar.Drone 2 operating system

The original operating system of the Ar.Drone 2 is a Parrot home-made Linux [2] running on an ARM EABI architecture. This Linux lays on a writable disk partition and it is thus possible to modify it. Nevertheless, modifying the root file system directly could be very damageable in case of mistakes. We will thus install another customized Linux system on a USB flash drive which will be plugged into the drone. The process described below requires root privileges on the computer Linux distribution.

USB flash drive partitions setup

We first create three partitions on the USB flash drive:

• one for the new operating system;

• one for the ARM EBAI cross-compiler (which makes development easier);

• one for users files, scripts, photos and videos.

We setup these partitions as follows:

1. ARDSYS: ext2 file system with 5GB; 2. ARDDEV: ext2 file system with 1GB; 3. ARDUSR: fat32 file system with 2GB.

Usually, USB flash drives are fat32 formatted. However the two first partitions cannot be setup with this kind of file system since it is not compliant with the symbolic links used by Linux (ARDSYS partition) and the ARM cross-compiler (ARDDEV partition). Besides, the drone can only take pictures and record videos on a fat32 file system. Therefore, the third partition (ARDUSR) has to be setup as a fat32 partition.

Please note that the second partition (ARDDEV) is optional and designed for cross-compilation from a x86-64 system to the ARM EABI architecture. We choose to install it directly on the USB flash drive in order to get a device ready to use for both end users and developers. Also, note that several Linux distributions provide such a compiler directly in their packages repository.

In the following commands the USB flash drive is identified as sdb. We first check the original content of the USB flash drive. l i n u x $ p a r t e d / dev / sdb p r i n t Disk / dev / sdb : 7747MB P a r t i t i o n Finally, we format the partitions and label them. l i n u x $ mkfs . e x t 2 -L "ARDSYS" / dev / sdb1 l i n u x $ mkfs . e x t 2 -L "ARDDEV" / dev / sdb2 l i n u x $ mkdosfs -F32 -n "ARDUSR" / dev / sdb3

The USB flash drive is now ready. l i n u x $ p a r t e d / dev / sdb p r i n t . . . Number S t a r t End S i z e Type F i l e system 1 1049kB 5663MB 5662MB primary e x t 2 2 5663MB 6737MB 1074MB primary e x t 2 3 6737MB 7747MB 1010MB primary f a t 3 2

After creating these 3 partitions, we have to mount them (in case the system did not perform this task automatically). l i n u x $ mkdir /mnt/ARDSYS l i n u x $ mkdir /mnt/ARDDEV l i n u x $ mkdir /mnt/ARDUSR l i n u x $ mount -t e x t 2 / dev / sdb1 /mnt/ARDSYS l i n u x $ mount -t e x t 2 / dev / sdb2 /mnt/ARDDEV l i n u x $ mount -t v f a t / dev / sdb3 /mnt/ARDUSR

Installing the ARM EABI compiler (ARDDEV partition)

In order to compile new programs for the drone, we have to get a cross-compiler which runs on a x86-64 architecture and produces an ARM EABI binary code. We can find a light one on the Mentor Graphics website [START_REF]GCC/G++ ARM EABI[END_REF]. This one is used by the Debian community members to compile their own ARM EABI Linux distribution [START_REF]Debian ARM EABI Port[END_REF]. After downloading it, we extract the archive in the ARDDEV partition. l i n u x $ t a r -C /mnt/ARDDEV -x v j f \ arm -2012.09 -64.arm-none-l i n u x -gnueabi-i 6 8 6 -pc-l i n u x -gnu . t a r . bz2

Then, we test the compiler as follows.

l i n u x $ export PATH=$PATH: / mnt/ARDDEV/arm-2012/ b i n / l i n u x $ cd /tmp l i n u x $ echo ' i n t main ( ) { return 0 ; } ' > n o t h i n g . c l i n u x $ arm-none-l i n u x -gnueabi-g c c n o t h i n g . c -o n o t h i n g . e l f l i n u x $ f i l e n o t h i n g . e l f n o t h i n g . e l f : ELF 32-b i t LSB e x e c u t a b l e , ARM, EABI5 v e r s i o n 1 (SYSV) d y n a m i c a l l y l i n k e d ( u s e s s h a r e d l i b s ) fo r GNU/ Linux 2 . 6 . 1 6 , not s t r i p p e d

The ARDDEV partition is now ready.

2.4 Installing the operating system (ARDSYS partition)

Setting up the root file system

First of all, we have to create a Linux root file system compliant with the ARM EABI processor architecture. We have chosen to install a stable Debian [4] system which provides an ARM compliant architecture called armel. We use the Debootstrap [10] tool to create the root file system. l i n u x $ cd /mnt/ARDSYS l i n u x $ d e b o o t s t r a p --a r c h=armel --f o r e i g n s q u e e z e /mnt/ARDSYS \ h t t p : / / f t p . d e b i a n . o r g / d e b i a n /

Connecting to the drone

The last part of the Deboostrap process has to be done from inside the drone. We thus plug the USB flash drive into the drone and turn the drone on.

Then, we have to connect our Linux station to the drone. The drone provides a Wi-Fi access point with no encryption and a DHCP server. Its network interface uses the IP address 192.168.1.1, therefore we can use the 192.168.1.2 for the Wi-Fi chip of the Linux station (or another one in the sub-network 192.168.1.0/24) or even call the DHCP server of the drone to automatically get an IP address. We have also to turn off the power management mode of our Wi-Fi chip in order to increase the quality of the connectivity.

Note that the hardware address (MAC), the channel number and the ESSID of the network can vary. In addition, we have to turn off the network daemon manager on our Linux computer (e.g. NetworkManager [START_REF] Gnome | NetworkManager[END_REF] on Debian) in order to manually configure our device as explained above. Most of Linux distributions have a network daemon program in order to manage network connections (e.g. Ethernet and Wi-Fi). Please refer to your Linux distribution documentation in order to know how to turn the relative network daemon off.

The corresponding commands are listed hereafter. l i n u x $ i f c o n f i g wlan0 down l i n u x $ i f c o n f i g wlan0 mode managed l i n u x $ i f c o n f i g wlan0 up l i n u x $ i w l i s t wlan0 s c an wlan0 Scan completed : . . . C e l l xx -Address : 9 0 : 0 3 : B0 : 4 0 :

. . . l i n u x $ i w c o n f i g wlan0 power o f f l i n u x $ i w c o n f i g
wlan0 c h a n n e l 1 l i n u x $ i w c o n f i g wlan0 e s s i d ardrone_000 ap 9 0 : 0 3 : B0 : 4 0 : 9 9 :AB l i n u x $ i w c o n f i g wlan0 wlan0 IEEE 8 0 2 . 1 1 bg ESSID : " ardrone_000 " Mode : Managed Frequency : x GHz A c c e s s Point : 9 0 : 0 3 : B0 : 4 0 : 9 9 :AB . . . l i n u x $ d h c l i e n t wlan0 # or l i n u x $ i f c o n f i g wlan0 1 9 2 . 1 6 8 . 1 . 2 l i n u x $ i f c o n f i g wlan0 wlan0 Link encap : E t h e r n e t HWaddr 0 0 : 1 1 : f 0 : 7 c : f e : 7 7 i n e t adr : 1 9 2 . 1 6 8 . 1 . 2 Bcast : 1 9 2 . 1 6 8 . 1 . 2 5 5

Masque : 2 5 5 . 2 5 5 . 2 5 5 . 0 . . . We can now check the connectivity from the base station to the drone with a ping. l i n u x $ p i n g -c1 1 9 2 . 1 6 8 . 1 . 1 PING 1 9 2 . 1 6 8 . 1 . 1 ( 1 9 2 . 1 6 8 . 1 . 1 ) 5 6 ( 8 4 ) b y t e s o f data . 64 b y t e s from 1 9 2 . 1 6 8 . 1 . 1 : icmp_req=1 t t l =64 time =2.07 ms ---1 9 2 . 1 6 8 . 1 . 1 p i n g s t a t i s t i c s ---1 p a c k e t s t r a n s m i t t e d , 1 r e c e i v e d , 0% p a c k e t l o s s , time 0ms r t t min/ avg /max/mdev = 2 . 0 7 6 / 2 . 0 7 6 / 2 . 0 7 6 / 0 . 0 0 0 ms Then, we have to get a root shell on the drone; we connect by using the telnet server which it runs natively. l i n u x $ t e l n e t 1 9 2 . 1 6 8 .

Finishing the ARDSYS debootstrap process

From the drone root shell, we have to switch to our ARDSYS partition system in order to finish the debootstrap process. The USB flash drive is identified by the drone as sda. The new Linux operating system is now fully installed and ready to run.

ARDSYS auto-boot

We are now going to modify the core init scripts of the drone and ARDSYS partition in order to switch automatically from the drone operating system to ARDSYS if the USB flash drive is plugged at drone startup time. The startup process is summarized in Figure 1. Then, we create the init script which mounts devices into the ARDSYS partition and chroots to it. Finally, the script calls the init script of the ARDUSR partition. This last script will be developed in the next section. a r d r o n e $ touch /mnt/ i n i t a r d r o n e $ chmod 777 /mnt/ i n i t

The content of the file /mnt/init has to be as follows.

#! / b i n / sh

s l e e p 3 ; IRD=$ ( dirname $ ( r e a d l i n k -f $0 ) ) ; mount -t tmpfs -o s i z e =8M tmpfs $IRD/tmp ; mount --bind / dev $IRD/ dev ; mount --bind / p r o c $IRD/ p r o c ; mount --bind / s y s $IRD/ s y s ; mount --bind / dev / p t s $IRD/ dev / p t s ; mount / dev / sda3 $IRD/mnt ; c h r o o t $IRD /mnt/ i n i t ;

Then, we test the init script process by rebooting the drone and checking if ARDSYS directories are well mounted after drone startup.

a r d r o n e $ r e b o o t

Once the drone has started, we reconnect the Linux base station to the drone as explained in paragraph 2.4.2. Then, we get a telnet shell on the drone. l i n u x $ t e l n e t 1 9 2 . 1 6 8 . 1 . 1

We can check that all the directories are properly mounted. a r d r o n e $ mount / dev / sda1 on /mnt type e x t 2 tmpfs on /mnt/tmp type tmpfs dev on /mnt/ dev type tmpfs p r o c on /mnt/ p r o c type p r o c s y s on /mnt/ s y s type s y s f s d e v p t s on /mnt/ dev / p t s type d e v p t s / dev / sda3 on /mnt/mnt type v f a t

The ARDSYS auto-boot process is now complete.

ArDroneXT customization

ARDSYS configuration

There are some modifications that can be applied to the ARDSYS partition.

Upgrading packages repository

# f i l e / e t c / a p t / s o u r c e s . l i s t deb h t t p : / / f t p . f r . d e b i a n . o r g / d e b i a n / s q u e e z e main c o n t r i b non-f r e e deb-s r c h t t p : / / f t p . f r . d e b i a n . o r g / d e b i a n / s q u e e z e main c o n t r i b non-f r e e deb h t t p : / / s e c u r i t y . d e b i a n . o r g / s q u e e z e / u p d a t e s main c o n t r i b non-f r e e deb-s r c h t t p : / / s e c u r i t y . d e b i an . o r g / s q u e e z e / u p d at e s main c o n t r i b non-f r e e

Changing host name

# f i l e / e t c / hostname ArDroneXT

Customizing telnet connection message

# f i l e / e t c / i s s u e |----------------------| |-My Wonderful ArDrone -| |----------------------|

Defining shell init

# f i l e / r o o t / . b a s h r c # c o n f i g u r e as you w i s h

We also need to create a script in order to directly launch a root shell. It will be used in the next section. This script is called sroot and has to be installed in the /bin of the ARDSYS partition. We also need to create scripts in order to halt and reboot the drone. Indeed, the operating system in the ARDSYS partition (i.e. ArDroneXT) cannot perform these tasks directly, their use is reserved to the core drone operating system. Calling halt or reboot from the ARDSYS partition will not have any effect. Therefore, we use the local telnet server to send instructions to the original base system of the drone. The script will be called sreturn and will be placed in the /bin of the ARDSYS partition. The content of the file /mnt/bin/sreturn has to be as follows.

#! / b i n / sh i f [ $# -eq 0 ] then
/ b i n / busybox t e l n e t 1 2 7 . 0 . 0 . 1 ; e l s e echo "$ * ; e x i t " | n e t c a t 1 2 7 . 0 . 0 . 1 2 3 ; f i

ARDUSR init script

We now have to create a user init script in the ARDUSR partition that will be launched by ArDroneXT just after executing the chroot. This script will enable to launch services at the drone startup time. It is suitable for instance to:

1. set the drone hostname; 2. launch a telnet server inside the ARDSYS partition (port 2323 for instance); 3. enable the drone to communicate with internet to perform some packages installation.

The telnet server will make it possible to run a root shell directly on ArDroneXT without passing by the original drone base system (i.e. ArDroneBS).

Here is an example of such a script which is installed in ARDUSR/init. #! / b i n / b a s h TELNET_PORT=2323; GATEWAY_IP= 1 9 2 . 1 6 8 . 1 . 2 ; hostname $ ( cat / e t c / hostname ) ; / b i n / busybox t e l n e t d -p ${TELNET_PORT} -l ' / b i n / s r o o t ' ; r o u t e add d e f a u l t gw ${GATEWAY_IP} ; echo " nameserver ␣${GATEWAY_IP}" > / e t c / r e s o l v . c o n f ;

We can also install new packages. For instance, we can install Python [START_REF]Python[END_REF].

ArDroneXT$ apt-g e t i n s t a l l python

It is of course possible to install more packages if needed.

Ad-hoc networking

In this section we modify the ARDUSR init script in order to force the drone to join a specific ad-hoc network. This feature enables to create a swarm of several Ar.Drone 2 which shares the same Wi-Fi network.

We first have to install wireless-tools [START_REF] Hp | Linux Wireless Tools[END_REF] in order to configure the Wi-Fi connection.

ArDroneXT$ apt-g e t i n s t a l l w i r e l e s s -t o o l s

ARDUSR init script upgrade

We now upgrade the ARDUSR init script in order to force the drone to join a pre-existing ad-hoc network with a predefined IP address. We also need to enable the broadcast ICMP reply (i.e. ping reply) on the drone in order to check ad-hoc network peers status. By default, the drone ignores ICMP requests sent in broadcast. The resulting script is detailed hereafter. We can create a DHCP server on our Linux base station and force the drone to use it in order to get its network configuration automatically at startup. However we will first have to bypass the original drone DHCP server. The resulting script is given bellow. We can setup the DHCP server on the Linux base station with dnsmasq [START_REF] Kelley | Dnsmasq[END_REF]. In the following example, our Linux base station has a wireless interface called wlan0 which IP address is set to 192.168.1.254. l i n u x $ / u s r / s b i n / dnsmasq --i n t e r f a c e=wlan0 \ --s t r i c t -o r d e r \ --expand-h o s t s \ --domain="ArDroneXT" \ --dhcp-r a n g e = 1 9 2 . 1 6 8 . 1 . 1 0 , 1 9 2 . 1 6 8 . 1 . 1 0 0 , 2 h \ --dhcp-o p t i o n=" o p t i o n : r o u t e r , 1 9 2 . 1 6 8 . 1 . 2 5 4 "

Ad-Hoc network creation

Then, we just have to turn the drone on and to configure the Wi-Fi chip of the base station to join the ad-hoc network. Please note that it is recommended that the Linux base station initiates the ad-hoc network to prevent any drone join problem. Indeed, we have noticed that the drone sometimes encounters some problems to init a new ad-hoc network. This problem stills unresolved for the moment. l i n u x $ i f c o n f i g wlan0 down l i n u x $ i w c o n f i g wlan0 mode ad-hoc l i n u x $ i w c o n f i g wlan0 e s s i d ArDroneXT l i n u x $ i f c o n f i g wlan0 up l i n u x $ i f c o n f i g wlan0 1 9 2 . 1 6 8 . 1 . 2 5 4 6 Supporting ARM EABI (using ARDSYS partition without drone)

This section enables to run programs directly inside the ARDSYS partition without using a drone.

The cross-execution problem

As explained above, the architecture of programs in ARDSYS is ARM EABI compliant. There is a strong probability that our Linux base station lays on a different processor architecture like x86_64 for instance. Consequently, it is theoretically impossible to launch ARDSYS programs directly on our Linux base station.

However, it is possible to use an emulator in order to solve the problem. A well known solution is QEMU [START_REF] Bellard | QEMU[END_REF]. It can emulate a lot of architectures including ARM EABI. After installing QEMU on our Linux base station, we will then be able to run ARM EABI programs directly.

For example, we create a simple ARM EABI executable thanks to our ARDDEV partition as follows. l i n u x $ export PATH=$PATH: / mnt/ARDDEV/arm-2012/ b i n / l i n u x $ cd /tmp l i n u x $ echo "#i n c l u d e ␣<s t d i o . h>" > h e l l o . c l i n u x $ echo ' i n t main ( ) { p r i n t f ( " I t ␣ works \n" ) ; return 0 ; } ' >> h e l l o . c l i n u x $ arm-none-l i n u x -gnueabi-g c c h e l l o . c -o h e l l o . e l f l i n u x $ f i l e h e l l o . e l f h e l l o . e l f : ELF 32-b i t LSB e x e c u t a b l e , ARM, EABI5 v e r s i o n 1 (SYSV) d y n a m i c a l l y l i n k e d ( u s e s s h a r e d l i b s ) l i n u x $ . / h e l l o . e l f . / h e l l o . e l f : cannot e x e c u t e b i n a r y f i l e : i n v a l i d a r c h i t e c t u r e fo r exec ( ) As we can see, we cannot run the hello.elf executable because of its ARM EABI architecture. We use QEMU to bypass the problem. l i n u x $ qemu-arm . / h e l l o . e l f / l i b / ld-l i n u x . s o . 3 : No such f i l e o r d i r e c t o r y

The error we get is due to the fact that the hello.elf program uses shared libraries which are not installed on our Linux base station. We thus have to compile our program in static mode to solve this issue. l i n u x $ arm-none-l i n u x -gnueabi-g c c h e l l o . c --s t a t i c -o h e l l o . e l f l i n u x $ f i l e h e l l o . e l f h e l l o . e l f : ELF 32-b i t LSB e x e c u t a b l e , ARM, EABI5 v e r s i o n 1 (SYSV) s t a t i c a l l y l i n k e d l i n u x $ qemu-arm . / h e l l o . e l f I t works

Applying cross-execution to ARDSYS

It is possible to adapt the previous solution to the whole ARDSYS partition in order to support the ARM EABI architecture directly on our Linux base station. The trick is to indicate to our system that it has to use QEMU for all ARM EABI programs. Most Linux distributions enable this binding when QEMU is installed. If your Linux distribution does not perform this action, please refer to Linux kernel module binfmt_misc [START_REF]Binary Formats Kernel Support[END_REF].

Then, we have just to perform a chroot inside ARDSYS. Please note that a chroot implies a file system isolation, thus we have to copy the QEMU executable inside the ARDSYS partition. We also have to use the static version of QEMU as explained in section 6.1. l i n u x $ f i l e $ ( which qemu-arm ) qemu-arm : ELF 64-b i t LSB e x e c u t a b l e , x86 -64 , v e r s i o n 1 (GNU/ Linux ) d y n a m i c a l l y l i n k e d ( u s e s s h a r e d l i b s ) l i n u x $ f i l e $ ( which qemu-arm-s t a t i c ) qemu-arm-s t a t i c : ELF 64-b i t LSB e x e c u t a b l e , x86 -64 , v e r s i o n 1 (GNU/ Linux ) s t a t i c a l l y l i n k e d

We copy the static version of the executable inside the ARDSYS partition. l i n u x $ cp $ ( which qemu-arm-s t a t i c ) /mnt/ARDSYS/ u s r / b i n / Now we can mount sub-directories and chroot in the same way we would have done if using a drone. l i n u x $ mount --bind / dev /mnt/ARDSYS/ dev l i n u x $ mount --bind / p r o c /mnt/ARDSYS/ p r o c l i n u x $ mount --bind / s y s /mnt/ARDSYS/ s y s l i n u x $ mount --bind / dev / p t s /mnt/ARDSYS/ dev / p t s l i n u x $ c h r o o t /mnt/ARDSYS ArDroneXT$ Then we can run any ARM EABI application. Please not that we first have to call the DHCP server because the network configuration (DNS server, default gateway, etc.) is not inherited when chrooting.

ArDroneXT$ d h c l i e n t e t h 0 # run any commands

1 . 1

 11 Trying 1 9 2 . 1 6 8 . 1 . 1 . . . Connected t o 1 9 2 . 1 6 8 . 1 . 1 . Escape C h a r a c t e r i s ' ^] ' . BusyBox v1 . 1 4 . 0 ( ) b u i l t -i n s h e l l ( ash ) Enter ' help ' fo r a l i s t o f b u i l t -i n commands . a r d r o n e $

  a r d r o n e $ mount / dev / sda1 /mnt a r d r o n e $ mount --bind / dev /mnt/ dev a r d r o n e $ mount --bind / p r o c /mnt/ p r o c a r d r o n e $ mount --bind / s y s /mnt/ s y s a r d r o n e $ mount --bind / dev / p t s /mnt/ dev / p t s a r d r o n e $ c h r o o t /mnt We finish the debootstrap process from within the ARDSYS partition. a r d s y s $ cd d e b o o t s t r a p a r d s y s $ . / d e b o o t s t r a p --second-s t a g e a r d s y s $ exi t We also copy the BusyBox [16] program of the original Linux to our new one. BusyBox provides light versions of several standard Linux tools. a r d r o n e $ cp / b i n / busybox /mnt/ b i n /

Figure 1 :

 1 Figure 1: ArDroneXT startup

  a r d r o n e $ touch /mnt/ b i n / s r o o t a r d r o n e $ chmod 777 /mnt/ b i n / s r o o t The content of the file /mnt/bin/sroot has to be as follows. #! / b i n / sh i f [ $# -eq 0 ] then su r o o t -c / b i n / bash ; e l s e su r o o t -c "$ * " ; f i

  a r d r o n e $ touch /mnt/ b i n / s r e t u r n a r d r o n e $ chmod 777 /mnt/ b i n / s r e t u r n

  cat / e t c / hostname ) ; i f c o n f i g ath0 down ; i w c o n f i g ath0 mode ad-hoc ; i w c o n f i g ath0 e s s i d ${ESSID } ; i w c o n f i g ath0 commit ; i f c o n f i g ath0 up ; i f c o n f i g ath0 $IP ; echo 0 > / p r o c / s y s / n e t / i p v 4 / icmp_echo_ignore_broadcasts ; / b i n / busybox t e l n e t d -p ${TELNET_PORT} -l ' / b i n / s r o o t ' ; r o u t e add d e f a u l t gw ${GATEWAY_IP} ; echo " nameserver ␣${GATEWAY_IP}" > / e t c / r e s o l v . c o n f ;

  cat / e t c / hostname ) ; i p t a b l e s -t f i l t e r -A OUTPUT -p udp --s p o r t 67 -j DROP; i p t a b l e s -t f i l t e r -A INPUT -p udp --d p o r t 67 -j DROP; i f c o n f i g ath0 down ; i w c o n f i g ath0 mode ad-hoc ; i w c o n f i g ath0 e s s i d ${ESSID } ; i w c o n f i g ath0 commit ; i f c o n f i g ath0 up ; d h c l i e n t ath0 ; echo 0 > / p r o c / s y s / n e t / i p v 4 / icmp_echo_ignore_broadcasts ; / b i n / busybox t e l n e t d -p ${TELNET_PORT} -l ' / b i n / s r o o t ' ;

Table :

 : Unless enough free and un-partitioned space is available on the USB flash drive, it is necessary to erase all previous data before creating the new partitions.

	l i n u x $ p a r t e d / dev / sdb rm 1
	l i n u x $ p a r t e d / dev / sdb p r i n t
	. . .
	Number S t a r t	End	S i z e	Type	F i l e system
	Then, we create the partitions table.
	l i n u x $ p a r t e d / dev / sdb mkpart primary 1 5663
	l i n u x $ p a r t e d / dev / sdb mkpart primary 5663 6737
	l i n u x $ p a r t e d / dev / sdb mkpart primary 6737 7747
			msdos
	Number S t a r t	End	S i z e	Type	F i l e system
	1	1049kB 7747MB 7746MB primary f a t 3 2

  / i n i t . d/ x t S t a r t a r d r o n e $ chmod 777 / e t c / i n i t . d/ x t S t a r t a r d r o n e $ cp / e t c / i n i t . d/ r c S / e t c / i n i t . d/ r c S . back a r d r o n e $ echo ' / e t c / i n i t . d/ x t S t a r t &' >> / e t c / i n i t . d/ r c S The content of the file /etc/init.d/xtStart has to be as follows.

	#! / b i n / sh
	s l e e p 4 ;
	i f [ -e / dev / sda ]
	then
	mount / dev / sda1 /mnt ;
	/mnt/ i n i t ;
	f i

ARDSYS upgrade

Now we plug the USB flash drive and start the drone. After enabling the Wi-Fi connection, we have to contact our new telnet server.

$ t e l n e t 1 9 2 . 1 6 8 . 1 . 1 2323 |----------------------- ----------------------| ArDroneXT$

We have to enable the drone to communicate with internet in order to install new packages. To achieve this task, we need (on the Linux base station):

• to enable IP forwarding;

• to start a DNS server relay;

• to set a NAT masquerading.

The require commands are listed bellow. l i n u x $ echo 1 > / p r o c / s y s / n e t / i p v 4 / ip_forward l i n u x $ dnsmasq l i n u x $ i p t a b l e s -t nat -A POSTROUTING --s o u r c e 1 9 2 . 1 6 8 . 1 . 0 / 2 4 \ -o e t h 0 -j MASQUERADE;

Now the drone can communicate with internet.

ArDroneXT$ p i n g -c1 www. l a b r i . f r PING www3 . l a b r i . f r ( 1 4 7 . 2 1 0 . 8 . 5 9 ) 5 6 ( 8 4 ) b y t e s o f data . 64 b y t e s from www3 . l a b r i . f r ( 1 4 7 . 2 1 0 . 8 . 5 9 ) : icmp_req=1 t t l =61 time =3.84 ms ---www3 . l a b r i . f r p i n g s t a t i s t i c s ---1 p a c k e t s t r a n s m i t t e d , 1 r e c e i v e d , 0% p a c k e t l o s s , time 0ms r t t min/ avg /max/mdev = 3 . 8 4 5 / 3 . 8 4 5 / 3 . 8 4 5 / 0 . 0 0 0 ms We can now perform a Debian update/upgrade. ArDroneXT$ apt-g e t update ArDroneXT$ apt-g e t upgrade ArDroneXT$ apt-g e t d i s t -upgrade ArDroneXT$ apt-g e t a u t o c l e a n ArDroneXT$ apt-g e t autoremove

If we choose the DHCP configuration to set the drone IP address automatically, we have to launch the dnsmasq tool as explained in the previous section.

Finally, we can test if several drones are part of the swarm by using a broadcast ping. Each drone that is part of the ad-hoc network should reply and thus be visible. In the following example, 2 drones are part of the network (192.168. 1.10 and 192.168

Swarm of several Ar.Drone 2

In order to configure other drones, we have, for each one:

• to clone the USB flash drive;

• to create the /etc/init.d/xtStart script in the drone root file system as explained in section 2.5;

• to upgrade the /etc/init.d/rcS script in the drone root file system as explained in section 2.5;

• optionally:

to change the drone IP in ARDUSR/init if it is set in this file; -to customize the hostname of the drone.

To clone a USB flash drive we can use the dd [START_REF]Coreutils[END_REF] software. In the following example, the original USB flash drive is sdb and the new one is sdc.