Jérôme Leroux
email: jerome.leroux@labri.fr

The Reachability Problem for Petri Nets is Not Primitive Recursive *

We provide an Ackermannian complexity lower bound for the reachability problem for checking programs, a model equivalent to Petri nets. Moreover in fixed dimension 2d + 4, we show that the problem is F d -hard. As a direct corollary, the reachability problem in dimension 10 is not elementary.

Introduction

Checking programs [START_REF] Leroux | The reachability problem for petri nets is not primitive recursive[END_REF], or equivalently vector addition systems with states [START_REF] Hopcroft | On the reachability problem for 5-dimensional vector addition systems[END_REF], or vector addition systems [START_REF] Karp | Parallel program schemata[END_REF], or Petri nets are one of the most popular formal methods for the representation and the analysis of parallel processes [START_REF] Esparza | Decidability issues for petri nets -a survey[END_REF].

Those equivalent models are acting on counters ranging over the natural numbers thanks to increment, decrement, and test commands (only at the end of an execution). The central algorithmic problem for checking programs is reachability: given a checking program, decide whether there exists an execution from an initial configuration to a final one. Many important computational problems in logic and complexity reduce or are even equivalent to this problem [START_REF] Schmitz | The complexity of reachability in vector addition systems[END_REF][START_REF] Hack | Decidability questions for Petri nets[END_REF]. After an incomplete proof by Sacerdote and Tenney [START_REF] Sacerdote | The decidability of the reachability problem for vector addition systems (preliminary version)[END_REF], decidability of the problem was established by Mayr [START_REF] Mayr | An algorithm for the general petri net reachability problem[END_REF][START_REF] Mayr | An algorithm for the general Petri net reachability problem[END_REF], whose proof was then simplified by Kosaraju [START_REF] Kosaraju | Decidability of reachability in vector addition systems (preliminary version)[END_REF]. Building on the further refinements made by Lambert in the 1990s [START_REF] Lambert | A structure to decide reachability in Petri nets[END_REF], in 2015, a first complexity upper bound of the reachability problem was provided [START_REF] Leroux | Demystifying reachability in vector addition systems[END_REF] more than thirty years after the presentation of the algorithm introduced by Mayr [START_REF] Kosaraju | Decidability of reachability in vector addition systems (preliminary version)[END_REF][START_REF] Lambert | A structure to decide reachability in Petri nets[END_REF]. The upper bound given in that paper is "cubic Ackermannian", i.e. in F ω 3 (see [START_REF] Schmitz | Complexity hierarchies beyond elementary[END_REF]). This complexity bound is obtained by analyzing the Mayr algorithm. With a refined algorithm and a new ranking function for proving termination, an Ackermannian complexity upper bound was obtained [START_REF] Leroux | Reachability in vector addition systems is primitive-recursive in fixed dimension[END_REF] This means that the reachability problem can be solved in time bounded by A(p(n)) where p is a primitive recursive function and where A is the Ackermann function. This paper also showed that the reachability problem in fixed dimension d (the dimension is the number of used counters) is primitive recursive by bounding the length of executions by O(F d+4 (n)) where F d+4 is a primitive recursive function of the Grzegorczyk hierarchy (see Section 2 for the definition of those functions), and n is the size of the input.

Concerning the complexity lower bound, in 1976, the reachability problem was proved to be ExpSpace-hard [START_REF] Cardoza | Exponential space complete problems for petri nets and commutative semigroups: Preliminary report[END_REF]. This bound used to be the best one for more than forty years until 2019 when it was improved to a Tower complexity lower bound [START_REF] Czerwiński | The reachability problem for petri nets is not elementary[END_REF], i.e. a non elementary complexity.

Contributions. In this paper we provide an Ackermannian complexity lower bound for the reachability problem for checking programs closing the gap with the Ackermannian complexity upper bound solving a 45 years old open problem. Moreover, in fixed dimension 2d + 4 with d ≥ 3, we prove that the reachability problem is hard for the complexity class F d introduced in [START_REF] Schmitz | Complexity hierarchies beyond elementary[END_REF] associated with the function F d . As a direct corollary, we derive that the reachability problem is not elementary in dimension 10.

This paper provides the last piece leading to the exact complexity of the reachability problem for checking programs. As previously mentioned, it follows a long series of results. This piece of work is not the most difficult one but it is an important one since it closes a long standing open problem. Technically, the most difficult piece is the notion of K-amplifiers introduced in the Tower complexity lower bound paper [START_REF] Czerwiński | The reachability problem for petri nets is not elementary[END_REF] that provides a way to postpone at the end of an execution the tests commands of a Minsky machine (a machine like a VASS but with commands that can test to zero some counters) with counters bounded by K.

In this paper, we provide several gadgets for proving an F d complexity lower bound for the reachability problem in dimension 2d + 4. Recently and independently, other gadgets for implementing such a bound have been introduced in order to obtain the same complexity upper bound by Wojciech Czerwiński, and Lukasz Orlikowski [START_REF] Czerwinski | Reachability in vector addition systems is ackermann-complete[END_REF] in dimension 6d, by myself [START_REF] Leroux | The reachability problem for petri nets is not primitive recursive[END_REF] in dimension 4d + 5, and by S lawomir Lasota [START_REF]Improved ackermannian lower bound for the vass reachability problem[END_REF] in dimension 3d + 2. We do not know if the lower bound provided in this paper, i.e. F d in dimension 2d + 4 is optimal since the complexity upper bound is F d+4 in dimension d. It follows that the parameterized complexity (i.e. in fixed dimension) of the reachability problem is still open.

We think that several different solutions to the complexity lower bound for the reachability problem is useful not only for the confidence in the claimed result but also for future work. In fact, the reachability problem for many extensions is open for almost all natural extensions except for vector addition systems with hierarchical zero tests [START_REF] Bonnet | The reachability problem for vector addition system with one zerotest[END_REF][START_REF] Reinhardt | Reachability in petri nets with inhibitor arcs[END_REF]. Moreover, the best known complexity lower bounds for those models only come from checking programs. Finding gadgets that take benefits from the extra power given by the considered extensions is an open problem.

Outline. In Section 2, we recall some properties satisfied by the fast growing functions F d and introduce a way to compute F d be iterating a reduction rule evalF d . In Section 3 we introduce the model of general programs, and the subclasses of test-free models that correspond to programs that cannot test counters to zero, and the checking programs that can only test counters at the end. Whereas the reachability problem for test-free program is equivalent to the so-called coverability problem for Petri nets (see [START_REF] Cardoza | Exponential space complete problems for petri nets and commutative semigroups: Preliminary report[END_REF][START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF] for complexity results), the reachability problem for checking program is equivalent to the so-called reachability problem for Petri nets. In Section 4 we provide tools to postpone at the end of an execution test commands of a general program. Those tools are used in Section 5 in order to simulate the bounded semantics of general programs thanks to the so-called preamplifiers. In Section 6 we provide tools for iterating a testfree program a fixed number of times that depends on the valuation of some counters. Those tools are used in Section 7 to implements evalF d thanks to a test-free program. By iterating this test-free program, we provide a way in Section 8 to implement an Ackermannian preamplifier. Finally, in Section 9 we collect intermediate results to provide complexity lower bounds for the reachability problem for checking programs.

Fast Growing Functions

We introduce the sequence (F d ) d∈N of functions F d : N → N defined by F 0 (n) = n + 1, and defined by induction on d ≥ 1 by

F d (n) = F n+1 d-1 (n).
Rather than take the original definition of Ackermann function, we let A(n) = F ω (n) defined by F ω (n) = F n+1 (n), which behaves like the classical function for our complexity-theoretical purpose. We introduce the function F v : N → N with v ∈ N d , defined as follows for every n ∈ N:

F v (n) = F v[d] d • • • • • F v[1] 1 (n) Remark 1. We have F 1 (n) = 2n + 1 and F 2 (n) = 2 n+1
(n + 1) -1 for every n ∈ N. The function F 3 behaves like a tower of n exponential and it is not elementary. Each function F d is primitive recursive and F ω is not primitive recursive.

Let us denote by 0 d the zero vector of N d , and by 1 d,i the ith unit vector of N d defined for every 1 ≤ j ≤ d by 1 d,i [j] = 1 if j = i and 1 d,i [j] = 0 otherwise. The lexicographic (strict) order < lex over N d is defined by w < lex v if w = v and the maximal p ∈ {1, . . . , d} such that w

[p] = v[p] satisfies w[p] < v[p].
Let evalF d : N d × N → N d × N be the function partially defined over the pairs (v, n) ∈ N d × N such that v = 0 d as follows where p is the minimal index in {1, . . . , d} such that v[p] > 0:

evalF d (v, n) = (v -1 d,p , 2n + 1) if p = 1 (v -1 d,p + (n + 1)1 d,p-1 , n) if p > 1 Since F p (n) = F n+1
p-1 (n), one can easily prove (see [START_REF] Schnoebelen | Revisiting ackermann-hardness for lossy counter machines and reset petri nets[END_REF] for more details) that if v = 0 d , then the pair (w, m) defined as evalF

d (v, n) satisfies F w (m) = F v (n). It follows that the function that maps (v, n) onto F v (n) is an invariant of evalF d .
Moreover, as w < lex v, it follows that we can iterate the function evalF d on a pair (v, n) only a finite number of times (we use the well-foundedness of the lexicographic order). Let us introduce the function evalF max

d : N d × N → N d × N defined by evalF max d (v, n) = evalF k d (v, n)
where k is the maximal number of times (it can be zero) we can apply the function evalF

d on (v, n). Notice that evalF max d (v, n) is a pair of the form (w, m) for some pair (w, m) ∈ N d × N. Moreover, by maximality of k, it follows that w = 0 d . Since the function (v, n) → F v (n) is an invariant of evalF d , we deduce that F 0 d (m) = F v (n).
It follows that the following equality holds (see [START_REF] Schnoebelen | Revisiting ackermann-hardness for lossy counter machines and reset petri nets[END_REF] for more details):

evalF max d (v, n) = (0 d , F v (n))
As a direct corollary, we deduce the following lemma. The following lemma will be useful in the sequel. In that lemma,

|v| is v[1] + • • • + v[d] for any vector v ∈ N d . Lemma 3. We have F v (n) ≥ 2 |v| n + |v| for every v ∈ N d and for every n ∈ N. Proof. Let v ∈ N d and n ∈ N. Assume that for every w ∈ N d such that w < lex v we have F w (m) ≥ 2 |w| m + |w| for every m ∈ N.
And let us prove that in that case F v (n) ≥ 2n |v| + |v| for every n ∈ N. In fact, since the lexicographic order is well-founded, by induction the proof of the lemma reduces to that statement.

Notice that if v = 0 d then F v (n) = n and we are done. So, we can assume that v = 0 d . In that case, let us introduce (w, m)

= evalF d (v, n). Since w < lex v, it follows that F w (m) ≥ 2 |w| m+|w|. Since F w (m) = F v (n), we get F v (n) ≥ 2 |w| m + |w|. Let p ∈ {1, . . . , d} be the minimal index such that v[p] > 0. Observe that if p = 1 then |w| = |v| -1 and m = 2n + 1. In particular 2 |w| m + |w| ≥ 2 |v| n + |v|. If p > 1 then |w| = |v| + n and m = n. Hence 2 |w| m + |w| ≥ 2 |v| n + |v|.
We have proved that F v (n) ≥ 2 |v| n + |v| in any case.

General Programs

We introduce in the section the formal model of programs acting on counters ranging over the natural numbers.

Formally, an implicit infinite countable set of elements called counters is given. A configuration is a function ρ that maps every counter on a natural number in such a way that the set of counters c such that ρ(c) = 0 is finite. We denote by 0 the configuration ρ such that ρ(c) = 0 for every counter c. The increment, decrement and test commands of a counter c are respectively denoted as inc(c), dec(c), and test(c). We associate with such a command cmd, the binary relation cmd ---→ over the configurations defined by α cmd ---→ β if α(x) = β(x) for every counter x = c, and satisfying additionally:

     β(c) = α(c) + 1 if cmd is inc(c) β(c) = α(c) -1 if cmd is dec(c) β(c) = 0 = α(c) if cmd is test(c)
A (general) program M is defined as an increment/decrement/test command, or inductively as a loop program loop M 0 , a series composition M 1 ; M 2 , or a non-deterministic choice M 1 or M 2 where M 0 , M 1 , M 2 are programs. The size of a program M is the number size(M ) defined inductively as

1 if M is a command, 1 + size(M 0 ) if M = loop M 0 , and 1 + size(M 1 ) + size(M 2 ) if M = M 1 ; M 2 or M = M 1 or M 2 .
The dimension of M is the cardinal of the set of counters used by M , and formally defined as expected. We associate with every program M the binary relation M -→ over the configurations defined as follows:

M -→ =              cmd ---→ if M = cmd is a command ( M 0 --→) * if M = loop M 0 M 1 --→; M 2 --→ if M = M 1 ; M 2 M 1 --→ ∪ M 2 --→ if M = M 1 or M 2
Where (→ 0 ) * is the reflexive and transitive closure of → 0 , and → 1 ; → 2 is defined by α → 1 ; → 2 β if there exists a configuration ρ such that α → 1 ρ and ρ → 2 β. Series compositions and non-deterministic choices are clearly associative with respect to the relation →. In particular given a sequence M 1 , . . . , M n of Minsky programs, the relations M 1 ;...;Mn ------→ and M 1 or ... or Mn ----------→ are well defined. We denote by M (n) the series composition of M by itself n times. We also denote by inc(c 1 , . . . , c n ) the program inc(c 1 ); . . . ; inc(c n ), by dec(c 1 , . . . , c n ) the program dec(c 1 ); . . . ; dec(c n ), and similarly test(c 1 , . . . , c n ) the program test(c 1 ); . . . ; test(c n ).

We say that a program is test-free if it does not use any test command. A checking program is a program of the form M ; test(c 1 , . . . , c n ) where M is a test-free program and c 1 , . . . , c n are some counters.

The reachability problem for general programs asks, given a general program M , whether there exists a configuration β such that 0 M -→ β. This problem is undecidable [START_REF] Minsky | Computation: finite and infinite machines[END_REF] even in dimension 2 but provides a way to define complexity classes beyond Elementary as recalled in Section 9. The reachability problem for test-free programs is equivalent (i.e. inter-reducible) to the so-called coverability problem for Petri nets (see [START_REF] Cardoza | Exponential space complete problems for petri nets and commutative semigroups: Preliminary report[END_REF][START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF] for the complexity of the problem), and the reachability problem for checking programs is equivalent (i.e. inter-reducible) to the so-called reachability problem for Petri nets.

In this paper, we use standard notions from model theory by considering counters as variables, and configurations as valuations of the variables. It means that a configuration is used to replace in an expression e over the counters, each occurrence of a counter c by ρ(c). We denote by ρ(e) the expression we obtain this way. When φ is a constraint over the counters, we also denote by ρ(φ) the constraint we obtain by considering φ as an expression over the counters. We say that ρ satisfies φ if the constraint ρ(φ) is true. For instance we say that ρ satisfies y = 2 c x where y, c and x are counters if ρ(y) = 2 ρ(c) ρ(x).

Simulating Test Commands

We provide in this section the central idea for simulating test commands. Assume that B denotes a finite set of counters. The simulation of a test command test(c) for some counter c ∈ B is using two distinct auxiliary counters x and y not in B. During the simulation, we consider configurations ρ satisfying y ≥ Kx where K = ρ( b∈B b). Intuitively, when the configuration satisfies y = Kx it means that all the previous simulation of test commands were correct and when y > Kx is means that at least one simulation was incorrect. ;dec(y) dec(x) (2) Intuitively this program is transferring the content of the counter b i into b i-1 thanks to the ith loop with i ∈ {1, . . . , d}. Then the program is transferring back the contents of the counters thanks to the last d loops. During each step of the transfer, the counter y is decremented. Since K = b∈B b is an invariant, the counter y can be decremented by at most K in total with the first d loops, and by K as well in total with the last d loops. It follows that y can be decremented by at most 2K. Moreover, the only way to decrement y by exactly 2K is when initially c = 0 and when all loops are executed the maximal number of times, meaning that the transfers are total, and in particular that the initial and the final configurations coincide on the counters in B. Since x is decremented by 2, it follows that if y ≥ Kx before the execution of the program, then the same constraint holds at the end. Moreover, if additionally y = Kx at the end, then necessarily the same constraint holds at the beginning and it means that y has been decremented by 2K, and in particular initially c = 0 and all the transfers were performed maximally. The following two lemmas formally proved those intuitions. Lemma 4. Let α, β be two configurations such that α test(c);dec(y) (2K) dec(x) (2) - ---------------→ β with c ∈ B and such that K = α( b∈B b). Then we have:

α simtest y,B,y (c) ---------→ β
Proof. We are going to prove that there exists an execution in such a way the loops are executed m 1 , . . . , m d , n d , . . . , n 1 times (in that order), where m i = n i = α(b i ) for every 1 ≤ i ≤ d. Notice that the decrement commands dec(y) cannot prevent such an execution since α(y) ≥ 2K = d i=1 (n i + m i ). Moreover, the decrement commands dec(x) (2) are also executable at the end of the program since α(x) ≥ 2. So, for proving the existence of an execution of the program with the loops executed the right number of times, we can forget the decrement commands on the counters y and x.

For the first d loops, such an execution is possible by observing that the ith loop with i ∈ {1, . . . , d} only decrements the counter b i (recall that we forget the counter y for the proof) that is untouched by the previous loops. After executing those d first loops, we get a configuration ρ satisfying for every counter c the following equalities:

ρ(c) =            α(b i+1 ) if c = b i with 0 ≤ i < d 0 if c = b d α(y) -K if c = y α(c) otherwise
Starting form ρ, the last d loops are symmetrical to the first d loops. In particular, the same argument as previously mentioned shows that there exists an execution from ρ that executes the last d loops the right number of times. Now, just observe that with such an execution, we have proved the lemma.

Lemma 5. Let α, β be two configurations such that α

simtest y,B,x (c)
---------→ β and let K = α( b∈B b). Then β( b∈B b) = K and if α satisfies y ≥ Kx then β satisfies the same constraint. Moreover if additionally β satisfies y = Kx then α satisfies the same constraint and:

α test(c);dec(y) (2K) dec(x) (2)
- ---------------→ β Proof. Let us denote by m 1 , . . . , m d , n d , . . . , n 1 the number of times loops of the program are executed (in that order). Observe that the ith loop with i ∈ {1, . . . , d} decrements the counter b i , and that counter is untouched by the previous loops. It follows that there exists a sequence r 1 , . . . , r d of natural numbers such that m i = α(b i )r i for every i ∈ {1, . . . , d}. We derive the following equality by observing that d i=0 α(b i ) = K:

d i=1 m i = K -α(b 0 ) - d i=1 r i
Let us denote by ρ the configuration we obtain just after executing those d first loops. Since

d i=1 n i = K -ρ(b d ) - d i=1 s i From β(y) = α(y) -d i=1 (m i + n i ) and β(x) = α(x) -2,
we deduce the following equalities:

β(y -Kx) = α(y -Kx) + 2K - n i=1 (m i + n i ) = α(y -Kx) + α(b 0 ) + ρ(b d ) + d i=1 (r i + s i )
Now, assume that α satisfies y ≥ Kx. From the previous equality, we deduce that β(y -Kx) is a sum of natural numbers. In particular β satisfies y ≥ Kx. If additionally β satisfies y = Kx the previous equality shows that α(y -Kx) = 0, α(b 0 ) = 0, ρ(b d ) = 0, and

r i = s i = 0 for every 1 ≤ i ≤ d. From r i = 0 for every 1 ≤ i ≤ d, it follows that m i = α(c i ) for every 1 ≤ i ≤ d. We deduce that ρ(b i ) = α(b i+1 ) for every 0 ≤ i < d. Now, from s i = 0 for every 1 ≤ i ≤ d, we deduce that n i = α(b i+1 ) for every 1 ≤ i ≤ d. In particular β(b i ) = α(b i ) for every 0 ≤ i ≤ d.
Finally, just observe that from d i=1 m i = K and d i=1 n i = K, we deduce that β(y) = α(y) -2K. We have proved the lemma.

Bounded Semantics and Preamplifiers

We introduce in this section the K-bounded semantics of general programs, where K is a natural number. Intuitively this semantics is obtained by bounding the sum of the counters by K. We also introduce the notion of K-preamplifiers that provides a way to simulate the Kbounded semantics of general programs thanks to checking programs equipped with the classical (unbounded) semantics.

More formally, we say that a configuration ρ is K-bounded for some

K ∈ N if c ρ(c) ≤ K.
Denoting by Conf ≤K the set of K-bounded configurations, we define the binary relation M -→ ≤K over Conf ≤K where M is a general program inductively as follows:

M -→ ≤K =              ( cmd ---→) ∩ (Conf ≤K × Conf ≤K ) if M = cmd is a command ( M 0 --→ ≤K ) * ∩ (Conf ≤K × Conf ≤K ) if M = loop M 0 M 1 --→ ≤K ; M 2 --→ ≤K if M = M 1 ; M 2 M 1 --→ ≤K ∪ M 2 --→ ≤K if M = M 1 or M 2
Intuitively α M -→ ≤K β for two configurations α, β if, and only if, there exists an execution of M such that every visited configuration including α and β, during the computation is Kbounded. The relation

M -→ ≤K is called the K-bounded semantics of M .
The K-bounded semantics can be simulated by checking programs thanks to the so-called K-preamplifiers. A K-preamplifier [START_REF] Czerwiński | The reachability problem for petri nets is not elementary[END_REF] for a triple of counters (x, y, b) is a checking program A such that:

• For every configuration β such that 0 A -→ β we have y ≥ bx and β(c) = 0 for every counter c ∈ {x, y, b}. Moreover, if β satisfies y = bx then β(b) = K.

• For every ℓ ≥ 1 there exists a configuration β satisfying 0 A -→ β, y = bx, and x = ℓ. Remark 6. A K-amplifier [START_REF] Czerwiński | The reachability problem for petri nets is not elementary[END_REF] for a triple of counters (x, y, b) is a checking program A such that for any configuration β, we have 0 A -→ β if, and only if, there exists ℓ > 0 such that β(x, y, b) = (ℓ, Kℓ, K) and such that β(c) = 0 for any counter c ∈ {x, y, b}. From a Kpreamplifier, one can compute a K-amplifier by introducing some additional counters. We do not introduce K-amplifiers in this paper in order to reduce the number of counters used by the simulation. We say that a counter c used by the preamplifier A is unsafe (for the simulation), if it belongs to {x, y, b} or if it occurs in a test command at the end of A, and let us say it is safe if it is not unsafe. Then denoting by u and s respectively the number of unsafe and safe counters of A, the dimension of A ⊲ M is equal to u + max(s, d).

Given a K-preamplifier

The checking program A ⊲ M is obtained as follows. By renaming the counters of A, we can assume without loss of generality that the unsafe counters of A are disjoint from the counters used by M . Moreover, with such a renaming we can additionally assume that the cardinal of the safe counters of A union the counters used by M is max(s, d). We assume that A is a checking program of the form A ′ ; test(c 1 , . . . , c n ) where A ′ is a test-free program. We can assume that b is not in {c 1 , . . . , c n } since otherwise K = 0 and in this case A can by replaced by the 0-preamplifier loop inc(x). We denote by B the counters used by M union {b}. By adding a test command test(c) for some counter c used by M , we can assume that M starts with a test command (notice that if M is not using any counter, then M is the empty program and the construction A ⊲ M can be defined as M ).

We introduce the test-free program M ′ obtained from M by replacing each increment command inc(c) by inc(c); dec(b), each decrement command dec(c) by dec(c); inc(b), and each test command test(c) by simtest x,B,y (c). The checking program A ⊲ M is then defined as follows:

A ⊲ M = A' M' loop dec(b) test(x, y, b, c 1 , . . . , c n )
For every configuration β, we have 0 M -→ ≤K β if, and only if, 0 A⊲M ---→ β. A formal proof for a variant construction of A ⊲ M (that cannot reuse safe counters of A, that introduces several additional test commands, and that uses additional counters) is given in [START_REF] Czerwiński | The reachability problem for petri nets is not elementary[END_REF]. In the next two paragraphs, we just recall briefly the key ingredients used for the formal proof.

For one direction, assume that 0 M -→ ≤K β for some configuration β and let us consider an execution of M from 0 to β such that every visited configuration including β is K-bounded. Denoting by m the number of times this execution is using a test command, we introduce ℓ = 2m. Since M starts with a test command, it follows that ℓ > 0. We consider an execution of A ′ that leads to a configuration ρ such that ρ(x, y, b) = (ℓ, Kℓ, K) and ρ(c) = 0 for every counter c ∈ {x, y, b}. Observe that ρ satisfies K = ρ( c∈B c). From the execution of M , we derive an execution of M ′ from ρ to a configuration δ satisfying δ(x) = 0, δ(y) = 0, and δ(c) = β(c) for every counter c used by M . In fact, every time a test command test(c) is executed, it is simulated by simtest x,B,y (c) using Lemma 4 that decrements x by 2, and y by 2K. Finally, from δ we iterate the last loop exactly δ(b) times in such a way we get the configuration β. This configuration can then execute the last test commands of A ⊲ M .

For the other direction, assume that 0 A⊲M ---→ β for some configuration β and let us consider an execution of A ⊲ M witnessing that property. In A ⊲ M the test-free program A ′ is executed first and the test commands test(c 1 , . . . , c n ) of A are postponed at the end of A⊲M . Since those tested counters are no longer used in between, the execution of A ′ can only produce from the zero configuration a configuration ρ satisfying y ≥ bx and ρ(c) = 0 for every counter c ∈ {x, y, b}. We denote by δ the configuration obtained from ρ after executing M ′ . Let K ′ = ρ(b). Assume by contradiction that ρ satisfies the strict constraint y > K ′ x. Lemma 5 shows that δ satisfies the same strict inequality. In particular β(y) = δ(y) > 0 and the last test command test(y) fails on β. We get a contradiction. It follows that δ satisfies the equality y = bx and since A is a K-preamplifier, we get K ′ = K in that case. Lemma 5 shows that δ satisfies y ≥ Kx. Moreover, since β(y) = β(x) = 0 we deduce that δ satisfies the equality y = Kx. From Lemma 5 we deduce that every execution of simtest x,B,y (c) in M ′ has the same effect as the execution of test(c); dec(y) (2K) ; dec(x) (2) . From the execution of M ′ we deduce that α M -→ ≤K β.

It follows that the K-bounded semantics of general programs can be simulated by checking programs of small size as soon as there exists small size K-preamplifiers.

Loop at Most

In this section we present a way to iterate test-free programs a numbers of times that depends on the valuation of some counters. Given two distinct counters c and c ′ , and a test-free program M , we introduce the following test-free program:

Loop at most c + c ′ times M = loop dec(c);inc(c ′ ) loop dec(c ′ );inc(c);M
Let us denote by C the counter expression c + c ′ . In the following lemmas, we assume that M is any test-free program that does not use the counters c and c ′ . Lemma 7. For every configuration α, β, we have: ----------------→ β if, and only if, there exists n, ℓ ∈ N such that n ≤ α(c), ℓ ≤ n + α(c ′ ), and such that: ------------------------→ β In particular ℓ ≤ α(C). If this inequality is an equality then β(c) = α(C) and β(c ′ ) = 0.

α Loop at most c + c ′ times M --
α (dec(c);inc(c ′ )) (n) ;(dec(c ′ );inc(c);M ) (ℓ)
Proof. We denote by N and N n,ℓ the following test-free programs where n, ℓ ∈ N:

N = 1: loop 2: dec(c);inc(c ′ ) 3: loop 4: dec(c ′ );inc(c);M N n,ℓ = (dec(c); inc(c ′ )) (n) (dec(c ′ ); inc(c); M ) (ℓ)
Let α, β be two configurations such that α N -→ β. We fix some execution witnessing that property. Let n be the number of times line 2 is executed and ℓ be the number of times line 4 is executed. Since each execution of line 2 decrements c, we deduce that after executing the first loop we get a configuration ρ satisfying ρ(c) = α(c)n and ρ(c ′ ) = α(c ′ ) + n. In particular n ≤ α(c). Symmetrically, since each execution of line 4 decrements c ′ , we deduce that

β(c ′ ) = ρ(c ′ ) -ℓ = α(c ′ ) + n -ℓ and β(c) = ρ(c) + ℓ = α(c) -n + ℓ. In particular ℓ ≤ n + α(c ′ ). Observe that α N n,ℓ ---→ β. Moreover, we have ℓ ≤ α(c). Observe that if ℓ = α(C), then from β(c ′ ) = α(c ′ ) + n -ℓ we get β(c ′ ) = n -α(c).
In particular n ≥ α(c) and with n ≤ α(c) we get n = α(c). We deduce that β(c) = α(C) and β(c ′ ) = 0.

Conversely, let α, β be two configurations such that α ------------------------→ β if, and only if, there exists n, ℓ ∈ N such that n ≤ α(c), ℓ ≤ n + α(c ′ ), and such that: --------------------------→ β In particular ℓ ≤ α(C) and β(C) ≤ 2α(C). If one of those two inequalities is an equality then ℓ = α(C), β(c) = 2α(C), and β(c ′ ) = 0.

α (dec(c);inc(c ′ )) (n) ;(dec(c ′ );inc(c) (2) ;M ) (ℓ)
Proof. The proof is very similar to the proof of Lemma 7.

Lemma 9. For every configuration α, β, we have: -----------------------→ β if, and only if, there exists n, ℓ ∈ N such that n ≤ α(c), ℓ ≤ n+α(c ′ ) 2 , and such that: -----------------------------→ β In particular ℓ ≤ α(C)

α Loop at most c + c ′ times (dec(c ′ ); M ) -
α (dec(c);inc(c ′ )) (n) ;(dec(c ′ );inc(c);dec(c ′ );M ) (ℓ)
2 . If this inequality is an equality then β(c) = α(C) 2 , and β(c ′ ) = 0.

Proof. We denote by N and N n,ℓ the following test-free programs where n, ℓ ∈ N:

N = 1: loop 2: dec(c);inc(c ′ ) 3: loop 4: dec(c ′ );inc(c);dec(c ′ );M N n,ℓ = (dec(c); inc(c ′ )) (n) (dec(c ′ ); inc(c); dec(c ′ ); M ) (ℓ)
Let α, β be two configurations such that α N -→ β. We fix some execution witnessing that property. Let n be the number of times line 2 is executed and ℓ be the number of times line 4 is executed. Since each execution of line 2 decrements c, we deduce that after executing the first loop we get a configuration ρ satisfying ρ(c) = α(c)n and ρ(c ′ ) = α(c ′ ) + n. In particular n ≤ α(c). Symmetrically, since each execution of line 4 decrements c ′ two times, we deduce that

β(c ′ ) = ρ(c ′ ) -2ℓ = α(c ′ ) + n -2ℓ and β(c) = ρ(c) + ℓ = α(c) -n + ℓ. In particular ℓ ≤ n+α(c ′ ) 2 .
Observe that α N n,ℓ ---→ β. Moreover, we have ℓ ≤ α(C) 2 . Observe that if ℓ = α(C) 2 , then from β(c ′ ) = α(c ′ ) + n -2ℓ we get β(c ′ ) = nα(c). In particular n ≥ α(c) and with n ≤ α(c) we get n = α(c). We deduce that β(c) = α(C) 2 and β(c ′ ) = 0. Conversely, let α, β be two configurations such that α -----------------------------→ β if, and only if, there exists n, ℓ ∈ N such that n ≤ α(c), ℓ ≤ n+α(c ′ ) 2 , and such that: ---------------------------→ β In particular ℓ ≤ α(C) 2 . If this inequality is an equality then β(c) = α(C), and β(c ′ ) = 0.

α (dec(c);inc(c ′ )) (n) ;((dec(c ′ );inc(c)) (2) ;M ) (ℓ)
Proof. The proof is very similar to the proof of Lemma 9.

Implementing evalF d

In this section, we introduce a test-free program evalF d that implements the function evalF d . This program is using counters x, x ′ , x 1 , . . . , x d+1 , y, b, b ′ , c 0 , c ′ 0 , c 1 , . . . , c d . We say that a configuration ρ is good if it satisfies x ′ = y = b ′ = c ′ 0 = 0, x > 0, b = 2 c 0 , x 1 = 2 c 0 x and x i = 2 c i-1 x i-1 for every i ∈ {2, . . . , d + 1}. We say that a good configuration ρ encodes a pair (v, n)

∈ N d × N if ρ(c 1 , . . . , c d ) = v and ρ(c 0 ) = n.
Remark 11. The counters x and x ′ should have been denoted as x 0 and x ′ 0 to simplify a little bit the definition of good configurations. However, since those two counters appear many times in the sequel, we prefer the notation without indexes. Moreover, this notation match the one used for preamplifiers. In fact, in the next section we introduce an Ackermannian preamplifier for the triple of counters (x, y, b) without any variable renaming.

We introduce the counter expressions C 0 , X and B defined as c 0 + c ′ 0 , x + x ′ , and b + b ′ respectively.

Intuitively, when the computation of evalF d is correct from a good configuration that encodes a pair (v, n) with v = 0 d then the computation terminates on a good configuration that encodes evalF d (v, n). When the computation is incorrect, we obtain a so-called bad configuration. Moreover, from a bad configuration any computation of evalF d leads to a bad configuration. Formally, we say that a configuration is i-bad for some i ∈ {2, . . . , d + 1} if it satisfies x + x ′ > 0, x i + y > 2 c i-1 (x i-1 + y), and x j + y = 2 c j-1 (x j-1 + y) for every j

∈ {i + 1, . . . , d + 1}. A configuration is 1-bad if is satisfies x ′ = y = 0, x > 0, b + b ′ < 2 c 0 +c ′ 0 , x 1 = 2 c 0 +c ′ 0
x, and x j = 2 c j-1 x j-1 for every j ∈ {2, . . . , d + 1}. We say that a configuration α is bad if it is i-bad for some i. A configuration that is good or bad is said to be conform. We associate to any conform configuration α its index of badness index(α) defined by index(α) = i if α is i-bad, and by index(α) = 0 if α is good. Intuitively, from any conform configuration α, the computation of evalF d can only produce conform configurations β such that index(β) ≥ index(α). In particular, if β is good, then α is good as well.

The program evalF d is defined as a non-deterministic choice of programs evalF d,p with p ∈ {1, . . . , d}. Intuitively from a good configuration α that encodes a pair (v, n) with v = 0 d , the computation of evalF d,p can lead to a good configuration only if p is the minimal index such that v[p] > 0. In that case the good configuration produced at the end of the computation encodes evalF d (v, n).

We introduce the following test-free program for p ∈ {1, . . . , d}. The first loop at line 2 intuitively transfer min x 1 , . . . , x d into y. Thanks to Lemma 7, the second loop at line 6 transfer back from y the value of X. Notice that x p is incremented twice during each iteration of the loop. The loop at line 6 is interpreted thanks to Lemma 7 if p > 1 and Lemma 8 if p = 1 as a loop that is iterated C 0 times, the loop at line 8 is interpreted thanks to Lemma 9 as a loop that is iterated X times and that divides X by 2, and finally the loop at line 10 is interpreted thanks to Lemma 7 as a loop that is iterated B times. Where updateB d,p is the empty program if p > 1 and the following one if p = 1. Notice that the loop at line 2 can be interpreted thanks to Lemma 10 as a loop that is iterated C 0 2 times, and the loop at line 4 is interpreted thanks to Lemma 8 as a loop that multiply by 2 the value of B.

updateB d,1 = 1: inc(c 0 ) 2: loop at most c 0 + c ′ 0 times 3: dec(c ′ 0 );inc(c 0 ) 4: loop at most b + b ′ times 5:
inc(b)

6: dec(c 0 )
We first provide two lemmas describing the behaviour of updateB d,1 .

Lemma 12. Assume that α updateB d,1

-------→ β for any two configurations α, β. Then β(C 0 ) = α(C 0 ) and we have:

β(B) ≤ α(2 C 0 +1 2 B) (1)
If the previous inequality is an equality and α(B) > 0 then β satisfies b ′ = 0 and c ′ 0 = 0.

Proof. Let s be the number of times line 3 is executed. Lemma 10 shows that s ≤ 1+α(C 0 ) 2 (the 1 in the expression comes form the increment command at line 6). Let ρ j-1 for j ∈ {1, . . . , s} be the configuration just before executing that line the jth time. We also denote by ρ s the configuration just before the execution of line 6. Lemma 8 shows that ρ j (B) ≤ ρ j-1 (B) for every j ∈ {1, . . . , s}. We deduce that the inequality (1) holds. If this inequality is an equality and α(B) > 0, then s = 1+α(C 0 ) 2 . Lemma 10 shows that β(c ′ 0 ) = 0. Notice that since the inequality ( 1) is an equality, then the inequality ρ j (B) ≤ 2ρ j-1 (B) is also an equality for every j ∈ {1, . . . , k}. In particular ρ k (b ′ ) = 0 from Lemma 8. It follows that β(b ′ ) = 0. -------→ β where β is the configuration defined for every counter c as follows:

β(c) =                α(C 0 ) if c = c 0 0 if c = c ′ 0 α(2 C 0 +1 2 B) if c = b 0 if c = b ′ α(c) otherwise
Proof. Just observe that we can apply Lemma 10 and Lemma 8.

Lemma 14. Let α be a conform configuration and β be any configuration such that α evalF d,p

-----→ β with p ∈ {1, . . . , d}. Then β is conform and index(β) ≥ index(α). In particular, if β is good then α is good. In that case, α satisfies b divides x, denoting by (v, n) the pair encoded by α then v = 0 d , p is the minimal index such that v[p] > 0, evalF d (v, n) is encoded by β, and β(x d+1 ) = α(x d+1 ).

Proof. Let r, s, k, m and n be the number of times lines 3, 5, 7, 9, and 11 are executed respectively. Observe that r ≤ min{α(x 1 ), . . . , α(x d+1 )} since every time line 3 is executed, the counters x 1 , . . . , x d+1 are decremented, s ≤ α(X) thanks to Lemma 7, k ≤ α(C 0 ), thanks to Lemma 7 if p > 1 and Lemma 8 if p = 1 (in fact in that case c p-1 = c 0 ), and n ≤ α(B)m thanks to Lemma 7.

Let us prove that β(X) > 0. Observe that α(X) > 0 since α is conform. Moreover, line 9 is the unique line that may prevent β(X) > 0 holding. However, each time this line is executed, by definition of loop at most, notice that x is incremented just before. It follows that β(X) > 0.

For each j ∈ {1, . . . , k}, let m j be the number of times line 9 is executed during the jth execution of the loop at line 6. We denote by α j-1 the configuration just before the jth execution of line 9, and by α k the configuration just before executing updateB d,p . Notice that α 0 (X) = α(X), 2m j ≤ α j-1 (X), and α j (X) = α j-1 (X)m j for every j ∈ {1, . . . , k}. Let us denote by h j the natural number such that α j-1 (X) = 2m j + h j . By induction on i ∈ {0, . . . , k}, we get the following equality:

i j=1 m j = α(X)[1 -2 -i ] - i j=1 2 j-i-1 h j
In particular with i = k, since m = k j=1 m j , we get the following equality by introducing the non negative rational number h = k j=1 2 j-k-1 h j :

2 α(C 0 ) m = -2 α(C 0 ) h - 1 2 k α(X)(2 α(C 0 ) -2 k ) + α((2 C 0 -1)X) (2)
Assume first that α is i-bad for some i ∈ {p + 2, . . . , d + 1}. In that case α satisfies x i + y > 2 c i-1 (x i-1 + y), and x j + y = 2 c j-1 (x j-1 + y) for every j ∈ {i + 1, . . . , d + 1}. Notice that β also satisfies the same constraints since x j + y for j ∈ {i, . . . , d + 1}, and c j for j ∈ {i, . . . , d} are invariant. Hence β is i-bad in that case.

So we can assume that α is not i-bad for every i ∈ {p + 2, . . . , d + 1}. Since α is conform, we deduce that α satisfies x p+1 + y ≥ 2 cp (x p + y), and x j + y = 2 c j-1 (x j-1 + y) for every j ∈ {p + 2, . . . , d + 1}. Since x j + y for j ∈ {p + 1, . . . , d + 1}, and c j for j ∈ {p + 1, . . . , d} are invariant, we deduce that β satisfies x j + y = 2 c j-1 (x j-1 + y) for every j ∈ {p + 2, . . . , d + 1}.

Observe that we have the following equalities:

β(x p+1 + y) = α(x p+1 + y) β(c p ) = α(c p ) -1 β(x p + y) = α(x p + y) + s + n β(y) = α(y) + r -(s + n)
From those equalities, we derive:

β(x p+1 + y -2 cp (x p + y)) = α(x p+1 + y -2 cp (x p + y)) + 2 α(cp)-1 (α(x p ) -r) + 2 α(cp)-1 β(y)
Notice that the right hand-side of the last equality is a sum of three natural numbers. It means that if one of those numbers is strictly positive, then β is (p + 1)-bad. So, we can assume that those three numbers are zero. It means that α and β satisfies x p+1 + y = 2 cp (x p + y), r = α(x p ), and β(y) = 0. In particular α is not (p + 1)-bad. Assume by contradiction that α is i-bad for some i ∈ {2, . . . , p}. It means that α satisfies x i + y > 2 c i-1 (x i-1 + y) and x j + y = 2 c j-1 (x j-1 + y) for every j ∈ {i + 1, . . . , d + 1}. In particular α satisfies x i > x i-1 and x j ≥ x j-1 for every j ∈ {i + 1, . . . , d}. We deduce that α satisfies x i < x p . It follows that r ≤ min{α(x 1 ), . . . , α(x d+1 )} < α(x p ) = r and we get a contradiction. Since α is not i-bad for every i ∈ {2, . . . , d + 1}, we deduce that α is 1-bad or good. In both cases, α satisfies x ′ = y = 0, B ≤ 2 C 0 , x 1 = 2 C 0 x, and x i = 2 c i-1 x i-1 for every i ∈ {2, . . . , d + 1}. In particular α(x d+1 ) ≥ • • • ≥ α(x) > 0. Notice that from α(y) = 0 and β(y) = 0, we deduce from

β(y) = α(y) + r -(s + n) that r = s + n.
Assume by contradiction that α(c i-1 ) > 0 for some i ∈ {2, . . . , p}. Since α satisfies x i = 2 c i-1 x i-1 , c i-1 > 0, and x i-1 > 0, we deduce that α(x i ) > α(x i-1 ). In particular, α(x p ) ≥ α(x i ) > α(x i-1 ). Like in the previous paragraph we get a contradiction with r ≤ min{α(x 1 ), . . . , α(x d+1 )} < α(x p ) = r. Therefore α(c i-1 ) = 0 for every i ∈ {2, . . . , p}. We deduce that α(x 1 ) = • • • = α(x p ). It follows from r = α(x p ) and r = s + n that α(x 1 ) = s + n.

Observe that we have (by developing the equalities and replacing 2 α(C 0 ) m by using the equality 2):

n = -(α(B)m -n) -α(2 B 0 -B)m -2 α(C 0 ) h - 1 2 k α(X)(2 α(C 0 ) -2 k ) + α((2 C 0 -1)X)) s = -(α(X) -s) + α(X)
It follows that we have (we use the fact that α(x 1 -2 C 0 X) = 0):

0 = α(x 1 ) -(s + n) =(α(B)m -n) + (2 α(C 0 ) -α(B))m + (α(X) -s) + 2 α(C 0 ) h + 1 2 k α(X)(2 α(C 0 ) -2 k )
Since each term of the right hand side of the previous equality are non negative, we deduce that all the terms are zero. It means that n

= α(B)m, (2 α(C 0 ) -α(B))m = 0, s = α(X), h = 0, 2 α(C 0 ) = 2 k (for the last equality, we use α(X) > 0). Since k ≤ α(C 0 ) we derive from 2 α(C 0 ) = 2 k that k = α(C 0 )
. By replacing h by 0, and k by α(C 0 ) in equation 2, we derive

m = α((1 -2 -C 0 )X). Assume that α is 1-bad. In that case α(B) < 2 α(C 0 ) . It follows from (2 α(C 0 ) -α(B))m = 0 that m = 0. From m = α((1 -2 -C 0 )X) and α(X) > 0 we get α(C 0 ) = 0. So, from α(B) < 2 α(C 0 )
we get α(B) = 0. Observe that in that case β is 1-bad (the case p = 1 is obtained thanks to Lemma 12). So, we can now assume that α is not 1-bad.

Since α is conform and not bad, we deduce that α is good. Hence α satisfies x ′ = c ′ 0 = b ′ = y = 0 and b = 2 c 0 . It follows from n = α(B)m that n = α((2 C 0 -1)X). Let ρ be the configuration we obtain just before executing updateB d,p . Since h = 0, then h k = 0. It follows that ρ(x ′ ) = 0. As s = α(X), Lemma 7 shows that ρ(x ′ ) = 0. Moreover, as n = α(B)m, Lemma 7 shows that ρ(b ′ ) = 0. It follows that ρ(x) = α(x)m = α(2 -c 0 x). Notice that ρ(x i ) with i ∈ {1, . . . , p -1} is equal to α(x i )r + s = s = α(x). We also have ρ(x p ) = α(x p )r + 2s + 2n = 2α(x p ). Notice that ρ(x i ) with i ∈ {p + 1, . . . , d + 1} is equal to α(x i ) since x i + y is an invariant and α(y) = ρ(y) = 0.

It follows that for every counter c, we have:

ρ(c) =                          0 if c ∈ {x ′ , c ′ 0 , b ′ , y} α(2 -c 0 x) if c = x α(x) if c = x i with i ∈ {1, . . . , p -1} 2α(x p ) if c = x p α(c p ) -1 if c = c p α(1 + c p-1 + c 0 ) if c = c p-1 α(c) otherwise
Notice that if p > 1 then α(c p-1 ) = 0 and β = ρ. In that case β is good and satisfies the lemma. If p = 1, notice that ρ(c 0 ) = 1 + 2α(c 0 ). From Lemma 12 we deduce that β is either 1-bad or good depending depending if the inequality of that lemma is strict or an equality. Notice that if the inequality is an equality, the configuration β is good and it encodes evalF d (v, n).

Lemma 15. Let α be a good configuration satisfying b divides x and that encodes a pair (v, n) with v = 0 d , and let p is the minimal index such that v[p] > 0. There exists a good configuration β that encodes evalF d (v, n) satisfying β(x d+1 ) = α(x d+1 ), and such that α

evalF d,p -----→ β.
Proof. We are going to prove that there exists an execution of evalF d,p from α such that lines 3, 5, 7 are executed r, s, k times with:

r = α(x 1 ) s = α(x) k = α(c 0 )
We also introduce the configurations that will appear along the execution of loop at line 6. To do so, we introduce the configurations α 0 , . . . , α k defined as follows for every counter c and for every j ∈ {0, . . . , k}:

α j (c) = α                                                                     x 2 j if c = x x if c = x i with i ∈ {1, . . . , p -1} 2bx + 2x(1 -2 c 0 -j ) if c = x p x i + x(1 -2 c 0 -j ) if c = x i with i ∈ {p + 1, . . . , d + 1} x(2 c 0 -j -1) if c = y c p -1 if c = c p c p-1 + 1 + j if c = c p-1 and p > 1 c 0 -j if c = c ′ 0 j if c = c 0 and p > 1 1 + 2j if c = c 0 and p = 1 c otherwise                       
Since α is good, it follows that α(x i ) ≥ r for every i ∈ {1, . . . , d + 1}, and r ≥ α(x). In particular line 3 and 5 can be effectively executed r and s times respectively. Notice that α 0 is the configuration we obtain after executing those two loops and the hidden first loop of the loop at most at line 6 exactly α(x) times.

We introduce the test-free program N corresponding to the subprogram between line 7 and line 11 (including those those lines) and prefixed by dec(c ′ 0 ); inc(c 0 ). Let us prove by induction on j ∈ {1, . . . , k} that α j-1 N -→ α j . To do so, we are going to prove that there exists an execution of N such that lines 9, 11 are executed m j , n j times with:

m j = α j-1 ( x 2 ) n j = α j-1 (m j b)
Notice that those three numbers are natural numbers since 2 k divides α(x). This execution is obtained thanks to Lemma 7 applied on line 11 in order to execute maximally the corresponding loop, and by applying Lemma 9 applied on line 9. We have proved that α j-1

M

-→ α j . In particular, by executing k times loop 6, we get the configuration α k . Notice that this configuration satisfies for every counter c:

α k (c) = α                                                x b if c = x x if c = x i with i ∈ {1, . . . , p -1} 2bx if c = x p x i if c = x i with i ∈ {p + 1, . . . , d + 1} 0 if c = y c p -1 if c = c p c p-1 + 1 + c 0 if c = c p-1 c otherwise                
In particular, by executing updateB d,1 following Lemma 13 (if p = 1), we get from α k a configuration β satisfying the lemma.

Since the test-free program evalF d is defined as evalF d,1 or • • • or evalF d,d , we deduce from Lemma 14 and Lemma 15 the following two corollaries.

Ackermannian Preamplifiers

In this section we prove that the following checking program is a K-preamplifier for K ----→ β. To do so, we consider an execution of Ack d,n defined as follows. We execute the first loop 2 F d+1 (n)-2n-1 ℓ -1 times (recall that F d+1 (n) ≥ 2n + 1). Just after this loop we get a good configuration ρ 0 that encodes ((0, . . . , 0, n), n + 1) and such that ρ 0 (x d+1 ) = Kℓ. Then we iterate evalF d as many times as possible following Lemma 15. This way we get a sequence ρ 0 , . . . , ρ k of good configurations such that ρ j (x d+1 ) = 2 F d+1 (n) ℓ and such that ρ j encodes the pair (v j , n j ) defined as (v j , n j ) = evalF j d ((n + 1)1 d,d , n). Since F v j (n j ) does not depend on j, we deduce that

= 2 F d+1 (n) of size O(d4 n ). Ack d,n = 1: inc(c 0 ) (n) ; inc(c d ) (n+1) 2: inc(x); inc(x 1 , . . . , x d ) (2 n ) ; inc(x d+1 ) (2 2n+1 ) 3: loop 4: inc(x); inc(x 1 , . . . , x d ) (2 n ) ; inc(x d+1 ) (2 2n+1
F v j (n j ) = F v 0 (n 0 ) = F n+1 d (n) = F d+1 (n). Since ρ k is a good configuration, it follows that ρ k satisfies b = 2 c 0 and x d+1 = 2 c d +•••+c 0 x. As ρ k encodes (v j , n j ), we deduce that ρ k (b) = 2 n j and ρ k (x) = 2 F d+1 (n)-n j -|v j | ℓ.
We have proved the following equality:

ρ k ( x b ) = 2 Fv k (n k )-2n k -|v k | Lemma 3 shows that if v k = 0 d then ρ k satisfies b divides x.
In particular from the good configuration ρ k we can execute evalF d one more time following Lemma 15 and get a contradiction with the maximality of k. It follows that We denote by ρ 0 the configuration we obtain after executing the first loop. Let k be the number of times the second loop is executed and let us denote by ρ j the configuration we obtain after the jth execution of the second loop for j ∈ {1, . . . , k}. Lemma 14 shows that ρ j is conform.

v k = 0 d . From F v k (n k ) = F d+1 (n), we deduce that n k = F d+1 (n). Hence ρ k (b) = K. Since v k = 0 d and ρ k is a good configuration, we deduce that ρ k satisfies x d+1 = • • • = x 1 . It follows that ρ k (x i ) =
Assume by contradiction that ρ k is i-bad for i ∈ {2, . . . , d + 1}. In that case ρ k satisfies x i + y > 2 c i-1 (x i-1 + y) and x j + y = 2 c j (x j-1 + y) for every j ∈ {i + 1, . . . , d + 1}. In particular ρ k (x d+1 ) > ρ k (x i-1 ). It follows that whatever the number of time the third loop is executed, the configuration β satisfy β(x d+1 ) > β(x i-1 ) and the last test command test(x d+1 ) fails. We get a contradiction. It follows that ρ k is 1-bad or good. Now, assume that ρ k is 1-bad. In that case

ρ k satisfies x ′ = y = 0, x > 0, b + b ′ < 2 c 0 +c ′ 0 , x 1 = 2 c 0 +c ′ 0 x and x i = 2 c i-1 x i-1
for every i ∈ {2, . . . , d+1}. Since the execution from ρ k to β only modify y, x 1 , . . . , x d+1 , c 0 , then β and ρ k coincides on the other counters. Since β successfully execute the last test commands, we deduce that ρ k satisfies b

′ = c ′ 0 = c 1 = • • • = c d = 0. It follows that ρ k satisfies x d+1 = • • • = x 1 . Since β(x d+1 ) = 0,
it means that third loop was executed ρ k (x d+1 ) times. We deduce that β(x i ) = 0 for every i ∈ {1, . . . , d}. It follows that β satisfies y > bx and β(c) = 0 for every counter c ∈ {x, y, b}.

Finally, assume that ρ k is good. From Lemma 14 we deduce that ρ j is good for every j ∈ {1, . . . , k} and denoting by (v j , n j ) the pair encoded by ρ j we have (v j , n j ) = evalF j d (v 0 , n 0 ). In particular F v j (n j ) = F d+1 (n). Since ρ k is good it satisfies x ′ = y = b ′ = c ′ 0 = 0, x > 0, b = 2 c 0 , x 1 = 2 c 0 x and x i = 2 c i-1 x i-1 for every i ∈ {2, . . . , d + 1}. Since the execution from ρ k to β only modify y, x 1 , . . . , x d+1 , c 0 , then β and ρ k coincides on the other counters. Since β successfully execute the last test commands, we deduce that ρ k satisfies c 1 = • • • = c d = 0. It follows that v k = 0 d and from F v k (n k ) = F d+1 (n) we get n k = F d+1 (n). Since ρ k satisfies b = 2 c 0 we deduce that ρ k (b) = K. Since ρ k satisfies x d+1 = • • • = x 1 and β(x d+1 ) = 0, it means that third loop was executed ρ k (x d+1 ) times. We deduce that β(x i ) = 0 for every i ∈ {1, . . . , d}. We have proved that β satisfies y = bx, ρ k (b) = K, and ρ k (c) = 0 for every counter c ∈ {x, y, b}.

Therefore Ack d,n is a K-preamplifier. It follows that the counter x d can be removed as well by observing that its value (for good configuration) is in fact equals to x d+1 2 -c d and the value of c d is hard coded in the control structure. This way, we get a K-preamplifier satisfying the lemma.

Complexity Classes Beyond Elementary

The reachability problem for general programs equipped with the bounded semantics provides a way to define complexity classes beyond Elementary. In fact, following [START_REF] Schmitz | Complexity hierarchies beyond elementary[END_REF], the problem that asks, given a 2-dimensional general program M of size n, whether there exists β such that 0 M -→ ≤K β with K = 2 F d (n) is F d -complete for every d ≥ 3. We deduce as a direct corollary the following theorem.

Theorem 20. The reachability problem for (2d + 4)-dimensional checking programs is F d -hard for any d ≥ 3. In particular the reachability problem for 10-dimensional checking programs is not Elementary.

Proof. Given a 2-dimensional program M , let n = size(M ). Corollary 19 shows that we can compute in time O(nd4 n ) a K-preamplifier A of size O(nd4 n ) with K = 2 F d (n) using 2(d -1) + 6 counters such that d -1 of them are safe. Now recall that the checking program N defined as A ⊲ M is computable in time size(A) + O(size(M )). It follows that N is computable in time O(nd4 n ). Moreover, as the number of safe counters of A is larger than or equal to 2, we deduce that the dimension of N is bounded by 2d + 4. Finally, just observe that for every configuration β we have 0 M -→ ≤K β if, and only if, 0 N -→ β.

Theorem 21 is nearly optimal since in [START_REF] Leroux | Reachability in vector addition systems is primitive-recursive in fixed dimension[END_REF] it is proved that the reachability problem for d-dimensional checking programs is in F d+4 .

Finally, let us recall [START_REF] Schmitz | Complexity hierarchies beyond elementary[END_REF] that the problem that asks, given a 2-dimensional general program M of size n, whether there exists a configuration β such that 0 M -→ ≤K β with K = 2 Fω(n) is F ω -complete. We deduce as a direct corollary the following theorem. Theorem 21 is optimal since in [START_REF] Leroux | Reachability in vector addition systems is primitive-recursive in fixed dimension[END_REF] it is proved that the reachability problem for checking programs is in F ω .

Conclusion

This paper proves that the reachability problem for checking programs is Ackermannian-complete. It also reduces the gap for the parameterized complexity of the reachability problem in fixed dimension. In order to close this gap, we see two possible research directions:

• Either we find a primitive recursive algorithm computing from d, n ∈ N a K-preamplifier for K = F d (n) with a dimension d + O(1),

• Or we find a new algorithm for deciding the reachability problem with a complexity upper bound in F d 2 +O(1) .

Lemma 2 .

 2 We have evalF max d ((n + 1)1 d,d , n) = (0 d , F d+1 (n)) for every n ≥ 0 and d ≥ 1.

  Those simulations are obtained by introducing the following test-free program. This program is using any implicit enumeration b 0 , . . . , b d of the counters in B satisfying b 0 = c. Such an enumeration naturally depends on the counter c. simtest y,B,x (c) = loop dec(b 1 );inc(b 0 );dec(y) . . . loop dec(b d );inc(b d-1 );dec(y) loop dec(b d-1 );inc(b d );dec(y) . . . loop dec(b 0 );inc(b 1 )

d i=0 b i is

  an invariant of every line of the program, we get β( d i=0 b i ) = K and ρ( d i=0 b i ) = K. Now, observe that the argument used in the previous paragraph holds for the last d loops. It follows that there exists a sequence s 1 , . . . , s d of natural numbers such that n i = ρ(b i-1 )s i for every 1 ≤ i ≤ d, and we derive the following equality:

  A and a general program M of dimension d, we can compute in time size(A) + O(d size(M )) a checking program A ⊲ M such that for any configuration β, we have 0 M -→ ≤K β, if, and only if, 0 A⊲M ---→ β. It follows that K-preamplifiers provide a way to postpone at the end of an execution test commands of general programs equipped with the K-bounded semantics. The size of A ⊲ M is size(A) + O(d size(M )). Concerning the dimension of A ⊲ M , let us first classify the counters used by A.

NLemma 8 .

 8 n,ℓ ---→ β for two natural numbers n, ℓ ∈ N such that n ≤ α(c) and ℓ ≤ n + α(c ′ ). Just observe that from the execution witnessing α N n,ℓ ---→ β, we deduce an execution witnessing α N -→ β by executing the first loop n times and the second loop ℓ times. For every configuration α, β, we have: α Loop at most c + c ′ times (inc(c); M )

N 2 .

 2 n,ℓ ---→ β for two natural numbers n, ℓ ∈ N such that n ≤ α(c) and ℓ ≤ n+α(c ′ ) Just observe that from the execution witnessing α N n,ℓ ---→ β, we deduce an execution witnessing α N -→ β by executing the first loop n times and the second loop ℓ times. Lemma 10. For every configuration α, β, we have: α Loop at most c + c ′ times (dec(c ′ ); inc(c); M )

evalF d,p = 1 : 10 :

 110 dec(c p );inc(c p-1 ) 2: loop 3: dec(x 1 , . . . , x d+1 );inc(y) 4: loop at most x + x ′ times 5: dec(y);inc(x p );inc(x 1 , . . . , x d+1 ) 6: loop at most c 0 + c ′ loop at most b + b ′ times 11: dec(y);inc(x p );inc(x p , . . . , x d+1 ) 12: updateB d,p

Lemma 13 .

 13 Let α be any configuration satisfying α(C 0 ) is odd. Then α updateB d,1

Corollary 16 .

 16 Let α be a conform configuration and β be any configuration such that α evalF d ----→ β. Then β is conform and index(β) ≥ index(α). In particular, if β is good then α is good. In that case, α satisfies b divides x, denoting by (v, n) the pair encoded by α then v = 0 d , evalF d (v, n) is encoded by β, and β(x d+1 ) = α(x d+1 ). Corollary 17. Let α be a good configuration satisfying b divides x and that encodes a pair (v, n) with v = 0 d . There exists a good configuration β that encodes evalF d (v, n) satisfying β(x d+1 ) = α(x d+1 ), and such that α evalF d ----→ β.

  )

8 :Lemma 18 .

 818 inc(y);dec(x 1 , . . . , x d+1 ) 9: loop 10:dec(c 0 ) 11: test(x d+1 , b ′ , c ′ 0 , c 0 , . . . , c d ) The checking program Ack d,n is a K-preamplifier for K = 2 F d+1 (n) .Proof. Let ℓ ≥ 1 and let β be the configuration satisfying β(x, y, b) = (ℓ, Kℓ, K) and β(c) = 0 for every counter c ∈ {x, y, b}. Let us prove that 0 Ack d,n

  Kℓ for every i ∈ {1, . . . , d + 1}. Based on this observation, from ρ k we can execute the third loop Kℓ times. Then we execute the last loop ρ k (c 0 ) times. This way, we get the configuration β.

Finally, let us consider a configuration β such that 0

 0 Ack d,n----→ β and let us prove that β satisfies y ≥ bx and β(c) = 0 for every counter c ∈ {x, y, b}. Moreover, if the inequality is an equality then let us prove that β(b) = K.

Theorem 21 .

 21 The reachability problem for checking programs isF ω -hard. Proof. Given a 2-dimensional program M , let n = size(M ). Corollary 19 shows that we can compute in time O(n 2 4 n ) a K-preamplifier A of size O(n 2 4 n ) with K = 2 F n+1 (n) = 2 Fω(n) . Now recall that the checking program N defined as A ⊲ M is computable in time size(A) + O(size(M )). It follows that N is computable in time O(n 2 4 n ).Finally, just observe that for every configuration β we have 0 M -→ ≤K β if, and only if, 0 N -→ β.

  Corollary 19. We can compute in time O(nd4 n ) a K-preamplifier of size O(nd4 n ) with K = 2 F d+1 (n) using 2d + 6 counters such that d of them are safe.Proof. The checking program Ack d,n is a K-preamplifier of size O(d4 n ) computable in time O(d4 d ) using 2d + 8 counters such that x ′ , x 1 , . . . , x d are safe counters. Notice that the counter c d is first initialized to n and then during an execution it is only decremented. It follows that its value can be encoded in the control structure of the program, i.e. by unfolding the program n times. Moreover, notice that during the execution, the value of x d + y can only increase.

Acknowledgements

I gratefully thank Philippe Schnoebelen for helpful comments and encouraging feedback.

This research has been supported by ANR programme BraVAS (ANR-17-CE40-0028).