Stéphane Demri

On Selective Unboundedness of VASS 1

Keywords: vector addition systems with states, place boundedness problem, regularity detection problem, exponential space

Numerous properties of vector addition systems with states amount to checking the (un)boundedness of some selective feature (e.g., number of reversals, counter values, run lengths). Some of these features can be checked in exponential space by using Rackoff's proof or its variants, combined with Savitch's Theorem. However, the question is still open for many others, e.g., regularity detection problem and reversal-boundedness detection problem. In the paper, we introduce the class of generalized unboundedness properties that can be verified in exponential space by extending Rackoff's technique, sometimes in an unorthodox way. We obtain new optimal upper bounds, for example for place boundedness problem, reversal-boundedness detection (several variants are present in the paper), strong promptness detection problem and regularity detection. Our analysis is sufficiently refined so as to obtain a polynomial-space bound when the dimension is fixed.

Introduction

Reversal-boundedness. A standard approach to circumvent the undecidability of the reachability problem for counter automata [START_REF] Minsky | Computation, Finite and Infinite Machines[END_REF] consists in designing subclasses with simpler decision problems. For instance, the reachability problem is decidable for vector addition systems with states (VASS) [START_REF] Mayr | An algorithm for the general Petri net reachability problem[END_REF][START_REF] Kosaraju | Decidability of reachability in vector addition systems[END_REF][START_REF] Leroux | Vector Addition System Reachability Problem (A Short Self-Contained Proof)[END_REF], for flat counter automata [START_REF] Comon | Multiple counters automata, safety analysis and Presburger analysis[END_REF][START_REF] Bozga | Fast acceleration of ultimately periodic relations[END_REF][START_REF] Demri | Taming Past LTL and Flat Counter Systems[END_REF] or for lossy counter automata [START_REF] Abdulla | Verifying programs with unreliable channels[END_REF]. Among the other interesting subclasses of counter automata, reversal-bounded counter automata verify that any counter has a bounded number of reversals, alternations between a nonincreasing mode and a nondecreasing mode, and vice versa. Reversal-boundedness remains a standard concept that is introduced in [START_REF] Baker | Reversal-bounded multipushdown machines[END_REF] for multistack automata. A major property of such operational models is that reachability sets are effectively definable in Presburger arithmetic [START_REF] Ibarra | Reversal-bounded multicounter machines and their decision problems[END_REF], which provides decision procedures for LTL existential model-checking and other related problems, see e.g. [START_REF] Dang | Liveness verification of reversal-bounded multicounter machines with a free counter[END_REF]. However, the class of reversal-bounded counter automata is not recursive [START_REF] Ibarra | Reversal-bounded multicounter machines and their decision problems[END_REF] but a significant breakthrough is achieved in [START_REF] Finkel | Reversal-bounded counter machines revisited[END_REF] by designing a procedure to determine when a VASS is reversalbounded (or weakly reversal-bounded as defined later), even though the decision procedure can be nonprimitive recursive in the worst-case. This means that reversal-bounded VASS can benefit from the known techniques for Presburger arithmetic [START_REF] Presburger | Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt[END_REF] in order to solve their verification problems. More precisely, we consider subclasses of counter systems for which the reachability sets of the form { x ∈ N n : (q 0 , x 0 ) * -→ (q, x)} are effectively Presburger-definable ((q 0 , x 0 ) and q are fixed). By decidability of Presburger arithmetic, this allows us to solve problems restricted to such counter systems such as the reachability problem, the control state reachability problem, the boundedness problem or the covering problem. Indeed, suppose that given (q 0 , x 0 ) and q, one can effectively build a Presburger formula ϕ such that ϕ holds true exactly for the values in { x ∈ N n : (q 0 , x 0 ) * -→ (q, x)}. One can then classically observe that (q 0 , x 0 ) * -→ (q, z) iff the formula below is satisfiable:

ϕ(x 1 , . . . , x n ) ∧ x 1 = z(1) ∧ • • • ∧ x n = z(n).
Hence, there is an important gain to have effectively semilinear reachability sets, which can be witnessed by detecting reversal-boundedness or by detecting regularity (guaranteeing the semilinearity by Parikh's Theorem [START_REF] Parikh | On context-free languages[END_REF]).

Selective unboundedness. In order to characterize the complexity of detecting reversal-boundedness on VASS (the initial motivation for this work), we make a detour to selective unboundedness, as explained below. Numerous properties of vector addition systems with states amounts to checking the (un)boundedness of some selective feature. Some of these features can be verified in exponential space by using Rackoff's proof or its variants [START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF], whereas the question is still open for many of them. In the paper, we advocate that many properties can be decided as soon as we are able to decide selective unboundedness, which is a generalization of place unboundedness for Petri nets (a model known to be equivalent to VASS but of greater practical appeal). The boundedness problem was first considered in [START_REF] Karp | Parallel program schemata[END_REF] and shown decidable by simply inspecting Karp and Miller trees: the presence of the infinity value ∞ (also denoted by ω) is equivalent to unboundedness. So, unboundedness is equivalent to the existence of a witness run of the form (q 0 , x 0 ) * -→ (q, x 1 ) π -→ (q, x 2 ) such that x 1 ≺ x 2 , assuming that the initial configuration is (q 0 , x 0 ) (≺ is the standard strict ordering on tuples of natural numbers). In [START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF], it is shown that if there is such a run, there is one of length at most doubly exponential. This leads to the ExpSpace-completeness of the boundedness problem for VASS using the lower bound from [START_REF] Lipton | The reachability problem requires exponential space[END_REF] and Savitch's Theorem [START_REF] Savitch | Relationships between nondeterministic and deterministic tape complexities[END_REF]. A variant problem consists in checking whether the ith component is bounded, i.e., is there a bound B such that for every configuration reachable from (q 0 , x 0 ), its ith component is bounded by B? Again, inspecting Karp and Miller trees reveals the answer: the presence of the infinity value ∞ at the ith position of some extended configuration is equivalent to i-unboundedness. Surprisingly, the literature often mentions this alternative problem, see e.g. [START_REF]Lectures on Petri Nets I: Basic Models[END_REF], but never specifies its complexity: ExpSpace-hardness can be obtained from [START_REF] Lipton | The reachability problem requires exponential space[END_REF] but as far as we know, no elementary complexity upper bound has been shown. A natural adaptation from boundedness is certainly that i-unboundedness could be witnessed by the existence of a run of the form (q 0 , x 0 ) * -→ (q, x 1 ) π -→ (q, x 2 ) such that x 1 ≺ x 2 with x 1 (i) < x 2 (i). By inspecting the proof in [START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF], one can show that if there is such a run, then there is one of length at most doubly exponential. However, although existence of such a run is a sufficient condition for i-unboundedness (simply iterate π infinitely), this is not a necessary condition. It might be explained by the fact that, if a VASS is unbounded, then there is a witness infinite run with an infinite number of distinct configurations. By contrast, it may happen that a VASS is i-unbounded but no infinite run has an infinite amount of distinct values at the ith position of the configurations of the run.

A generalization. In the paper, we present a generalization of place unboundedness by checking whether a set of components is simultaneously unbounded, possibly with some ordering (see Section 3.2). This amounts to specifying in the Karp and Miller trees, the ordering with which the value ∞ appears in the different components. Such a generalization is particularly useful since we show that many problems such as reversal-boundedness [START_REF] Ibarra | Reversal-bounded multicounter machines and their decision problems[END_REF], strong reversal-boundedness [START_REF] Ibarra | Counter machines and verification problems[END_REF], reversal-boundedness from [START_REF] Finkel | Reversal-bounded counter machines revisited[END_REF] can be naturally reduced to simultaneous unboundedness. Moreover, this allows to extend the class of properties for which ExpSpace can be obtained, see e.g. standard results in [START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF][START_REF] Habermehl | On the complexity of the linear-time mu-calculus for Petri nets[END_REF][START_REF] Faouzi Atig | On Yen's path logic for Petri nets[END_REF].

Our contribution. In the paper we show the following results.

1. Detecting whether a VASS is reversal-bounded in the sense of [START_REF] Ibarra | Reversal-bounded multicounter machines and their decision problems[END_REF] or in the sense of [START_REF] Finkel | Reversal-bounded counter machines revisited[END_REF] is ExpSpace-complete by refining the decidability results from [START_REF] Finkel | Reversal-bounded counter machines revisited[END_REF] (see Theorem 5.2). 2. To do so, we introduce the generalized unboundedness problem in which many problems can be captured such as the reversal-boundedness detection problems, the boundedness problem, the place boundedness problem, termination, strong promptness detection problem, regularity detection and many other decision problems on VASS. We show that this problem can be solved in exponential space by adapting [START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF] even though it does not fall into the class of increasing path formulae recently introduced in [START_REF] Faouzi Atig | On Yen's path logic for Petri nets[END_REF][START_REF] Atig | On Yen's path logic for Petri nets[END_REF] (see Theorem 4.6). 3. Consequently, we show that regularity and strong promptness detection problems for VASS are in ExpSpace. The ExpSpace upper bound has been left open in [START_REF] Faouzi Atig | On Yen's path logic for Petri nets[END_REF]. Even though most of our results essentially rest on the fact that the place boundedness problem can be solved in ExpSpace, our generalization is introduced to obtain new complexity upper bound for other related problems. On our way to this complexity result, we provide a witness run characterization for place unboundedness that can still be expressed in Yen's path logic [START_REF] Yen | A unified approach for deciding the existence of certain net paths[END_REF][START_REF] Faouzi Atig | On Yen's path logic for Petri nets[END_REF] but with a path formula of exponential size in the dimension. 4. As a by-product of our analysis and following a parameterized analysis initiated in [START_REF] Rosier | A multiparameter analysis of the boundedness problem for vector addition systems[END_REF][START_REF] Howell | An analysis of the nonemptiness problem for classes of reversal-bounded multicounter machines[END_REF], for all the above-mentionned problems, we show that fixing the dimension of the VASS allows to get a PSpace upper bound.

The complexity of our witness run characterization for selective unboundedness partly explains why it has been ignored so far. It is clear that whenever the place boundedness problem is decidable, the boundedness problem is decidable too. However, the converse does not always hold true: for instance the boundedness problem for transfer nets is decidable unlike the place boundedness problem [START_REF] Dufourd | Boundedness of reset P/T nets[END_REF]. Place boundedness problem can be therefore intrinsically more difficult than the boundedness problem: there is always a simple way to be unbounded but if one looks for i-unboundedness, it might be much more difficult to detect it, if possible at all. The paper has also original contributions as far as proof techniques are concerned. First, simultaneous unboundedness has a simple characterization in terms of Karp and Miller trees, but we provide in the paper a witness run characterization, which allows us to provide a complexity analysis along the lines of [START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF]. We also provide a witness pseudo-run characterization in which we sometimes admit negative component values. This turns out to be the right approach when a characterization from coverability graphs [START_REF] Karp | Parallel program schemata[END_REF][START_REF] Valk | Petri nets and regular languages[END_REF] already exists. Apart from this unorthodox adaptation of [START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF], in the counterpart of Rackoff's proof about the induction on the dimension, we provide an induction on the dimension and on the length of the properties to be verified (see Lemma 4.4). The preliminary work [START_REF] Demri | On Selective Unboundedness of VASS[END_REF] has already been used in [START_REF] Praveen | Small Vertex Cover Makes Petri Net Coverability and Boundedness Easier[END_REF] to obtain new complexity results. This is a genuine breakthrough comparable to [START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF][START_REF] Rosier | A multiparameter analysis of the boundedness problem for vector addition systems[END_REF][START_REF] Habermehl | On the complexity of the linear-time mu-calculus for Petri nets[END_REF][START_REF] Faouzi Atig | On Yen's path logic for Petri nets[END_REF]. We believe this approach is still subject to extensions. Finally, a recent work [START_REF] Blockelet | Model-checking coverability graphs of vector addition systems[END_REF] has also established similar ExpSpace upper 3 bounds for checking properties on VASS by introducing a temporal logic on coverability graphs.

By the way, we pay a special attention to explain most of the technical developements, at the cost of repeating sometimes standard arguments (see e.g. the nondeterministic procedure in Section 4.1). We feel that this will considerably help the reader for understanding the chain of technical results.

Plan of the paper. In Section 2, we present the vector addition systems with states as well as their decision problems including the simultaneous unboundedness problem and reversalboundedness detection problem. Section 3 introduces the class of generalized unboundedness properties as well as the generalized unboundedness problem. We show how regularity detection, strong promptness and weak reversal-boundedness detection can be reduced to generalized unboundedness problem. In Section 4, we prove our main result: the generalized unboundedness problem for VASS is ExpSpace-complete. In Section 5, as a consequence of the main result, we show that the regularity detection problem and the strong promptness detection problem are in ExpSpace. Moreover, (weak) reversal-boundedness detection problem for VASS is also shown ExpSpace-complete.

Preliminaries

In this section, we recall the main definitions for vector addition systems with states (VASS), without states (VAS) as well as the notions of reversal-boundedness introduced in [START_REF] Ibarra | Reversal-bounded multicounter machines and their decision problems[END_REF][START_REF] Finkel | Reversal-bounded counter machines revisited[END_REF]. We also present the simultaneous unboundedness problem, which generalizes the place unboundedness problem for Petri nets. First, we write N [resp. Z] for the set of natural numbers [resp. integers] and [m, m ′ ] with m, m ′ ∈ Z to denote the set { j ∈ Z : m ≤ j ≤ m ′ }. Given a dimension n ≥ 1 and a ∈ Z, we write a ∈ Z n to denote the vector with all values equal to a. For x ∈ Z n , we write x(1), . . . , x(n) for the entries of x. For x, y ∈ Z n , x y def ⇔ for every i ∈ [1, n], we have x(i) ≤ y(i). We also write x ≺ y when x y and x y.

Simultaneous unboundedness problem for VASS

VASS. A vector addition system with states [START_REF] Hopcroft | On the reachability problem for 5-dimensional vector addition systems[END_REF] (VASS for short) is a finite-state automaton with transitions labelled by tuples of integers viewed as update functions. A VASS is a structure V = (Q, n, δ) such that Q is a nonempty finite set of control states, n ≥ 1 is the dimension, and δ is the transition relation defined as a finite set of triples in Q × Z n × Q. Elements t = (q, b, q ′ ) ∈ δ are called transitions and are often represented by q b -→ q ′ . Moreover, a VASS has no initial control state and no final control state but in the sequel we introduce such control states on demand. Figure 1 presents a VASS of dimension 4 with two control states. VASS with a unique control state are called vector addition systems (VAS for short) [START_REF] Karp | Parallel program schemata[END_REF]. In the sequel, a VAS T is represented by a finite nonempty subset of Z n , encoding naturally the transitions. VASS and VAS are equivalent to Petri nets, see e.g. [START_REF] Reutenauer | The Mathematics of Petri nets[END_REF]. In this paper, the decision problems are defined with the VASS model and the decision procedures are designed for VAS, assuming that we know how the problems can be reduced, see e.g. [START_REF] Hopcroft | On the reachability problem for 5-dimensional vector addition systems[END_REF]. Indeed, we prefer to define problems with the help of the VASS model since when infinite-state transition systems arise in the modeling of computational processes, there is often a natural factoring of each system state into a control component and a memory component, where the set of control states is typically finite. In this paper, we use the reduction from VASS to VAS defined in [START_REF] Hopcroft | On the reachability problem for 5-dimensional vector addition systems[END_REF] that allows to simulate a VASS of dimension n by

q 0 q 1               -1 0 0 0                             0 0 0 0                             0 1 -1 1                             0 -1 1 0              
Figure 1: A simple VASS with two control states a VAS of dimension n + 3, independently of its number of control states (formal definition is recalled in the proof of Lemma 2.5). Even though a simpler reduction exists that increments the dimension by the cardinal of the set of control states, the reduction from [START_REF] Hopcroft | On the reachability problem for 5-dimensional vector addition systems[END_REF] is exactly what we need, since sometimes, at some intermediate stage, we may increase exponentially the number of control states.

Runs.

A configuration of V is defined as a pair (q, x) ∈ Q × N n (for VAS, we simply omit the control state). An initialized VASS is a pair made of a VASS and a configuration. Given two configurations (q, x), (q ′ , x ′ ) and a transition t = q b -→ q ′ , we write (q, x) t -→ (q ′ , x ′ ) whenever x ′ = x + b. We also write (q, x) -→ (q ′ , x ′ ) when there is no need to specify the transition t. The operational semantics of VASS updates configurations; runs of such systems are essentially sequences of configurations. Every VASS induces a (possibly infinite) directed graph of configurations. Indeed, all the interesting problems on VASS can be formulated on its transition system (Q × N n , -→). Given a VASS V = (Q, n, δ), a run ρ is a nonempty (possibly infinite) sequence ρ = (q 0 , x 0 ), . . . , (q k , x k ), . . . of configurations such that (q i , x i ) -→ (q i+1 , x i+1 ) for all i. We set Reach(V, (q 0 , x 0 )) def = {(q k , x k ) : there is a finite run (q 0 , x 0 ), . . . , (q k , x k )}. Considering the VASS in Figure 1, one can show that

{ a b d ∈ N 3 : d ≤ a × b} = { a b d ∈ N 3 : ∃ a ′ b ′ c ′ ∈ N 3 , (q 0 , a ′ b ′ c ′ d ) ∈ Reach(V, (q 0 , a b 0 0 ))}
A run can be alternatively represented by an initial configuration and a sequence of transitions, assuming that no negative component values is obtained by applying the sequence of transitions. A path π is a finite sequence of transitions whose successive control states respect δ (actually this notion is mainly used for VAS without control states). A pseudo-configuration is defined as an element of Q × Z n . When π = t 1 • • • t k is a path, the pseudo-run ρ = (π, (q, x)) is defined as the sequence of pseudo-configurations (q 0 , x 0 ) • • • (q k , x k ) such that (q 0 , x 0 ) = (q, x), and for every

i ∈ [1, k], there is t = q i b - → q i+1 such that x i = x i-1 + b.
So, we deliberately distinguish the notion of path (sequence of transitions) from the notion of pseudo-run (sequence of elements in Q × Z n respecting the transition from V). The pseudo-run ρ is induced by the path π and of length k + 1; the path π is of length k. (q 0 , x 0 ) is called the initial pseudo-configuration and (q k , x k ) is called the final pseudo-configuration in the pseudo-run ρ. We also use the notation (q, x) t -→ (q ′ , x ′ ) with pseudo-configurations. Given a VASS V [resp. a pseudo-configuration (q, x), etc.] of dimension n, we write V(I) [resp. (q, x)(I), etc.] to denote the restriction of V [resp. (q, x), etc.] to the components in I ⊆ [1, n].

Sizes. Let us start by defining the size of some VAS T of dimension n ≥ 1. Given x ∈ Z n , we write maxneg( x) [resp. max( x)] to denote the value max({max(0, -

x(i)) : i ∈ [1, n]}). [resp. max({ x(i) : i ∈ [1, n]})]. By extension, we write maxneg(V) to denote max{maxneg( b) : q b - → q ′ ∈ δ}. Furthermore, we write scale(V) to denote the value max({| b(i)| : q b - → q ′ ∈ δ, i ∈ [1, n]}).
For instance, maxneg((-2, 3)) = 2 and scale({(-2, 3)}) = 3. The size of T , written |T |, is defined by the value below: n × card(T ) × (1 + ⌈log 2 (1 + scale(T ))⌉). Given a finite subset X of Z n , we also write |X| to denote n × card(X) × (1 + ⌈log 2 (1 + scale(X))⌉). We write | x| to denote the size of x ∈ Z n defined as the size of the singleton set { x}. Given a VASS V = (Q, n, δ), we write |V| to denote its size defined by

card(Q) + n × card(δ) × (2 × card(Q) + (1 + ⌈log 2 (1 + scale(V))⌉))
Observe that 1 + ⌈log 2 (1 + a)⌉ is a sufficient number of bits to encode integers in [-a, a] for a > 0. Moreover scale(V) ≥ maxneg(V), scale(V) ≤ 2 |V| and |V| ≥ 2. In a few words, we adopt reasonably succint encodings for all the objects involved in decision problems, in particular the integers are encoded with a binary representation.

Standard problems. The reachability problem for VASS is decidable [START_REF] Mayr | An algorithm for the general Petri net reachability problem[END_REF][START_REF] Kosaraju | Decidability of reachability in vector addition systems[END_REF][START_REF] Reutenauer | The Mathematics of Petri nets[END_REF][START_REF] Lambert | A structure to decide reachability in Petri nets[END_REF][START_REF] Leroux | Vector Addition System Reachability Problem (A Short Self-Contained Proof)[END_REF]. Nevertheless, the exact complexity of the reachability problem is open: we know it is ExpSpacehard [START_REF] Lipton | The reachability problem requires exponential space[END_REF][START_REF] Cardoza | Exponential space complete problems for Petri nets and Commutative Semigroups: Preliminary report[END_REF][START_REF] Esparza | Decidability and complexity of Petri net problems -an introduction[END_REF] and no primitive recursive upper bound exists. By contrast, the covering problem and boundedness problems seem easier since they are ExpSpace-complete [START_REF] Lipton | The reachability problem requires exponential space[END_REF][START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF]. Decidability is established in [START_REF] Karp | Parallel program schemata[END_REF] but with a worst-case nonprimitive recursive bound. The ExpSpace lower bound is due to Lipton and the upper bound to Rackoff. In order to be complete, one should make precise how vectors in Z n are encoded. The upper bound holds true with a binary representation of integers whereas the lower bound holds true already with the values -1, 0 and 1. Consequently, the problem is ExpSpace-hard even with an unary encoding. The proof technique in [START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF] has been also used to establish that LTL model-checking problem for VASS is ExpSpace-complete [START_REF] Habermehl | On the complexity of the linear-time mu-calculus for Petri nets[END_REF]. By adding the possibility to reset counters in the system (providing the class of reset VASS), the boundedness and the reachability problems becomes undecidable, see e.g. [START_REF] Dufourd | Reset nets between decidability and undecidability[END_REF]. By contrast, the covering problem for VASS with resets is decidable by using the theory of well-structured transition systems, see e.g. [START_REF] Finkel | Well-structured transitions systems everywhere![END_REF].

Simultaneous unboundedness problem. Let (V, (q 0 , x 0 )) be an initialized VASS of dimension n and X ⊆ [1, n]. We say that (V, (q 0 , x 0 )) is simultaneously X-unbounded if for any B ≥ 0, there is a run from (q 0 , x 0 ) to some (q, y) such that for every i ∈ X, we have y(i) ≥ B. When X = { j}, we say that (V, (q 0 , x 0 )) is j-unbounded. It is clear that (V, (q 0 , x 0 )) is bounded (i.e., the set Reach(V, (q 0 , x 0 )) is finite) iff for all j ∈ [1, n], (V, (q 0 , x 0 )) is not j-unbounded. So, here is the simultaneous unboundedness problem.

Simultaneous unboundedness problem:

Input: Initialized VASS (V, (q 0 , x 0 )) of dimension n and X ⊆ [1, n].
Question: is (V, (q 0 , x 0 )) simultaneously X-unbounded? Theorem 2.1. [START_REF] Karp | Parallel program schemata[END_REF] Simultaneous unboundedness problem is decidable. This follows from [START_REF] Karp | Parallel program schemata[END_REF][START_REF] Valk | Petri nets and regular languages[END_REF]: (V, (q 0 , x 0 )) is simultaneously X-unbounded iff the coverability graph CG(V, (q 0 , x 0 )) (see e.g., [START_REF] Karp | Parallel program schemata[END_REF][START_REF] Valk | Petri nets and regular languages[END_REF]) contains an extended configuration (q, y) such that y(X) = ∞ (for α ∈ Z∪{∞}, we write α to denote any vector of dimension n ≥ 1 whose component values are α). More properties about coverability graphs are recalled below but just note that in the sequel, we show that the simultaneous unboundedness problem is ExpSpace-complete too.

Before going any further, let us recall some properties about coverability graphs [START_REF] Karp | Parallel program schemata[END_REF][START_REF] Valk | Petri nets and regular languages[END_REF], see complete definitions in [START_REF] Reutenauer | The Mathematics of Petri nets[END_REF]. Not only this will be useful to prove Lemma 3.1 but we will refer to it quite often.

A coverability graph approximates the set of reachable configurations from a given configuration and it is a finite structure that can be effectively computed. Let us start by preliminary definitions. Let us consider the structure (N ∪ {∞}, ≤) such that for all k, k

′ ∈ N ∪ {∞}, k ≤ k ′ def ⇔ either k, k ′ ∈ N and k ≤ k ′ or k ′ = ∞. We write k < k ′ whenever k ≤ k ′ and k k ′ .
The ordering ≤ can be naturally extended to tuples in (N ∪ {∞}) n by defining it component-wise: for all

x, x ′ ∈ (N ∪ {∞}) n , x x ′ def ⇔ for i ∈ [1, n], either x(i), x ′ (i) ∈ N and x(i) ≤ x ′ (i) or x ′ (i) = ∞. We also write x ≺ x ′ when x x ′ and x x ′ . Given x, x ′ ∈ (N ∪ {∞}) n such that x < x ′ , we write acc( x, x ′ ) to denote the element of (N ∪ {∞}) n such that for i ∈ [1, n], if x(i) = x ′ (i) then acc( x, x ′ )(i) def = x ′ (i), otherwise acc( x, x ′ )(i) def = ∞.
Let us conclude this paragraph by a last definition. For all x ∈ (N ∪ {∞}) n and for every t ∈ Z n , x + t is defined as an element of (Z ∪ {∞}) n such that for every

i ∈ [1, n], if x(i) ∈ N then ( x + t)(i) def = x(i) + t(i), otherwise ( x + t)(i) def = ∞.
Given a VASS V = (Q, n, δ) and a configuration (q 0 , x 0 ), we recall that the coverability graph CG(V, (q 0 , x 0 )) is a structure (V, E) such that V ⊆ Q × (N ∪ {∞}) n and E ⊆ V × δ × V, see e.g. [START_REF] Karp | Parallel program schemata[END_REF] or in [START_REF] Finkel | Reduction and covering of infinite reachability trees[END_REF] a generalization to well-structured transition systems. Here are essential properties of CG(V, (q 0 , x 0 )):

(CG1) CG(V, (q 0 , x 0 )) is a finite structure (consequence of König's Lemma and Dickson's Lemma).

(CG2) For any configuration (q, y) reachable from (q 0 , x 0 ) in V, there is (q, y ′ ) in CG(V, (q 0 , x 0 )) such that y y ′ . Otherwise said, any reachable configuration can be covered by an element of CG(V, (q 0 , x 0 )). Moreover, if (q 0 , x 0 ) π -→ (q, y) is a run of V, then (q 0 , x 0 ) π -→ (q, y ′ ) in CG(V, (q 0 , x 0 )).

(CG3) For every extended configuration (q, y ′ ) in CG(V, (q 0 , x 0 )) and for every bound B ∈ N, there is a run (q 0 , x 0 )

* - → (q, y) in V such that for i ∈ [1, n], if y ′ (i) = ∞ then y(i) ≥ B otherwise y(i) = y ′ (i).
Unfortunately, even though CG(T , x 0 ) is finite, in the worst-case its number of nodes can be nonprimitive recursive [START_REF] Valk | Petri nets and regular languages[END_REF][START_REF] Jantzen | Complexity of Place/Transition Nets[END_REF]. Figure 2 presents a VASS of dimension 1 (on the left) and the corresponding coverability graph for the initial configuration (q 0 , 0).

Standard reversal-boundedness and its variant

A reversal for a counter occurs in a run when there is an alternation from nonincreasing mode to nondecreasing mode and vice-versa. For instance, in the sequence below, there are three reversals identified by an upper line: 00112233344443332223334444555554

q 0 q 1 q 2 (t 1 ) +1 0 (t 2 ) (t 3 ) -1 0 (t 4 ) q 0 , 0 q 1 , 1 q 2 , 0 q 0 , ∞ q 1 , 0 q 1 , ∞ q 2 , ∞ t 1 t 3 t 2 t 4 t 1 t 2 t 2 t 3 t 4
Figure 2: A VASS and its coverability graph from the initial configuration (q 0 , 0) Similarly, the sequence 00111222223333334444 has no reversal. Figure 3 presents schematically the behavior of a counter with 5 reversals. A VASS is reversal-bounded whenever there is r ≥ 0 such that for any run, every counter makes no more than r reversals. This class of VASS has been introduced and studied in [START_REF] Ibarra | Reversal-bounded multicounter machines and their decision problems[END_REF], partly inspired by similar restrictions on multistack automata [START_REF] Baker | Reversal-bounded multipushdown machines[END_REF]. A formal definition will follow, but before going any further, it is worth pointing out a few peculiarities of this subclass. Indeed, reversal-bounded VASS are augmented with an initial configuration so that existence of the bound r is relative to the initial configuration. Secondly, this class is not defined from the class of VASS by imposing syntactic restrictions but rather semantical ones. In spite of the fact that the problem of deciding whether a counter automaton (VASS with zero-tests) is reversal-bounded is undecidable [START_REF] Ibarra | Reversal-bounded multicounter machines and their decision problems[END_REF], we explain later why reversalbounded counter automata have numerous fundamental properties. Moreover, a breakthrough has been achieved in [START_REF] Finkel | Reversal-bounded counter machines revisited[END_REF] by establishing that checking whether a VASS is reversal-bounded is decidable. The decidability proof in [START_REF] Finkel | Reversal-bounded counter machines revisited[END_REF] provides a decision procedure that requires nonprimi-tive recursive time in the worst case since Karp and Miller trees need to be built [START_REF] Karp | Parallel program schemata[END_REF][START_REF] Valk | Petri nets and regular languages[END_REF]. In the sequel, we show that this can be checked with exponential space only, and this is optimal as far as worst-case complexity is concerned. Let V = (Q, n, δ) be a VASS. Let us define the auxiliary VASS V rb = (Q ′ , 2n, δ ′ ) such that essentially, the n new components in V rb count the number of reversals for each component from V. We set Q ′ = Q × {DEC, INC} n and, for every v ∈ {DEC, INC} n and every i ∈ [1, n], v(i) encodes whether component i is in a decreasing mode or in an increasing mode. Moreover,

(q, mode) b ′ - → (q ′ , mode ′ ) ∈ δ ′ (with b ′ ∈ Z 2n ) def ⇔ there is q b - → q ′ ∈ δ such that b ′ ([1, n]) = b and for every i ∈ [1, n],
one of the conditions below is satisfied:

• b(i) < 0, mode(i) = mode ′ (i) = DEC and b ′ (n + i) = 0, • b(i) < 0, mode(i) = INC, mode ′ (i) = DEC and b ′ (n + i) = 1, • b(i) > 0, mode(i) = mode ′ (i) = INC and b ′ (n + i) = 0, • b(i) > 0, mode(i) = DEC, mode ′ (i) = INC and b ′ (n + i) = 1, • b(i) = 0, mode(i) = mode ′ (i) and b ′ (n + i) = 0.
Initialized VASS (V, (q, x)) is reversal-bounded [START_REF] Ibarra | Reversal-bounded multicounter machines and their decision problems[END_REF] def

⇔ for every i ∈ [n + 1, 2n], { y(i) : ∃ run (q rb , x rb ) * - → (q ′ , y) in V rb } is finite with q rb = (q, INC), x rb restricted to the n first compo- nents is x and x rb restricted to the n last components is 0. When r ≥ max({ y(i) : ∃ run (q rb , x rb ) * - → (q ′ , y) in V rb } : i ∈ [n + 1, 2n]), (V, (q, x)) is said to be r-reversal-bounded. For a fixed i ∈ [1, n], when { y(n + i) : ∃ run (q rb , x rb ) * - → (q ′ , y) in V rb }
is finite, we say that (V, (q, x)) is reversalbounded with respect to i. Reversal-boundedness for counter automata, and a fortiori for VASS, is very appealing because reachability sets are semilinear as recalled below.

Theorem 2.2. [START_REF] Ibarra | Reversal-bounded multicounter machines and their decision problems[END_REF] Let (V, (q, x)) be an r-reversal-bounded VASS. For each control state q ′ , the set { y ∈ N n : ∃ run (q, x) * -→ (q ′ , y)} is effectively semilinear. This means that one can compute effectively a Presburger formula that characterizes precisely the reachable configurations whose control state is q ′ . So, detecting reversal-boundedness for VASS, which can be easily reformulated as an unboundedness problem with the above reduction, is worth the effort since semilinearity follows and then decision procedures for Presburger arithmetic can be used. By a simple observation, boundedness and reversal-boundedness are related as follows.

Lemma 2.3. (V, (q, x)) is reversal-bounded with respect to i iff (V rb , (q rb , x rb )) is not (n + i)- unbounded.
An interesting extension of reversal-boundedness is introduced in [START_REF] Finkel | Reversal-bounded counter machines revisited[END_REF][START_REF] Sangnier | Vérification de systèmes avec compteurs et pointeurs[END_REF] for which we only count the number of reversals when their values occur for a counter value above a given bound B. For instance, finiteness of the reachability set implies reversal-boundedness in the sense of [START_REF] Finkel | Reversal-bounded counter machines revisited[END_REF][START_REF] Sangnier | Vérification de systèmes avec compteurs et pointeurs[END_REF], which we call weak reversal-boundedness.

Let V = (Q, n, δ) be a VASS and a bound B ∈ N. Instead of defining a counter automaton V rb as done to characterize (standard) reversal-boundedness, we define directly an infinite directed graph that corresponds to a variant of the transition system of V rb : still, there are n new counters that record the number of reversals but only if their values occur above a bound [1, n]) + b, and for every i ∈ [1, n], one of the conditions below is satisfied:

B. That is why, the infinite directed graph T S B = (Q × {DEC, INC} n × N 2n , - → B ) is defined as follows: (q, mode, x) - → B (q ′ , mode ′ , x ′ ) def ⇔ there is a transition q b - → q ′ ∈ δ such that x ′ ([1, n]) = x(
• b(i) < 0, mode(i) = mode ′ (i) = DEC and x ′ (n + i) -x(n + i) = 0 • b(i) < 0, mode(i) = INC, mode ′ (i) = DEC, x(i) ≤ B and x ′ (n + i) -x(n + i) = 0, • b(i) < 0, mode(i) = INC, mode ′ (i) = DEC, x(i) > B and x ′ (n + i) -x(n + i) = 1, • b(i) > 0, mode(i) = mode ′ (i) = INC and x ′ (n + i) -x(n + i) = 0, • b(i) > 0, mode(i) = DEC, mode ′ (i) = INC, x(i) > B and x ′ (n + i) -x(n + i) = 1, • b(i) > 0, mode(i) = DEC, mode ′ (i) = INC, x(i) ≤ B and x ′ (n + i) -x(n + i) = 0, • b(i) = 0, mode(i) = mode ′ (i) and x ′ (n + i) -x(n + i) = 0. Given B ≥ 0 and r ≥ 0, the initialized VASS (V, (q, x)) is r-reversal-B-bounded def ⇔ for every i ∈ [n + 1, 2n], { y(i) : (q rb , x rb ) * - → B (q ′ , y) in T S B } is finite and r ≥ max({ y(i) : (q rb , x rb ) * - → B (q ′ , y) in T S B } : i ∈ [n + 1, 2n]). Initialized VASS (V, (q, x)) is weakly reversal-bounded [20] def ⇔ there is some B ≥ 0 such that for every i ∈ [n + 1, 2n], { y(i) : (q rb , x rb ) * - → B (q ′ , y) in T S B } is finite. Observe that whenever (V, (q, x)) is r-reversal-bounded, (V, (q, x)) is r-reversal-0- bounded.
Reversal-boundedness for counter automata, and a fortiori for VASS, is again very appealing because reachability sets are semilinear as stated below.

Theorem 2.4. [START_REF] Ibarra | Reversal-bounded multicounter machines and their decision problems[END_REF][START_REF] Finkel | Reversal-bounded counter machines revisited[END_REF] Let (V, (q, x)) be an initialized VASS that is (weakly) r-reversal-Bbounded for some r, B ≥ 0. For each control state q ′ , the set { y ∈ N n : run (q, x) * -→ (q ′ , y)} is effectively semilinear. This means that one can compute effectively a Presburger formula that characterizes precisely the reachable configurations whose control state is q ′ . The original proof for reversal-boundedness can be found in [START_REF] Ibarra | Reversal-bounded multicounter machines and their decision problems[END_REF] and its extension for weak reversal-boundedness is presented in [START_REF] Finkel | Reversal-bounded counter machines revisited[END_REF]; whenever a counter value is below B, this information is encoded in the control state which provides a reduction to (standard) reversal-boundedness.

Reversal-boundedness detection problem

Input: Initialized VASS (V, (q, x)) of dimension n and i ∈ [1, n].

Question: Is (V, (q, x)) reversal-bounded with respect to the component i?

We also consider the variant with weak reversal-boundedness.

Let us conclude this section by Lemma 2.5 below. The proof is essentially based on [26, Lemma 2.1] and on the definition of the initialized VASS (V rb , (q rb , x rb )). The key properties are that the dimension increases only linearly and the scale "only" exponentially in the dimension. Lemma 2.5. Given a VASS V = (Q, n, δ) and a configuration (q, x), one can effectively build in polynomial space an initialized VAS (T , x ′ ) of dimension 2n

+ 3 such that (V, (q, x)) is reversal-bounded with respect to i iff (T , x ′ ) is not (n + i)-unbounded. Moreover, scale(T ) = max((card(Q) × 2 n + 1) 2 , scale(V)). Proof. (Lemma 2.5) Let V = (Q, n, δ) be a VASS and (q, x) ∈ Q × N n . Suppose that Q has m ≥ 1 control states with Q = {q 1 , . . . , q m }. Let us recall the construction of an equivalent initialized VAS of dimension n + 3 from [26, Lemma 2.1], that we write (((Q, n, δ), (q, x))) HP = (T , x ′ ). We pose a i def = i and b i def = (m + 1)(m + 1 -i) for every i ∈ [1, m]. A configuration (q i , y) of V is encoded by the configuration y ′ in T such that y ′ ([1, n]) = y and y ′ ([n + 1, n + 3]) = (a i , b i , 0).
The initial configuration x ′ is computed from (q, x) by using this encoding. It remains to define the transitions in T .

• For each t = q i b - → q j ∈ δ, we consider the transition t ′ ∈ T such that t ′ ([1, n]) = b and t ′ ([n + 1, n + 3]) = (a j -b i , b j , -a i ).
• For technical reasons, for every i ∈ [1, m], we add two dummy transitions t i and t ′ i in T such that

-t i ([1, n]) = t ′ i ([1, n]) = 0, -t i ([n + 1, n + 3]) = (-a i , a m+1-i -b i , b m+1-i ), -t ′ i ([n + 1, n + 3]) = (b i , -a m+1-i , -b m+1-i + a i ). Observe that for t = q i b - → q j ∈ δ, (t ′ + t i + t ′ i )([1, n]) = b and (t ′ + t i + t ′ i )([n + 1, n + 3]) = (a j -a i , b j -b i , 0). The proof of [26, Lemma 2.1] establishes that every run (q ′ 0 , y 0 ) • • • (q ′ k , y k ) in V leads to a run ρ ′ = z 0 • • • z 3k in T such that • for every i ∈ [0, k], z 3i ([1, n]) = y i and z 3i is the standard encoding of (q ′ i , y i ). Moreover, each step (q ′ i , y i ) t - → (q ′ i+1 , y i+1 ) corresponds to the three steps z 3i t I t ′ I t -→ z 3i+3 in ρ ′ where q ′ i is the Ith control state of Q.
An analogous property holds true in the converse direction (and this is the place where the dummy transitions play a crucial role). This implies that for every i ∈ [1, n], (V, (q, x)) is iunbounded iff ((V, (q, x))) HP is i-unbounded.

Let us come back to our reduction. Let V = (Q, n, δ), (q, x) and i be an instance of the reversal-boundedness detection problem. Using Lemma 2.3 and the properties of the construction in [START_REF] Hopcroft | On the reachability problem for 5-dimensional vector addition systems[END_REF]Lemma 2.1], it is easy to show that • (V, (q, x)) is reversal-bounded with respect to i iff ((V rb , (q rb , x rb ))) HP is not (n+i)-unbounded.

• The scale of the VAS ((V rb , (q rb , x rb ))) HP is bounded by max((card(Q) ×2 n +1) 2 , scale(V))

(as well as the scale of the target initial configuration).

• ((V rb , (q rb , x rb ))) HP can be built in polynomial space.

It is worth noting that the cardinal of the set of control states of V rb is card(Q)×2 n where Q is the set of control states of V. Hence, this excludes the possibility to construct ((V rb , (q rb , x rb ))) HP in logarithmic space.

Note that by using the simple reduction from VASS to VAS that increases the dimension by the number of control states, we would increase exponentially the dimension, which would disallow us to obtain forthcoming optimal complexity bounds. Indeed, the number of control states in V rb is exponential in the number of control states in V.

In Lemma 3.6, we explain how to reduce weak reversal-boundedness detection to a generalization of (n + i)-unboundedness.

Generalized Unboundedness Properties

In this section, we essentially introduce the generalized unboundedness problem and we show how several detection problems can be naturally reduced to it.

Witness runs for simultaneous unboundedness

By [START_REF] Karp | Parallel program schemata[END_REF][START_REF] Valk | Petri nets and regular languages[END_REF], we know that (V, (q 0 , x 0 )) is i-unbounded iff the coverability graph CG(V, (q 0 , x 0 )) contains an extended configuration with ∞ on the ith component. This is a simple characterization whose main disadvantage is to induce a nonprimitive recursive decision procedure in the worst case. By contrast, unboundedness of (V, (q 0 , x 0 )) (i.e. i-unboundedness for some i ∈ [1, n]) is equivalent to the existence of witness run of the form (q 0 , x 0 ) * -→ (q 1 , x 1 ) + -→ (q 2 , x 2 ) such that x 1 ≺ x 2 and q 1 = q 2 . In [START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF], it is shown that if there is such a run, there is one of length at most doubly exponential. Given a component i ∈ [1, n], a natural adaptation to i-unboundedness is to check the existence of a run of the form (q 0 , x 0 ) * -→ (q 1 , x 1 ) π -→ (q 2 , x 2 ) such that x 1 ≺ x 2 , q 1 = q 2 and x 1 (i) < x 2 (i). By inspecting the proof in [START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF], one can show that if there is such a run, then there is one of length at most doubly exponential. However, although existence of such a run is a sufficient condition for i-unboundedness (simply iterate π infinitely), this is not necessary as shown on the VASS below:

q 0 q 1 1 0 0 0 -1 1
The second component is unbounded from (q 0 , 0) but no run (q 0 , 0) * -→ (q, x 1 ) [START_REF] Atig | On Yen's path logic for Petri nets[END_REF] and q ∈ {q 0 , q 1 } exists. Indeed, in order to increment the second component, the first component needs first to be incremented. Below, we present the coverability graph for this VASS with initial configuration (q 0 , (0, 0)) q 0 , (0, 0) q 0 , (∞, 0) q 1 , (0, 0)

π - → (q, x 2 ) with x 1 ≺ x 2 , x 1 (2) < x 2
q 1 , (∞, 0) q 1 , (∞, ∞) 1 0 0 0 0 0 -1 1 1 0 -1 1
Note that the only way to introduce ∞ in the second component is to introduce first ∞ on the first component. In general for VASS of dimension n, i-boundedness amounts to the existence of a run of the form (q 0 , x 0 )

π ′ 0 - → (q 1 , x 1 ) π 1 - → (q 1 , x 2 ) π ′ 1 - → • • • π ′ K-1 --→ (q K , x 2K-1 ) π K - → (q K , x 2K )
where x 2K (i) > x 2K-1 (i). Moreover, for all l ∈ [1, K] and for all j ∈ [1, n], whenever x 2l ( j) < x 2l-1 ( j), there is l ′ < l such that x 2l ′ ( j) > x 2l ′ -1 ( j) (this will be proved soon formally). This illustrates the idea that to be able to increment unboundedly the ith component, we may be able to increment earlier other components. Similarly, the ultimate condition for simultaneous unboundedness needs to specify the different ways to introduce the value ∞ along a given branch of the Karp and Miller coverability graphs. This is done thanks to the condition PB σ defined below and further generalized in Section 3.2. A disjointness sequence is a nonempty sequence

σ = X 1 • • • • • X K of nonempty subsets of [1, n] such that for i i ′ , X i ∩ X i ′ = ∅ (consequently K ≤ n). A run of the form (q 0 , x 0 ) π ′ 0 - → (q 1 , x 1 ) π 1 - → (q 2 , x 2 ) π ′ 1 - → • • • π ′ K-1 --→ (q 2K-1 , x 2K-1 ) π K - → (q 2K , x 2K )
satisfies the property PB σ (Place Boundedness with respect to a disjointness sequence σ) iff the conditions below hold true:

(P0) For every l ∈ [1, K], q 2l-1 = q 2l .
(STRICT) For all l ∈ [1, K] and all j ∈ X l , x 2l-1 ( j) < x 2l ( j).

(NONSTRICT) For all l ∈ [1, K] and all j ∈ ([1, n] \ X l ), x 2l ( j) < x 2l-1 ( j) implies j ∈ l ′ ∈[1,l-1] X l ′ .
Observe that when (STRICT) holds, the condition (NONSTRICT) is equivalent to: for all l ∈ [1, K] and all j

l ′ ∈[1,l-1]
X l ′ , we have x 2l-1 ( j) ≤ x 2l ( j). Consequently, for all l ∈ [1, K] and for all paths of the form (π l ) k for some k ≥ 1, the effect on the jth component may be negative

only if j ∈ l ′ ∈[1,l-1]
X l ′ . Finally, note that the conditions on X 1 • • • X K are reminiscent of chains in automata, see e.g. [START_REF] Perrin | Infinite Words: Automata, Semigroups, Logic and Games[END_REF]Chapter 5].

It is now time to provide a witness run characterization for simultaneous X-unboundedness that is a direct consequence of the properties of the coverability graphs [START_REF] Valk | Petri nets and regular languages[END_REF].

Lemma 3.1. Let (V, (q 0 , x 0 )) be an initialized VASS of dimension n and X ⊆ [1, n]. Then, (V, (q 0 , x 0 )) is simultaneously X-unbounded iff there is a run ρ starting at (q 0 , x 0 ) satisfying PB σ for some disjointness sequence

σ = X 1 • • • • • X K such that X ⊆ (X 1 ∪ • • • ∪ X K ) and X ∩ X K ∅.
Consequently, (V, (q 0 , x 0 )) is i-unbounded iff there is a run ρ starting at (q 0 , x 0 ) satisfying PB σ for some disjointness sequence σ

= X 1 • • • • • X K with i ∈ X K .
Proof. As a consequence of the properties on the coverability graphs presented in Section 2.1, given X ⊆ [1, n], (V, (q 0 , x 0 )) is simultaneously X-unbounded iff CG(V, (q 0 , x 0 )) contains some (q, y) with y(X) = ∞ [START_REF] Karp | Parallel program schemata[END_REF]. It is now time to show the statement. (←) Let us consider the run ρ

(q 0 , x 0 ) π ′ 0 - → (q 1 , x 1 ) π 1 - → (q 2 , x 2 ) π ′ 1 - → (q 3 , x 3 ) π 2 - → • • • (q 2K-1 , x 2K-1 ) π K - → (q 2K , x 2K )
of length L satisfying the property PB σ . Let B ≥ 0. We construct a run ρ ′ satisfying PB σ of the form (π ′ 0 (π 1 )

β 1 π ′ 1 (π 2 ) β 2 • • • (π K ) β K , (q 0 , x 0 )
) for some β 1 , . . . , β K ≥ 1 such that (B, . . . , B) x f (X) where (q f , x f ) is the final configuration of ρ ′ . Now let us define β K , . . . , β 1 (in this very ordering):

• β K = B.
• Now suppose that β i+1 , . . . , β K are already defined and i < K. Let us define β i by

β i def = B + (K -i)(L -1)maxneg(V) + Σ i ′ ∈[i+1,K] ((L -1)maxneg(V))β i ′ For every j ∈ [i + 1, K],
the path π j has at most (L -1) transitions and each transition may decrease a component by at most maxneg(V). The term

Σ i ′ ∈[i+1,K] ((L-1)maxneg(V))β i ′ guarantees that each component in X i is large enough to fire π j without reaching negative values. Similarly, each path π ′ j with j ∈ [i, K -1],
has at most (L -1) transitions and each transition may decrease a component by at most maxneg(V). The term (Ki)(L -1)maxneg(V) guarantees that each component in X i is large enough to fire π ′ j without reaching negative values. Finally the term B in β i guarantees that the final value of the component i is greater than B. Consequently, the expression (Ki)(L -1)maxneg(T ) is related to the paths π ′ i , . . . , π ′ K-1 whereas the expression

Σ i ′ ∈[i+1,K] ((L -1)maxneg(V))β i ′ is related to the paths π i+1 , . . . , π K . It is not difficult to show that (π ′ 0 (π 1 ) β 1 π ′ 1 (π 2 ) β 2 • • • (π K ) β K , (q 0 , x 0 )
) defines a run, it satisfies PB σ and (B, . . . , B) x f (X) where x f is the final configuration of ρ ′ . Since the above construction can be performed for any B, we conclude that (V, (q 0 , x 0 )) is simultaneously X-unbounded. (→) Now suppose that (V, (q 0 , x 0 )) is simultaneously X-unbounded. This means that CG(V, (q 0 , x 0 )) has an extended configuration (q, y) ∈ Q × (N ∪ {∞}) n such that y(X) = (∞, . . . , ∞). We can assume that y is the first extended configuration on that branch with y(X) = (∞, . . . , ∞). Let us consider the sequence below (q 0 , x 0 )

π ′ 0 - → (q 1 , y 1 ) π 1 - → (q 2 , y 2 ) π ′ 1 - → (q 3 , y 3 ) π 2 - → • • • π ′ K-1 --→ (q 2K-1 , y 2K-1 ) π K - → (q 2K , y 2K )
obtained from CG(V, (q 0 , x 0 )) such that • For every l ∈ [1, K], q 2l-1 = q 2l , and y 2K = y.

• For every l ∈ [1, K], X l ∅ with X l def = { j ∈ [1, n] : y 2l ( j) = ∞, y 2l-1 ( j) ∞} and y 2l-1 ≺ y 2l .
Let us suppose that the above sequence in CG(V, (q 0 , x 0 )) has L (extended) configurations and let us pose

σ = X 1 • • • X K . It is easy to show that σ is a disjointness sequence with X ⊆ l∈[1,K]
X l and X ∩ X K ∅. Again, we shall design a run ρ satisfying PB σ of the form

(π ′ 0 (π 1 ) β 1 π ′ 1 (π 2 ) β 2 • • • (π K ) β K , (q 0 , x 0 )
) for some β 1 , . . . , β K ≥ 1. Now let us define β K , . . . , β 1 (in this very ordering):

• β K = 1.
• Now suppose that β i+1 , . . . , β K are already defined for i < K. Let us define β i by

β i def = 1 + (K -i)(L -1)maxneg(V) + Σ i ′ ∈[i+1,K] ((L -1)maxneg(V))β i ′ . Now, it is not difficult to show that ρ = (π ′ 0 (π 1 ) β 1 π ′ 1 (π 2 ) β 2 • • • (π K ) β K , (q 0 , x 0 )
) defines a run and it satisfies PB σ .

Existence of a run satisfying PB σ can be expressed in the logical formalisms from [START_REF] Yen | A unified approach for deciding the existence of certain net paths[END_REF][START_REF] Faouzi Atig | On Yen's path logic for Petri nets[END_REF] but this requires a formula of exponential size in the dimension because an exponential number of disjointness sequences needs to be taken into account. By contrast, each disjunct has a size only polynomial in n. The path formula looks like that (in order to fit exactly the syntax from [START_REF] Yen | A unified approach for deciding the existence of certain net paths[END_REF][START_REF] Faouzi Atig | On Yen's path logic for Petri nets[END_REF] we would need a bit more work since existential quantification cannot occur in the scope of disjunction):

X 1 •••X K ,i∈X K ∃ x 1 , . . . , x 2K K l=1 ( j∈X l x 2l-1 ( j) < x 2l ( j)) ∧ ( j (X 1 ∪•••∪X l-1 ) x 2l-1 ( j) ≤ x 2l ( j))
It is worth noting that the satisfaction of PB σ does not imply x 1 x 2K . This prevents us from defining this condition with an increasing path formula [START_REF] Faouzi Atig | On Yen's path logic for Petri nets[END_REF] and therefore the ExpSpace upper bound established in [START_REF] Faouzi Atig | On Yen's path logic for Petri nets[END_REF] does not apply straightforwardly to i-unboundedness.

A helpful generalization

We introduce below a slight generalization of the properties PB σ in order to underline their essential features and to provide a future uniform treatment. Moreover, this allows us to express new properties, for instance those helpful to characterize nonregularity. The conditions (STRICT) and (NONSTRICT) specify inequality constraints between component values. We The length of P is K and its scale is equal to the maximum between 1 and the maximal absolute value of integers occurring in the interval expressions of P (if any). A run of the form (q 0 , x 0 )

π ′ 0 - → (q 1 , x 1 ) π 1 - → (q 2 , x 2 ) π ′ 1 - → (q 3 , x 3 ) • • • π ′ K-1 --→ (q 2K-1 , x 2K-1 ) π K - → (q 2K , x 2K )
satisfies the property P def ⇔ the conditions below hold true:

(P0) For every l ∈ [1, K], q 2l-1 = q 2l .
(P1) For every l ∈ [1, K] and j ∈ [1, n], we have x 2l ( j)x 2l-1 ( j) ∈ I l ( j).

(P2) For every l ∈ [1, K] and j ∈ [1, n], if x 2l ( j) -x 2l-1 ( j) < 0, then there is l ′ < l such that x 2l ′ ( j) -x 2l ′ -1 ( j) > 0.
Given a run ρ, we say that ρ, satisfies P if ρ admits a decomposition satisfying the conditions (P0)-(P2). By extension, (V, (q 0 , x 0 )) satisfies P def ⇔ there is a finite run starting at (q 0 , x 0 ) satisfying P. It is easy to see that condition (P1) [resp. (P2)] is a quantitative counterpart for condition (STRICT) [resp. (NONSTRICT)] defined in Section 3.1.

Let us now introduce below our most general problem, especially tailored to capture selective unboundedness.

Generalized Unboundedness Problem

Input: Initialized VASS (V, (q 0 , x 0 )) and generalized unboundedness property P.

Question: Does (V, (q 0 , x 0 )) satisfy P?

Let us first forget about control states: we can safely restrict ourselves to VAS without any loss of generality, as it is already the case for many properties. Lemma 3.2. There is a logarithmic-space many-one reduction from the generalized unboundedness problem for VASS to the generalized unboundedness problem for VAS. Moreover, an instance of the form ((V, (q, x)), P) is reduced to an instance of the form ((T , x ′ ), P ′ ) such that 1. if V is of dimension n, then T is of dimension n + 3, 2. P and P ′ have the same length and scale, 3. scale(T ) = max((card(Q) + 1) 2 , scale(V)) where Q is the set of control states of V.

The proof is essentially based on [26, Lemma 2.1].

Proof. Let V = (Q, n, δ), (q, x) ∈ Q × N n and P = (I 1 , . . . , I K ) be an instance of the generalized unboundedness problem for VASS. First, (T , x ′ ) = ((V, (q, x))) HP following the construction from [26, Lemma 2.1] (see also the proof of Lemma 2.5). Let us now construct P ′ .

• P ′ = (I ′ 1 , . . . , I ′ K ) with for every l ∈ [1, K], I ′ l ([1, n]) = I l and I ′ l ([n + 1, n + 3]) = [0, 0]. We recall that every run (q ′ 0 , y 0 ) • • • (q ′ k , y k ) in V leads to a run ρ ′ = z 0 • • • z 3k in the target VAS such that • for every i ∈ [0, k], z 3i ([1, n]) = y i and z 3i is the standard encoding of (q ′ i , y i ). Moreover, each step (q ′ i , y i ) t - → (q ′ i+1 , y i+1 ) corresponds to the steps z 3i t I t ′ I t -→ z 3i+3 in ρ ′ where q ′ i is the Ith control state of Q.
An analogous property holds true in the converse direction, which guarantees the correctness of the reduction. Observe that when

x 2l-1 ([n + 1, n + 3]) = x 2l ([n + 1, n + 3]) for some l ∈ [1, K] with x 2l-1 ([n + 1, n + 3]
) not of the form (a i , b i , 0), we can always come back to such a situation since the dummy transitions are fired in a very controlled way.

Generalized unboundedness properties can be expressed in more general formalisms for which decidability is known. However, in Section 4, we establish ExpSpace-completeness. Theorem 3.3. [START_REF] Faouzi Atig | On Yen's path logic for Petri nets[END_REF][START_REF] Atig | On Yen's path logic for Petri nets[END_REF] The generalized unboundedness problem is decidable.

Given (V, (q 0 , x 0 )), the existence of a run from (q 0 , x 0 ) satisfying P can be easily expressed in Yen's path logic [START_REF] Yen | A unified approach for deciding the existence of certain net paths[END_REF] and the generalized unboundedness problem is therefore decidable by [START_REF] Faouzi Atig | On Yen's path logic for Petri nets[END_REF]Theorem 3] and [START_REF] Mayr | An algorithm for the general Petri net reachability problem[END_REF][START_REF] Kosaraju | Decidability of reachability in vector addition systems[END_REF]. We cannot rely on [START_REF] Yen | A unified approach for deciding the existence of certain net paths[END_REF]Theorem 3.8] for decidability since [54, Lemma 3.7] contains a flaw, as observed in [START_REF] Faouzi Atig | On Yen's path logic for Petri nets[END_REF]. [START_REF] Faouzi Atig | On Yen's path logic for Petri nets[END_REF] precisely establishes that satisfiability in Yen's path logic is equivalent to the reachability problem for VASS. Moreover, it is worth noting that the reduction from the reachability problem to satisfiability [3, Theorem 2] uses path formulae that cannot be expressed as generalized unboundedness properties. Observe that the ExpSpace upper bound obtained for increasing path formulae in [3, Section 6] cannot be used herein since obviously generalized unboundedness properties are not necessarily increasing. That is why, we need directly to extend Rackoff's proof for boundedness [START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF].

From regularity to reversal-boundedness detection

In this section, we explain how simultaneous unboundedness problem, regularity detection, strong promptness detection and weak reversal-boundedness detection can be reduced to generalized unboundedness problem. This will allow us to obtain ExpSpace upper bound for all these problems. Lemma 3.4. Every property PB σ can be encoded as a generalized unboundedness property P σ with length K ≤ n and scale(P σ ) = 1.

Proof. From a disjointness sequence σ = X 1 • • • X K , we define the generalized unboundedness property P σ = (I 1 , . . . , I K ) as follows. For every l ∈

[1, K] and j ∈ [1, n], if j ∈ X l then I l ( j) = [1, +∞[. Otherwise, if j ∈ ([1, n] \ ( 1≤l ′ ≤l X l ′ )), then I l ( j) = [0, +∞[, otherwise I l ( j) =] -∞, +∞[.
It is easy to check that P σ and PB σ define the same set of runs.

Regularity detection.

Another example of properties that can be encoded by generalized unboundedness properties comes from the witness run characterization for nonregularity, see e.g. [START_REF] Valk | Petri nets and regular languages[END_REF][START_REF] Faouzi Atig | On Yen's path logic for Petri nets[END_REF]. Nonregularity of an initialized VASS (V, (q 0 , x 0 )) is equivalent to the existence of a run of the form (q 0 , x 0 )

π ′ 0 - → (q 1 , x 1 ) π 1 - → (q 2 , x 2 ) π ′ 1 - → (q 3 , x 3 ) π 2 - → (q 4 , x 4 ) such that 1. q 1 = q 2 , 2. q 3 = q 4 , 3. x 1 ≺ x 2 , 4. there is i ∈ [1, n] such that x 4 (i) < x 3 (i), 5. for all j ∈ [1, n] such that x 4 ( j) < x 3 ( j), we have x 1 ( j) < x 2 ( j),
see e.g. [START_REF] Valk | Petri nets and regular languages[END_REF][START_REF] Faouzi Atig | On Yen's path logic for Petri nets[END_REF] and [START_REF] Reutenauer | The Mathematics of Petri nets[END_REF]Chapter 6]. Here, the language recognized by the initialized VASS is the set of finite sequences of transitions firable from the initial configuration (no final condition). Consequently, nonregularity condition can be viewed as a disjunction of generalized unboundedness properties of the form (I i 1 , I i 2 ) where

I i 1 (i) = [1, +∞[, I i 2 (i) =] -∞, -1]
, and for j i, we have I i 1 ( j) = [0, +∞[ and I i 2 ( j) =] -∞, +∞[. Condition (5.) above will be satisfied thanks to Condition (P1) in the definition of a generalized unboundedness property.

Strong promptness detection. We show below how the strong promptness detection problem can be reduced to the simultaneous unboundedness problem, leading to an ExpSpace upper bound. The strong promptness detection problem is defined as follows [START_REF] Valk | The residue of vector sets with applications to decidability problems in Petri nets[END_REF].

Strong promptness detection problem

Input: An initialized VASS ((Q, n, δ), (q, x)) and a partition (δ I , δ E ) of δ.

Question: Is there k ∈ N such that for every run (q, x) * -→ (q ′ , x ′ ), there is no run (q ′ , x ′ ) π -→ (q ′′ , x ′′ ) using only transitions from δ I and of length more than k (π ∈ δ * I )? Let us consider below the VASS V of dimension 1 with δ I made of the two transitions in bold.

q 0 q 1 q 2 +1 0 -1 -1
(V, (q 0 , 0)) is not strongly prompt and there is no run (q 0 , 0) * -→ (q, x) π -→ (q, y) for some q ∈ {q 0 , q 1 , q 2 } such that x y, π is nonempty and contains only transitions in δ I . Lemma 3.5. There is a logarithmic-space reduction from strong promptness detection problem to the complement of simultaneous unboundedness problem.

Proof. Let (V, (q, x)) be an initialized VASS with V = (Q, n, δ) and equipped with the partition (δ I , δ E ). We construct the VASS V[δ I ] = (Q × {0, 1}, n + 1, δ ′ ) made of two copies of V. The 0-copy behaves exactly as V whereas the 1-copy contains only the transitions from δ I and has an extra counter that is incremented for each transition. The transitions from the 0-copy to the 1-copy determines nondeterministically when the length of sequences of transitions in δ I starts to be computed. V[δ I ] is defined as follows: (q, i) b -→ (q ′ , i ′ ) ∈ δ ′ iff one of the conditions below holds true:

• i = i ′ = 0, q b([1,n]) ----→ q ′ ∈ δ, b(n + 1) = 0, • i = 0, i ′ = 1, b = 0 and q = q ′ , • i = i = 1, q b([1,n]) ----→ q ′ ∈ δ I , b(n + 1) = +1.
It is easy to show that (V, (q, x)) is strongly prompt with respect to the partition (δ I , δ E ) iff (V[δ I ], (q, x ′ )) is not (n + 1)-unbounded for some x ′ with restriction to [1, n] equal to x.

Weak reversal-boundedness detection. Complement of weak reversal-boundedness involves two universal quantifications (on B and r) that can be understood as simultaneous unboundedness properties. Lemma 3.6 below is a key intermediate result in our investigation. Lemma 3.6. Given a VASS V = (Q, n, δ) and a configuration (q, x), (V, (q, x)) is not weakly reversal-bounded with respect to i iff (V rb , (q rb , x rb )) has a run satisfying PB σ for some disjoint-

ness sequence σ = X 1 • • • X K with n + i ∈ X K and i ∈ (X 1 ∪ • • • ∪ X K-1 ). Proof. (←) Let σ = X 1 • • • X K be a disjointness sequence such that n+i ∈ X K , i ∈ (X 1 ∪• • •∪X K-1 )
and (V rb , (q rb , x rb )) has a run ρ satisfying PB σ . Suppose that ρ is of the form below (q 0 , x 0 )

π ′ 0 - → (q 1 , x 1 ) π 1 - → (q 2 , x 2 ) π ′ 1 - → • • • π ′ K-1 --→ (q 2K-1 , x 2K-1 ) π K - → (q 2K , x 2K )
and of length L. By construction of (V rb , (q rb , x rb )), a reversal for i is operated on the path π K , and the projection of ρ on the n first components and to Q (for the control states from Q × {INC, DEC} n ) corresponds to a run of V. For all B, B ′ ≥ 1, we define a run ρ ′ that performs at least B ′ reversals above B for the component i, which guarantees that (V, (q, x)) is not weakly reversal-bounded with respect to i. The run ρ ′ is of the form (π ′ 0 (π 1 )

β 1 π ′ 1 (π 2 ) β 2 • • • (π K ) β K , (q, x)
). Let us define β K , . . . , β 1 ≥ 1 as follows: first β K def = B ′ , then suppose that β j+1 , . . . , β K are already defined and j < K. If i X j , then

β j def = Σ j ′ ∈[ j+1,K] ((L -1)maxneg(V))β j ′ , otherwise β j def = (B + B ′ × L × maxneg(V)) + (K -j)(L -1)maxneg(V) + Σ j ′ ∈[ j+1,K] ((L -1)maxneg(V))β j ′ .
It is not difficult to show that (π ′ 0 (π 1 )

β 1 π ′ 1 (π 2 ) β 2 • • • (π K ) β K , (q, x)
) defines a run and in the part of the run corresponding to the path (π K ) β K , at least B ′ reversals above B are observed for the ith component. Indeed, after firing π ′ 0 (π 1 )

β 1 • • • π ′ K-1
, the value for the component i is greater than B + B ′ × L × maxneg(V). Moreover, after firing π ′ 0 (π 1 )

β 1 • • • π ′ K-1 (π K ) j with j ∈ [1, B ′ ], the value for component i is greater than B + (B ′ -j) × L × maxneg(V).
(→) Suppose that (V, (q, x)) is not weakly reversal-bounded. We use [START_REF] Finkel | Reversal-bounded counter machines revisited[END_REF]Lemma 13] that characterizes weak reversal-boundedness on the coverability graph CG(V, (q, x)). First, let us recall [20, Lemma 13] formulated on the coverability graph CG(V, (q, x)): (V, (q, x)) is r-reversal-B-bounded with respect to i for some r and B iff for every elementary loop in CG(V, (q, x)) that performs a reversal on the ith component, the ith component of every extended configuration on the loop is less than B. An elementary loop is a sequence of extended configurations respecting the edge relation E of CG(V, (q, x)) such that the two extremity (extended) configurations are identical and these are the only ones identical on the loop. Since (V, (q, x)) is not weakly reversal-bounded and CG(V, (q, x)) is a finite structure (with a finite amount of elementary loops), there is an elementary loop that performs a reversal on the ith component and such that one of its extended configuration has ∞ on the ith component (otherwise we would find a B by finiteness). So, there is a sequence in CG(V, (q, x)) of the form below (q 0 , x 0 )

t 1 - → (q 1 , x 1 ) t 2 - → • • • (q k ′ , x k ′ ) t k ′ +1 --→ • • • t k - → (q k , x k ) with (q 0 , x 0 ) = (q, x), k ′ < k and (q k ′ , x k ′ ) t k ′ +1 --→ • • • t k - → (q k , x k
) is an elementary loop. Remember that the x i 's are extended configurations. Since (q k ′ , x k ′ )

t k ′ +1 --→ • • • t k - → (q k , x k
) has an extended configuration with ∞ on the ith component, this entails that x k ′ (i) is already equal to ∞. With a similar reasoning, all the extended configurations in (q k ′ , x k ′ )

t k ′ +1 --→ • • • t k - → (q k , x k
) have the same amount of components equal to ∞. Let i 1 , . . . , i K ≤ k ′ be positions on which at least one component has been newly given the value ∞ and σ = X 1 • • • X K be the disjointness sequence such that each X l is the set of components that have been newly given the value ∞ at the position i l . It is then easy to see that (t 1 • • • t k , (q rb , x rb )) is a pseudo-run weakly satisfying P σ•{n+i} with P σ•{n+i} defined from σ • {n + i} as done in the beginning of Section 3.3 for dealing with simultaneous unboundedness. Weak satisfaction is introduced in Section 3.4. From Lemma 3.7, (V rb , (q rb , x rb )) has a run ρ ′ satisfying P σ•{n+i} , which is equivalent to ρ ′ satisfying PB σ•{n+i} . Observe that σ•{n+i} is also of the appropriate form.

As a corollary, we are in a position to present a witness run characterization for weak reversalboundedness detection. (V, (q 0 , x 0 )) is not weakly reversal-bounded with respect to i iff there exist a disjointness sequence σ = X 1 • • • X K and a run (q 0 , x 0 )

π ′ 0 - → (q 1 , x 1 ) π 1 - → (q 2 , x 2 ) π ′ 1 - → • • • π ′ K - → (q 2K+1 , x 2K+1 ) π K+1 --→ (q 2K+2 , x 2K+2 ) such that 1. π K+1 contains a reversal for the ith component, 2. the subrun (q 0 , x 0 ) * - → (q 2K , x 2K ) satisfies PB σ , 3. i ∈ (X 1 ∪ • • • ∪ X K ), and 4. for every j ∈ [1, n], x 2K+2 ( j) < x 2K+1 ( j) implies j ∈ (X 1 ∪ • • • ∪ X K ).
Based on Lemmas 2.3 and 3.1, a characterization for reversal-boundedness can be also defined.

A first relaxation

Below, we relax the satisfaction of the property P by allowing negative component values in a controlled way. A pseudo-run of the form (q 0 , x 0 )

π ′ 0 - → (q 1 , x 1 ) π 1 - → (q 2 , x 2 ) π ′ 1 - → (q 3 , x 3 ) • • • π ′ K-1 --→ (q 2K-1 , x 2K-1 ) π K - → (q 2K , x 2K )
weakly satisfies P def ⇔ it satisfies (P0), (P1), (P2) (see Section 3.2) and (P3) defined below:

(P3) for every j ∈ [1, n], every pseudo-configuration x such that x( j) < 0 occurs after some x 2l for which x 2l ( j)x 2l-1 ( j) > 0.

If the run ρ satisfies P, then viewed as a pseudo-run, it also weakly satisfies P. Lemma 3.7 below states that the existence of pseudo-runs weakly satisfying P is equivalent to the existence of runs satisfying P and their length can be compared. Later, we use the witness pseudo-run characterization.

Lemma 3.7. Let ρ be a pseudo-run of length L weakly satisfying P (of length K). Then, there is a run ρ satisfying P of length at most ((L × maxneg(V)

) K × (1 + K 2 × L × maxneg(V)) + L.
Proof. Let ρ be a pseudo-run of the form below weakly satisfying the property P = (I 1 , . . . , I K ):

(q 0 , x 0 )

π ′ 0 - → (q 1 , x 1 ) π 1 - → (q 2 , x 2 ) π ′ 1 - → (q 3 , x 3 ) π 2 - → • • • π ′ K-1 --→ (q 2K-1 , x 2K-1 ) π K - → (q 2K , x 2K )
We design a run ρ satisfying P of the form

(π ′ 0 (π 1 ) β 1 π ′ 1 (π 2 ) β 2 • • • (π K ) β K , (q 0 , x 0 ))
and of the appropriate length for some β 1 , . . . , β K ≥ 1. We use the same type of construction as in the proof of Lemma 3.1. First, let us define X 1 , . . . , X K ⊆ [1, n] that records when components are strictly increasing: for every l ∈

[1, K], X l = { j ∈ [1, n] : x 2l-1 ( j) < x 2l ( j)} \ ( l ′ <l X l ′ ).
Observe that for l l ′ , we have X l ∩ X l ′ = ∅. Now let us define β K , . . . , β 1 (again, in this ordering):

• β K def = 1.
• Now suppose that β i+1 , . . . , β K are already defined and i < K. Let us define

β i . If X i = ∅, then β i def = 1. Otherwise β i def = (K -i)(L -1)maxneg(V) + Σ i ′ ∈[i+1,K] ((L -1)maxneg(V))β i ′ .
The term (K-i)(L-1)maxneg(V) is related to the paths π ′ i , . . . , π ′ K-1 whereas the term

Σ i ′ ∈[i+1,K]
((L-1)maxneg(V))β i ′ is related to the paths π i+1 , . . . , π K . Again, it is worth noting that L -1 transitions cannot decrease a component by more than (L -1)maxneg(V). Now, it is not difficult to show that (π ′ 0 (π 1 )

β 1 π ′ 1 (π 2 ) β 2 • • • (π K ) β K , (q 0 , x 0 )
) defines a run (and not only a pseudo-run) and moreover it satisfies P which is witnessed by the decomposition below:

(q 0 , x 0 ) π ′ 0 - → (q 1 , y 1 ) π 1 - → (q 2 , y 2 ) (π 1 ) β 1 -1 π ′ 1 ------→ (q 3 , y 3 ) π 2 - → • • • • • • (π K-1 ) β K-1 -1 π ′ K-1 -----------→ (q 2K-1 , y 2K-1 ) π K - → (q 2K , y 2K )
It remains to verify that this run is not too long. Let us define the sequence γ 0 , . . . , γ K-1 with

γ i = Σ i ′ ∈[K-i,K] β i ′ . So, γ 0 = β K = 1 and γ i+1 = β K-i-1 + γ i with β K-i-1 ≤ (i + 1)(L -1)maxneg(V) + ((L -1)maxneg(V))γ i So γ i+1 ≤ (K×L×maxneg(V))+(L×maxneg(V))γ i for every i ∈ [1, K-1]. If L×maxneg(V) = 1, then γ K-1 ≤ K(K × L × maxneg(V)). Otherwise γ K-1 ≤ (L × maxneg(V)) K-1 × (1 + K × L × maxneg(V))
. Finally, by using that the sum of the paths π ′ i is bounded by L, we get the desired bound.

The principle of the proof of Lemma 3.7 (and part of the proof of Lemma 3.1) is identical to the idea of the proof of the following property of the coverability graph CG(V, (q 0 , x 0 )) (see e.g., details in [START_REF] Reutenauer | The Mathematics of Petri nets[END_REF]). For every extended configuration (q, y ′ ) ∈ Q × (N ∪ {∞}) n in CG(V, (q 0 , x 0 )) and bound B ∈ N, there is a run (q 0 , x 0 )

* - → (q, y) in V such that for i ∈ [1, n], if y ′ (i) = ∞ then y(i) ≥ B otherwise y(i) = y ′ (i).
In the proof of Lemma 3.7, the paths π i 's are repeated hierarchically in order to eliminate negative values.

Additionally, if ρ is a pseudo-run of length L weakly satisfying P and L is at most doubly exponential in N = |V| + |(q 0 , x 0 )| + K + scale(P), then there is a run satisfying P and starting in x 0 that is also of length at most doubly exponential in N.

So, standard unboundedness admits also a witness pseudo-run characterization with a disjunction of n generalized unboundedness properties of length 1. But, if a pseudo-run ρ weakly satisfies P of length 1, then ρ is a run satisfying P, explaining why only the witness run characterization is relevant for standard unboundedness.

ExpSpace Upper Bound

In this section, we deal with VAS only and we consider a current VAS T of dimension n (see Lemma 3.2). Without any loss of generality, we can assume that n > 1, otherwise it is easy to show that the generalized unboundedness problem restricted to VAS of dimension 1 can be solved in polynomial space. Moreover, we assume that maxneg(T ) ≥ 1.

Motivations for approximating properties

Generalized unboundedness properties apply on runs but as it will be shown below, it would be more convenient to relax the conditions to pseudo-runs. A first step has been done in Section 3.4; we push further the idea in order to adapt Rackoff's proof. In forthcoming Section 4.2, we introduce approximations of generalized unboundedness properties and in Section 4.3, we explain how to shrink pseudo-runs satisfying such properties. To do so, we extend Rackoff's proof technique to obtain a small run property for runs witnessing (standard) unboundedness. In the rest of this section, first we recall main ingredients of Rackoff's proof (with references to forthcoming results about generalized unboundedness) and then, we motivate the main ingredients of our approximation properties.

Ingredients in Rackoff's proof. Let us briefly recall the structure of Rackoff's proof to show that the boundedness problem for VAS is in ExpSpace. Let (T , x 0 ) be an initialized VAS of dimension n. A witness run for unboundedness is of the form ρ = x 0 * -→ y + -→ y ′ with y ≺ y ′ . In [START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF], it is shown that ρ can be of length at most doubly exponential. In order to get the ExpSpace upper bound, Savitch's Theorem is used. Let us be a bit more precise. A nondeterministic algorithm guessing such a run of length less than L is defined as follows. Here is the algorithm with inputs T , x and L: If the maximal absolute value in T and x is 2 N for some N ≥ 0 and L is doubly exponential in N, then the maximal absolute value appearing in the algorithm is doubly exponential in N too. The decision procedure above guesses the small run and only requires exponential space thanks to the following additional arguments:

1. guess L ′ and L ′′ such that L ′ < L ′′ ≤ L; 2. i := 0; x c := x (current configuration); 3. While i < L ′ do (a)
1. A counter with an exponential amount of bits can count until a double-exponential value. 2. Only two configurations need to be stored thanks to nondeterminism.

Comparing or adding two natural numbers requires logarithmic space only (if their values

is doubly exponential in N, then their comparisons require only exponential space in N). 4. By Savitch's Theorem [START_REF] Savitch | Relationships between nondeterministic and deterministic tape complexities[END_REF], a nondeterministic procedure for a given problem using space f (N) ≥ log(N) can be turned into a deterministic procedure using f (N) × f (N) space. 5. Exponential functions are closed under multiplication.

Rackoff's proof to establish the small run property goes as follows. First, a technical lemma shows that if there is some i-B-bounded pseudo-run (instance of the approximation property A introduced in forthcoming Section 4.2), then there is one of length at most B |T | C for some constant C. i-B-boundedness refers to the fact that the ith first components have values in [0, B -1]. The proof essentially shows that existence of such a pseudo-run amounts to solving an inequation system and by using [START_REF] Borosh | Bounds on positive integral solutions of linear diophantine equations[END_REF], small solutions exist, whence the existence of a short i-B-bounded pseudo-run (the same technique is used in forthcoming Lemma 4.2). The idea of using small solutions of inequation system to solve problems on counter systems dates back from [START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF][START_REF] Gurari | An NP-complete number-theoretic problem[END_REF] and nowadays, this is a standard proof technique, see e.g. [START_REF] Demri | Taming Past LTL and Flat Counter Systems[END_REF]. This proof can be extended to numerous properties on pseudo-runs for which intermediate counter value differences can be expressed in Presburger arithmetic as done in [START_REF] Yen | A unified approach for deciding the existence of certain net paths[END_REF][START_REF] Faouzi Atig | On Yen's path logic for Petri nets[END_REF]. Then, a proof by induction on the dimension is performed by using this very technical lemma and the ability to repeat sequences of transitions; the proof can be extended when the first intermediate configuration is less or equal to the last configuration of the sequence (leading to the concept of increasing path formula in [START_REF] Faouzi Atig | On Yen's path logic for Petri nets[END_REF]). This condition allows to perform the induction on the dimension with a unique increasing formula. Unfortunately, generalized unboundedness properties are not increasing in the sense of [START_REF] Faouzi Atig | On Yen's path logic for Petri nets[END_REF]. Therefore, Rackoff's proof requires to be extended even though the essential ingredients remain, see the proof of Lemma 4.4. The generalization of the technical lemma corresponds to forthcoming Lemma 4.2; it is not surprising since generalized unboundedness properties are Presburger-definable properties. However, not only we need to refine the expression B |T | C in terms of various parameters (length of P, scale(P), n, scale(T )) in order to get the final ExpSpace upper bound (or the PSpace upper bound with fixed dimension), but also we have to check that the new ingredients in the definition of the forthcoming approximation properties A do not prevent us from extending [START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF]Lemma 4.4]. Finally, it is important to specify the length of small pseudoruns with respect to parameters from P.

What needs to be approximated. Lemma 3.7 states that the existence of a run satisfying the generalized unboundedness property P is equivalent to the existence of a pseudo-run weakly satisfying P = (I 1 , . . . , I K ). Therefore, in the sequel, without any loss of generality, we can focus on weak satisfaction. Suppose that the pseudo-run ρ = x 0

π ′ 0 - → x 1 π 1 - → x 2 • • • x 2K-1 π K - → x 2K
weakly satisfies P. Note that 1. every element of (I 1 , . . . , I K ) constraints ρ, as far as each path π j is concerned, 2. each pseudo-configuration x takes its values in Z n , 3. whenever a component value is negative, there is some earlier path π j that strictly increases that component (see Condition (P3)).

An approximation property A (parameterized by elements made explicit below) relaxes weak satisfaction in the following way (compare each condition C above with C ′ ). 1 ′ . Only a suffix (I l , . . . , I K ) of P is considered and a pseudo-run ρ ′ satisfying A will be therefore of the form y 2l-2

π ′ l-1 -→ y 2l-1 π l - → y 2l • • • π ′ K-1 --→ y 2K-1 π K - → y 2K . Hence l ∈ [1, K] is a parameter of A.
Such a relaxation is useful when gluing pseudo-runs weakly satisfying distinct parts of P. 2 ′ . For each configuration y and for each component i ∈ I, y(i) ∈ [0, B -1] for some I ⊆ [1, n] and B ≥ 0 unless values on the ith component can be pumped (see 3 ′ . below). Hence I and B are parameters of A too and such a relaxation will allow to provide a proof by induction on the dimension. 3 ′ . Whenever a component value is negative in ρ ′ , either there is some earlier path π j in ρ ′ that strictly increases that component or that component belongs to some set INCR of components whose values can be pumped. Hence, INCR ⊆ [1, n] is a parameter of A and such a relaxation is useful when gluing pseudo-runs and pumping values can be performed thanks to paths occurring in other pseudo-runs (materialized by the fact that the component belongs to INCR).

Approximating generalized unboundedness properties

We are now in position to define the property A[P, l, INCR, I, B]. Given a generalized unboundedness property

P of length K, l ∈ [1, K], INCR ⊆ [1, n], I ⊆ [1,
n] and B ≥ 0, a pseudorun of the form below (P1 ′ ) For every l ′ ∈ [l, K] and for every j ∈ [1, n], we have y 2l ′ ( j)y 2l ′ -1 ( j) ∈ I l ′ ( j) (only the suffix (I l , . . . , I K ) is considered).

y 2l-2 π ′ l-1 -→ y 2l-1 π l - → y 2l • • • π ′ K-1 --→ y 2K-1 π K - → y 2K
(P2 ′ ) For every l ′ ∈ [l, K] and for every j ∈ [1, n], if y 2l ′ ( j)y 2l ′ -1 ( j) < 0, then one of the conditions holds true:

• there is l ′′ ∈ [l, l ′ -1] such that y 2l ′′ ( j) -y 2l ′′ -1 ( j) > 0, • j ∈ INCR.
(P3 ′ ) For every pseudo-configuration x in ρ occurring between y 2l ′ and strictly before

y 2l ′ +2 with l ′ ≥ l -1, x(J) ∈ [0, B -1] J with J = I \ PUMP(l, l ′ ) where PUMP(l, l ′ ) = (INCR ∪ { j : ∃ l ′′ ∈ [l, l ′ ], y 2l ′′ ( j) -y 2l ′′ -1 ( j) > 0}).
Condition (P3 ′ ) reflects the intuition that only the values from components in J need to be controlled. We also write A[P, l, INCR, I, +∞] to denote the property obtained from A[P, l, INCR, I, B] by replacing [0, B -1] J by N J in the condition (P3 ′ ). Observe that a pseudo-run satisfies A[P, 1, ∅, [1, n], +∞] iff it weakly satisfies P (see Section 3.4). The property A[P, l, INCR, I, +∞] is exactly the condition we need in the proof of Lemma 4.4 below thanks to the property stated below.

Lemma 4.1. If the pseudo-run ρ = y 2l-2

π ′ l-1 -→ y 2l-1 π l - → y 2l • • • π K - → y 2K satisfies the approximation property A[P, l, INCR, I, +∞], then (π ′ l-1 (π l ) n l π ′ l (π l+1 ) n l+1 • • • (π K ) n K , y 2l-2 )
also satisfies it, for all n l , . . . , n K ≥ 1.

A similar statement does not hold for pseudo-runs satisfying A (values for components in J might become out of [0, B -1]) and for runs satisfying P (component values might become negative).

Proof. (Lemma 4.1) Let ρ ′ be the pseudo-run

y 2l-2 = z 2l-2 π ′ l-1 (π l ) n l -1 ------→ z 2l-1 π l - → z 2l • • • π ′ K-1 (π K ) n K -1 --------→ z 2K-1 π K - → z 2K
obtained from ρ by copying n i times the path π i . For every l ′ ∈ [l, K] and for every j ∈ [1, n], y 2l ′ ( j)y 2l ′ -1 ( j) = z 2l ′ ( j)z 2l ′ -1 ( j), whence ρ ′ satisfies the conditions (P1 ′ ) and (P2 ′ ). Of course, we need also to take advantage that ρ satisfies (P2 ′ ). Indeed, suppose that z 2l ′ ( j)-z 2l ′ -1 ( j) < 0. So y 2l ′ ( j)y 2l ′ -1 ( j) < 0 and by satisfaction of (P2 ′ ) by ρ, we can also conclude that either j ∈ INCR or there is

l ′′ ∈ [l, l ′ -1] such that y 2l ′′ ( j) -y 2l ′′ -1 ( j) > 0 (equivalent to z 2l ′′ ( j) -z 2l ′′ -1 ( j) > 0).
Since ρ satisfies condition (P3 ′ ), for every pseudo-configuration x in ρ occurring between y 2l ′ and strictly before y 2l ′ +2 with l ′ ≥ l -1, x(J) ∈ N J with J = I \ PUMP(l, l ′ ). Now let x in ρ ′ occurring between z 2l ′ and strictly before z 2l ′ +2 with l ′ ≥ l -1. Let J = I \ PUMP(l, l ′ ). For every l ′′ ∈ [l, l ′ ] and for every j ∈ J, the path π l ′′ has a positive effect on the component j. One can show that this entails that x(J) ∈ N J using the property (P3 ′ ) on ρ.

Property A[P, l, INCR, I, B] can be viewed as a collection of local path increasing formulae in the sense of [START_REF] Faouzi Atig | On Yen's path logic for Petri nets[END_REF].

Bounding the length of pseudo-runs

It is important to specify the length of small pseudo-runs with respect to parameters from P as done in Lemma 4.2 below.

ρ = x 2l-2 π ′ l-1 -→ x 2l-1 π l - → x 2l • • • π ′ K-1 --→ x 2K-1 π K - → x 2K
We pose d 0 = card(J 0 ) with J 0 = I \ INCR. We suppose that the pseudo-run ρ is induced by the path t 1 . . .

t k with ρ = u 0 • • • u k . Let f : [2l -2, 2K] → [0, k] be the map such that x i = u f (i) ; consequently f (2l -2) = 0 and f (2K) = k.
By the satisfaction of the condition (P3 ′ ) from A[P, l, INCR, I, B], for every pseudo-configuration u j with j ≤ f (2l-1), we have u j (J 0 ) ∈ [0, B-1] J 0 . If the length of π ′ l-1 is at least B d 0 , then there are two distinct positions j < j ′ ≤ f (2l-1) such that u j (J 0 ) = u j ′ (J 0 ) (by the pigeonhole principle) and therefore (t 1 . . .

t j t j ′ +1 . . . t k , x 2l-2 ) also satisfies A[P, l, INCR, I, B].
Observe that the values for components in [1, n] \ J 0 are allowed to be negative. By iterating this contraction process, without any loss of generality, we can assume that in ρ, we have

f (2l -1) -f (2l -2) < B d 0 and for every l ′ ∈ [l -1, K -1], f (2l ′ + 1) -f (2l ′ ) < B card(I) ≤ B n . Now, for each D ∈ [l, K] we shorten the pseudo-run x 2D-1 π D - → x 2D
. This is done by removing loops, as explained below, and by following the key steps of the proof of [START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF]Lemma 4.4]. We pose d = card(J) with

J = I \ (INCR ∪ { j : ∃ l ′ ∈ [l, D -1], x 2l ′ ( j) -x 2l ′ -1 ( j) > 0}) = I \ PUMP(l, D -1).
A simple loop with respect to J is a pair sl = ( s, π) such that s ∈ [0, B -1] J and π = t ′ 1 . . . t ′ γ is a path satisfying the conditions below:

(SL1) For every j ∈ [1, γ], s + Σ i∈[1, j] t ′ i (J) ∈ [0, B -1] J (the bound B is never exceeded). (SL2) Σ i∈[1,γ]
t ′ i (J) = 0 (the total effect on the components in J is zero),

(SL3) For j < j ′ ∈ [1, γ] with ( j, j ′ ) (1, γ), we have Σ i∈[ j, j ′ ] t ′ i (J) 0 (minimality of the path).
The length of sl is defined as the length of its path π and its effect is the value Σ i∈ [1,γ] t ′ i (remember that not all the components are in J). Consequently, let y 0 • • • y γ be a pseudo-run induced by the simple loop ( y 0 (J), t ′ 1 . . . t ′ γ ). Then, 1. y 0 (J) = y γ (J) (by (SL2)). 2. For j < j ′ ∈ [1, γ] such that ( j, j ′ ) (1, γ), we have y j (J) y j ′ (J) (by (SL3)).

It is easy to show that the length of a simple loop with respect to J is strictly below

B d with B d ≤ B d 0 ≤ B card(I) . Its effect is therefore in [-scale(T )B d , scale(T )B d ] n . Let z 1 , . . . , z α be the effects of simple loops occurring in x 2D-1 t 2D-1 --→ . . . t 2D - → x 2D as factors.
Because the effects of simple loops are bounded (see above), we have

α ≤ (1 + 2 × scale(T )B d ) n ≤ (1 + 2 × scale(T )) n B n 2 .
From the pseudo-run x 2D-1 π D -→ x 2D , we define a finite sequence of pairs made of a pseudo-run

y i 0 • • • y i K i and a tuple v i ∈ N α such that • v 0 = 0 and y 0 0 • • • y 0 K 0 = x 2D-1 • • • x 2D . • y i+1 0 • • • y i+1 K i+1
and v i+1 are computed from y i 0 • • • y i K i and v i by removing a simple loop from y i 0 • • • y i K i with effect z β and by computing v i+1 from v i by only incrementing v i (β), i.e. a simple loop is removed but we remember its effect by incrementing v i (β).

• The length of the final pseudo-run y N 0 • • • y N K N (on which no simple loop can be removed) is less than (1 + B d ) 2 . Explanations about this bound are provided below.

• { x 2D-1 (J), . . . , x 2D (J)} = { y i 0 (J), . . . , y i K i (J)} for every i ∈ [0, N]. In words, the set of tuples restricted to components in J remains even all over this process of removing simple loops. This will be useful to bring back simple loops.

Consequently, whenever v i ( j) > 0, there is a simple loop ( s, π) with effect some z j such that s ∈ { y i 0 (J), . . . , y i K i (J)}. Let us explain how to compute

y i+1 0 • • • y i+1 K i+1 and v i+1 from y i 0 • • • y i K i , v i . Suppose that y i 0 • • • y i K i is induced by the path π i = t 1 • • • t K i .
If π i has no simple loop t j • • • t j ′ as a factor such that { x 2D-1 (J), . . . , x 2D (J)} = { y i 0 (J), . . . , y i j-1 (J), y i j ′ (J) . . . , y i K i (J)}, then N = i (we stop the process). Otherwise, let ( y i j-1 (J), t j • • • t j ′ ) be a simple loop with respect to J such that { x 2D-1 (J), . . . , x 2D (J)} = { y i 0 (J), . . . , y i j-1 (J), y i j ′ (J) . . . , y i K i (J)}.

Then

y i+1 0 • • • y i+1 K i+1 is the pseudo-run (t 1 • • • t j-1 , t j ′ +1 • • • t K i , y i 0 ) and v i+1 is equal to v i except that v i+1 (β) = v i (β) + 1 with t j , . . . , t j ′ having the effect z β . Since x 2D-1 π D - → x 2D
is finite, it is clear that this process eventually stops and the above-mentioned conditions are clearly satisfied (except for the bound on the length of y N 0 • • • y N K N ). Before going any further, let us briefly explain why eventually the length of 2 . Suppose that the pseudo-run 2 pseudo-run configurations. First, observe that each block of B d + 1 consecutive pseudo-configurations contains at least one simple loop. Moreover, we wish to preserve the set { x 2D-1 (J), . . . , x 2D (J)}, so we cannot remove any simple loop. The set { x 2D-1 (J), . . . , x 2D (J)} has cardinal at most B d . Consequently, there is a block of B d + 1 successive pseudo-configurations so that all the restrictions to the components in J have already appeared earlier.

y N 0 • • • y N K N is less than (1 + B d )
y i 0 • • • y i K i has at least (1 + B d )
Let y N 0 • • • y N K N be the final sequence induced by the path t 1 • • • t K N with final loop vector v N ∈ N α .

Since the pseudo-run ρ satisfies A[P, l, INCR, I, B], we have the following properties.

1. For every j ∈ [1, n], we have (( Σ i∈ [1,α] v N (i)

z i ) + Σ i∈[1,K N ] t i )( j) ∈ I D ( j).
Depending on the value of I D ( j), this can encoded by at most 2 inequality constraints of the form Σ i∈ [1,α] a i v N (i)( j) ≥ b j . 2. For every j ∈ J, (( Σ i∈ [1,α] v N (i)

z i ) + Σ i∈[1,K N ] t i )( j) ≥ 0.
There is a bit of redundancy here for the components in J since removing simple loops does not change the projection over J of the first and last pseudo-configurations. Hence, we only need to bother about the components in ([1, n] \ J). The vector v N is a solution to the following inequality system:

(

j∈([1,n]\J) (( Σ i∈[1,α] v N (i) z i ) + Σ i∈[1,K N ] t i )( j) ∈ I D ( j))
The number of inequalities can be bounded by 2n, the number of variables is bounded by (1 + 2 × scale(T )) n B n 2 and all the absolute values of the components are bounded by (1 + B n ) 2 × scale(T ) + scale(P). It is time to apply [START_REF] Borosh | Bounds on positive integral solutions of linear diophantine equations[END_REF] in order to obtain a small solution:

Theorem 4.3. [8] Let A ∈ [-M, M] U×V and b ∈ [-M, M] U
, where U, V, M ∈ N. If there is x ∈ N V such that A x ≥ b, then there is y ∈ [0, (max{V, M}) CU ] V such that A y ≥ b, where C is some constant.

By application of Theorem 4.3 on the above system with the values below

1. V = (1 + 2 × scale(T )) n B n 2 . 2. M = (1 + B n ) 2 ×
u i 0 • • • u i L i = (t i 1 • • • t i L i , u i 0 ) such that • u 0 0 • • • u 0 L 0 = y N 0 • • • y N K N .
• The length of the sequence is exactly α + 1 (α is the number of distinct effects).

• u j+1 0 • • • u j+1 L j+1 = (t j+1 1 • • • t j+1 L j+1 , u j+1 0 ) is computed from (t j 1 • • • t j L j , u j 0 )
as follows. Let ( s j+1 , π j+1 ) be a simple loop with effect z j+1 . There exists β such that u j β (J) = s j+1 . Then,

t j+1 1 • • • t j+1 L j+1 def = t j 1 • • • t j β • (π j+1 ) X( j+1) • t j β+1 • • • t j L j and u j+1 0 • • • u j+1 L j+1 = (t j+1 1 • • • t j+1 L j+1 , u j 0 ).
It is easy to check that x 2D-1 = u α 0 . By replacing x 2D-1 This value is bounded by

π D - → x 2D by u α 0 • • • u α L α for each D ∈ [l, K],
(K + 1) × C ′ × scale(T ) p 1 (n) scale(P) p 2 (n) × B p 3 (n)
where C ′ is a constant and p 1 (•), p 2 (•) and p 3 (•) are polynomials. Since n, B ≥ 2, this value is bounded by (K + 1)(scale(T ) × scale(P) × B) p(n) for some polynomial p(•). Suppose that p(n) = Σ f i=0 a i n i (without any loss of generality, we can assume that the a i 's are non-negative and a f 0). Let f ′ ≥ 0 be such that Σ f i=0 a i ≤ 2 f ′ . Since n ≥ 2, (scale(T ) × scale(P) × B) p(n) is bounded by (scale(T ) × scale(P) × B) n f + f ′ . Hence, the length of the final pseudo-run satisfying A[P, l, INCR, I, B] and starting at x 0 is bounded by (K + 1) × (scale(T ) × scale(P) × B) n C 1 for some constant C 1 .

For every i ∈ [0, n], let us define the value g(i) that serves to bound the length of pseudo-runs satisfying A, not only the approximation: Proof.

g(i) def =        (2µ) n C 1 with µ = (1 + K) × scale(T ) × scale(P) if i = 0, 2µ(maxneg(T ) × g(i -1)) n C 1 + g(i -1) if i > 0.
Let ρ = x 2l-2 π ′ l-1 -→ x 2l-1 π l - → x 2l • • • π ′ K-1 --→ x 2K-1 π K - →
x 2K be a pseudo-run satisfying the property A[P, l, INCR, I, +∞]. We suppose that ρ is induced by the path

t 1 • • • t k with ρ = u 0 • • • u k and f : [2l -2, 2K] → [0, k] is the map such that x i = u f (i) . So f (2l -2) = 0 and f (2K) = k.
The proof is by induction on i = card(I). If i = 0, then we apply Lemma 4.2 with B = 2 and we obtain a pseudo-run satisfying the approximation property A[P, l, INCR, I, +∞] leading to the bound (µ × 2) n C 1 . Now suppose card(I) = i + 1 and J = (I \ INCR). We pose B = maxneg(T ) × g(i). We recall that T is the current VAS with n ≥ 2. We perform a case analysis depending where in ρ a value from a component in J is strictly greater than B -1 (if any).

x 2l-2 π ′ l-1 -→ x 2l-1 • • • x 2D ρ 1 = x 2D π 1 D - → u α ρ 2 t α+1 -→ satisfies A[P,D+1,INCR ′ ,(I\{i 0 }),+∞] u α+1 π 2 D - → x 2D+1 • • • x 2K-1 π K - → x 2K ρ 3
We construct a pseudo-run of the form ρ ′ 1 ρ ′ 2 ρ ′ 3 such that each ρ ′ j is obtained by shortening ρ j and the length of ρ

′ 1 [resp. ρ ′ 2 , ρ ′ 3 ] is bounded by (µ × B) n C 1 + 1 [resp. B i+1 + 1, g(i) + 1].
• If D > l -1, then we introduce P ⋆ = (I ′ l , . . . , I ′ D ) with for every l ′′ ∈ [l, D] and for every

j ∈ [1, n], -if x 2l ′′ ( j) -x 2l ′′ -1 ( j) > 0 then I ′ l ′′ ( j) = I l ′′ ( j) ∩ [1, +∞[, -otherwise I ′ l ′′ ( j) = I l ′′ ( j).
The construction of P ⋆ allows us to preserve the set of elements in [l, D] whose values can be arbitrarily increased. Moreover, above, by taking the intersection with [1, +∞[, in ρ ′ 1 , we preserve the set of components in which proper pumping is possible. By Lemma 4.2, there is a pseudo-run ρ

′ 1 = (t 1 1 • • • t 1 β 1 , x 2l-2 ) satisfying A[P ⋆ , 1, INCR, I, B] such that β 1 ≤ (µ × B) n C 1 .
Indeed, scale(P ⋆ ) ≤ scale(P) and the length of P ⋆ is obviously bounded by

K. Say ρ ′ 1 = y 2l-2 * - → y 2l-1 * - → y 2l • • • * - → y 2D-1 * - → y 2D . Suppose that ρ ′ 1 = u 1 0 • • • u 1 β 1 and f 1 : [2l -2, 2D] → [0, β 1 ] is the map such that y i = u 1 f 1 (i) with f 1 (2l -2) = 0 and f 1 (2D) = β 1 . If D = l -1, then ρ 1 = (t 1 • • • t α , x 2l-2
) with an analogous decomposition in terms of y i 's.

So, whenever D ≥ l -1, we have { j :

y 2l ′ -1 ( j) < y 2l ′ ( j), l ′ ∈ [l, D]} = { j : x 2l ′ -1 ( j) < x 2l ′ ( j), l ′ ∈ [l, D]
} -partly by construction of P ⋆ . We write Z to denote the set { j :

y 2l ′ -1 ( j) < y 2l ′ ( j), l ′ ∈ [l, D]}.
• Now, by the pigeonhole principle, there is a pseudo-run

ρ ′ 2 = (t 2 1 • • • t 2 β 2 , y 2D ) such that u ′ α = y 2D + t 2 1 + • • • + t 2 β 2 , u ′ α (J) = u α (J) and β 2 < B card(J) ≤ B i+1 . We pose u ′ α+1 = u ′ α + t α+1 . • Finally, observe that (t α+2 • • • t k , u ′ α+1 ) satisfies A[P, D + 1, INCR ′ , (I \ {i 0 }), +∞] with INCR ′ def = INCR∪Z. By the induction hypothesis, there is a pseudo-run ρ ′ 3 = (t 3 1 • • • t 3 β 3 , u ′ α+1 ) satisfying A[P, D + 1, INCR ′ , (I \ {i 0 }), +∞] and such that β 3 ≤ g(i). Because u ′ α+1 (i 0 ) ≥ maxneg(T ) × g(i), ρ ′ 3 also satisfies A[P, D + 1, INCR ′ , I, +∞]. Gluing the previous transitions, the pseudo-run (t 1 1 • • • t 1 β 1 t 2 1 • • • t 2 β 2 t α+1 t 3 1 • • • t 3 β 3 , x 2l-2 )
satisfies the approximation property A[P, l, INCR, I, +∞] and its length is bounded by (µ×B) n C 1 + B i+1 + g(i). Case 3: A value for some component in J is strictly greater than B -1 for the first time within the path π D for some D ∈ [l, K].

The pseudo-run ρ can be written as follows with

π D = π 1 D π 2 D and π 1 D ε x 2l-2 π ′ l-1 -→ x 2l-1 • • • x 2D-1 π 1 D - → u α+1 π 2 D - → x 2D • • • x 2K-1 π K - → x 2K By Lemma 4.1, the pseudo-run ρ ′ = (π ′ l-1 π l • • • π ′ D-1 (π D ) 2 π ′ D • • • π K , x 2l-2
) also satisfies the approximation property A[P, l, INCR, I, +∞] and can be written as x 2l-2

π ′ l-1 -→ x 2l-1 • • • x 2D-2 π ′ D-1 π D ----→ x 2D = z 2D-1 π D - → z 2D π ′ D+1 --→ • • • z 2K-1 π K - → z 2K .
We are therefore back to Case 2.

We are now in position to bound the length of pseudo-runs weakly satisfying the generalized unboundedness property P. Lemma 4.5. If ρ is a pseudo-run weakly satisfying P, then there is a ρ ′ starting from the same pseudo-configuration, weakly satisfying P and of length at most (µ × 2 × maxneg(T )) n (2n+1)C for some C > 1 with µ = (1 + K) × scale(T ) × scale(P).

Proof. Since T has a pseudo-run weakly satisfying P iff T has a pseudo-run satisfying A[P, 1, ∅, [1, n], +∞], by Lemma 4.4, it is sufficient to bound g(n). By Lemma 4.4, for some constant C 2 > C 1 (for instance C 2 = C 1 + 1), we have

g(i) ≤        (2µ) n C 2 if i = 0, 2µ(maxneg(T ) × g(i -1)) n C 2 if i > 0.
By [START_REF] Minsky | Computation, Finite and Infinite Machines[END_REF] (see also [START_REF] Van Emde | Machine models and simulations[END_REF]), a deterministic Turing machine M of size n running in space K2 n K can be simulated by a deterministic counter automaton C of size O(n) with 4 counters and that is 2 2 n K ′ -bounded (counter values are bounded by 2 2 n K ′ when the initial configuration has zero counter values). Moreover, M can reach a halting state on the empty tape iff C can reach a halting control state with a run starting with zero counter values. A deterministic counter automaton is understood as a simple machine with a finite set of control states equipped with counters and the only instructions on counters are increments, decrements and zero-tests. In [START_REF] Lipton | The reachability problem requires exponential space[END_REF][START_REF] Esparza | Decidability and complexity of Petri net problems -an introduction[END_REF], it is shown that given a deterministic counter automaton C of size n with a halting control state, one can build a net program (equivalent to a Petri net) of size O(n 2 ) simulating C. In particular, its dimension is also in O(n 2 ). This net program can be easily shown equivalent to a VASS V of dimension n ′ (in O(n 2 )), with m ′ control states (also in O(n 2 )) and with two distinguished control states q 0 , q h satisfying the following conditions:

• C halts iff there is a run from (q 0 , 0) reaching a configuration with control state q h .

• Whenever the simulation of C in a run in V is not faithful to C, then the run eventually terminates.

• C does not halt iff there is an infinite run from (q 0 , 0) that never reaches a configuration with control state q h . Consequently, when C halts, all the runs from (q 0 , 0) are finite and there is a finite number of runs from (q 0 , 0). We define the VASS V ′ of dimension n ′ + 1 that behaves as V except that we add a self-loop transition to q h whose effect is to add one to the (n ′ + 1)st component. Then, we have C halts iff there is a run in V ′ of the form (q 0 , 0)

* - → (q, x) * - → (q, x ′ ) such that x([1, n ′ ]) = x ′ ([1, n ′ ]
) and x(n ′ + 1) < x ′ (n ′ + 1). This can be easily turned into an instance of the generalized unboundedness problem. The ExpSpace-hardness proof is therefore a simple adaptation of the ExpSpace-hardness result from [START_REF] Lipton | The reachability problem requires exponential space[END_REF][START_REF] Esparza | Decidability and complexity of Petri net problems -an introduction[END_REF]. Reproducing the arguments would not add much apart from repeating arguments from [START_REF] Esparza | Decidability and complexity of Petri net problems -an introduction[END_REF]. More details about this standard reduction can be also found in the slides [START_REF] Demri | Slides on EXPSPACE-hard problems on VASS[END_REF].

Other Applications

In this section, we draw conclusions from Theorem 4.6. First, as a by-product of Theorem 4.6 and using the reductions from Section 3.3, we can easily regain the ExpSpace upper bound mentioned below. Proof. The ExpSpace upper bound for regularity detection problem and strong promptness detection problem is a consequence of remarks from Section 3.3. Indeed, for both problems, one needs to guess a generalized unbounded property P of length at most n (dimension of the input VASS) and of scale 1 and then check whether there is a run satisfying P. In case of positive answer to this question, we answer negatively to the original instance of the original problem.

Let us establish the lower bound for the simultaneous unboundedness problem. Let V be the VASS from the lower bound proof for Theorem 4.6(I). We define the VASS V ′ of dimension n ′ +1 that behaves as V except that we add a self-loop transition to q h whose effect is to add one to the (n ′ +1)th component. Then, we have C halts iff (V ′ , (q 0 , 0)) is not (n ′ +1)-unbounded. Simultaneous unboundedness problem is therefore coExpSpace-hard but since coExpSpace= ExpSpace, the simultaneous unboundedness problem is ExpSpace-hard. Now, let us establish the upper bound for the simultaneous unboundedness problem. Let (V, (q, x)) be an initialized VASS of dimension n and X be a subset of [1, n]. We first guess a disjointness sequence σ

= X 1 • • • • • X K such that X ⊆ l∈[1,K]
X l and X ∩ X K ∅ (this requires only polynomial space). Let us now consider the generalized unboundedness property P σ as defined in Section 3.3 for dealing with simultaneous unboundedness. Checking whether (V, (q, x)) satisfies P σ can be reduced in logspace to an instance of the generalized unboundedness problem, that can be solved in exponential space in the size of (V, (q, x)): indeed the length of P σ is bounded by n and its scale is equal to one.

The complexity upper bound for regularity detection problem has been left open in [START_REF] Faouzi Atig | On Yen's path logic for Petri nets[END_REF]. Decidability of the strong promptness detection problem is established in [START_REF] Valk | The residue of vector sets with applications to decidability problems in Petri nets[END_REF]. The ExpSpace upper bound has been already stated in [START_REF] Yen | A unified approach for deciding the existence of certain net paths[END_REF][START_REF] Faouzi Atig | On Yen's path logic for Petri nets[END_REF]. We cannot rely on [START_REF] Yen | A unified approach for deciding the existence of certain net paths[END_REF] because of the flaw in [START_REF] Yen | A unified approach for deciding the existence of certain net paths[END_REF]Lemma 7.7]. Condition 4. in [3, page 13] does not characterize strong promptness (but only promptness) as shown in Section 3.3. Finally, increasing path formulae from [START_REF] Faouzi Atig | On Yen's path logic for Petri nets[END_REF] cannot characterize strong promptness detection unlike generalized unboundedness properties. Therefore, the upper bound for strong promptness detection is also new. Below, we state how the previous results allow us to characterize the computational complexity of reversal-boundedness detection problem for VASS and its variant with weak reversal-boundedness. Proof. (I) Let us start by showing ExpSpace-hardness. Let V be the VASS from the lower bound proof for Theorem 4.6(I) obtained from [START_REF] Lipton | The reachability problem requires exponential space[END_REF][START_REF] Esparza | Decidability and complexity of Petri net problems -an introduction[END_REF]. We define the VASS V ′ of dimension n ′ +1 that behaves as V except that we add two transitions q h e n ′ +1 --→ q h and q h -e n ′ +1 ---→ q h where e i denotes the ith unit vector and q h is the halting control state of V. Then, we have C halts iff (V ′ , (q 0 , 0)) is not reversal-bounded with respect to n ′ +1. Reversal-boundedness detection problem is therefore coExpSpace-hard but since coExpSpace= ExpSpace, the problem is ExpSpace-hard. Now, let us show ExpSpace upper bound. Let V = (Q, n, δ) be a VASS and (q, x) be a configuration. By Lemma 2.5, (V, (q, x)) is not reversal-bounded with respect to i iff (T , x ′ ) = ((V rb , (q rb , x rb ))) HP is (n + i)-unbounded. The operator (•) HP refers to the reduction from VASS to VAS in [START_REF] Hopcroft | On the reachability problem for 5-dimensional vector addition systems[END_REF] (see also the proof of Lemma 2.5). scale(T ) is bounded by max((card(Q) × 2 n + 1) 2 , scale(V)) and ((V rb , (q rb , x rb ))) HP can be built in polynomial space. Dimension of T is 2n + 3. First, we guess P of length at most 2n + 3 for characterizing (n + i)-unboundedness (this requires only polynomial space): its scale is equal to one. A witness pseudo-run weakly satisfying P (in T ) does not need to be longer than ((1 + 2n + 3) × 2 × max((card(Q) × 2 n + 1) 2 , scale(V)) 2 ) (2n+3) (2(2n+3)+1)C , which is doubly exponential in the size of V and (q, x) (our initial instance). This comes from Lemma 4.5. A nondeterministic algorithm guessing such a pseudo-run requires only exponential space. (II) When n is fixed, the above expression is only exponential in the size of V and (q, x). (III) This part is similar to (I) and (II). By combining Lemmas 3.6 and 3.2, we build in polynomial space an initialized VAS (T , x ′ ) such that (V, (q, x)) is not weakly reversal-bounded iff (T , x ′ ) satisfies P ′ σ for some disjointness sequence σ = X 1 • • • X K with n + i ∈ X K , i ∈ (X 1 ∪ • • • ∪ X K-1 ) and such that • P ′ σ is defined from P σ as done in the proof of Lemma 3.2 (length bounded by n and scale equal to 1),

• the dimension of T is 2n + 3,

• scale(T ) ≤ max((card(Q) × 2 n + 1) 2 , scale(V)).

Again, a witness pseudo-run weakly satisfying P ′ σ (in (T , x ′ )) does not need to be longer than

((1 + 2n + 3) × 2 × max((card(Q) × 2 n + 1) 2 , scale(V)) 2 ) (2n+3) (2(2n+3)+1)C
which is doubly exponential in the size of V and (q, x) (our initial instance). A nondeterministic algorithm guessing such a pseudo-run requires only exponential space.

Let us establish the ExpSpace-hardness. Let V be the VASS from the lower bound proof for Theorem 4.6(I). We define the VASS V ′ of dimension n ′ +1 that behaves as V except that we add two transitions q h 2×e n ′ +1 ----→ q ′ h -e n ′ +1 ---→ q h Then, C halts iff (V ′ , (q 0 , 0)) is not weakly reversal-bounded with respect to n ′ + 1. Weak reversal-boundedness detection problem is therefore coExpSpacehard, whence ExpSpace-hard. By Theorem 5.2(I), once an initialized VASS is shown to be reversal-bounded, one can compute effectively semilinear sets corresponding to reachability sets, for instance one by control state, see recent developments in [START_REF] Kopczynski | Parikh Images of Grammars: Complexity and Applications[END_REF]. The size of the representation of such sets is at least polynomial in the maximal number of reversals. However, we know that an initialized VASS can be bounded but still the cardinality of its reachability set may be nonprimitive recursive, see e.g. [START_REF] Valk | Petri nets and regular languages[END_REF]. A similar phenomenon occurs with reversal-boundedness, as briefly explained below. Not only we wonder what is the computational complexity of the problem of determining whether a VASS is reversal-bounded but also in case of reversal-boundedness, it is important to evaluate the size of the maximal reversal r in terms of the size of the VASS, see e.g. the recent work [START_REF] Kopczynski | Parikh Images of Grammars: Complexity and Applications[END_REF] following [START_REF] Howell | An analysis of the nonemptiness problem for classes of reversal-bounded multicounter machines[END_REF] that uses in an essential way the value r. In case of reversalboundedness, the maximal reversal can be nonprimitive recursive in the size of the initialized VASS in the worst case, which, we admit, is not an idyllic situation for analyzing reversalbounded VASS. Indeed, given n ≥ 0, one can compute in polynomial time in n an initialized VASS (V n , (q 0 , x n )) that generates a finite reachability set of cardinal O(A(n)) for some nonprimitive recursive map A(•) similar to Ackermann function, see e.g., the construction in [START_REF] Jantzen | Complexity of Place/Transition Nets[END_REF]. Let us precise what this means by recalling a variant of Ackermann function:

• A 0 (m) = 2m + 1, A n+1 (0) = 1.
• A n+1 (m + 1) = A n (A n+1 (m)).

• A(n) = A n (2).

The function A(n) majorizes the primitive recursive functions.

Moreover, (V n , (q 0 , x n )) can be shown to admit only finite runs, see details in [START_REF] Jantzen | Complexity of Place/Transition Nets[END_REF]. It is then easy to compute a variant VASS V ′ n by adding a component and such that each transition of V n is replaced by itself followed by incrementating the new component and then decrementing it (creating a reversal). Still V ′ n has no infinite computation, (V ′ n , (q 0 , x ′ n )) is reversal-bounded ( x ′ n restricted to the components of V n is equal to x n ) and its maximal reversal is in O(A(n)).

Concluding Remarks

We have proved the ExpSpace upper bound for the generalized unboundedness problem (both the initialized VASS and the generalized unboundedness property are part of the inputs). For example, this allows us to show, for the first time (apart from the preliminary version [START_REF] Demri | On Selective Unboundedness of VASS[END_REF]), that the following problems on VASS can be solved in exponential space:

• the place boundedness problem,

• the reversal-boundedness detection problem,

• the regularity detection problem,

• the strong promptness detection problem.

We have shown that these problems can be solved in polynomial space when the dimension is fixed. Even though our proof technique is clearly tailored along the lines of [START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF], we had to provide a series of adaptations in order to get the final ExpSpace upper bound (and the PSpace upper bound for fixed dimension). In particular, we advocate the use of witness pseudo-run characterizations (instead of using runs) when there exist decision procedures using coverability graphs.

Let us conclude by possible continuations. First, our ExpSpace proof can be obviously extended for example by admitting covering constraints, to replace intervals in properties by more complex sets of integers or to combine our proof technique with the one from [START_REF] Faouzi Atig | On Yen's path logic for Petri nets[END_REF], see also [START_REF] Blockelet | Model-checking coverability graphs of vector addition systems[END_REF]. The robustness of our proof technique still deserves to be determined. A challenging question is to determine the complexity of checking when a reachability set obtained by an initialized VASS is semilinear. Indeed, it was proved independently by Hauschildt and Lambert that the class of semilinear VASS is recursive: checking whether a given VASS has a semilinear reachability set is decidable [see the unpublished works by [START_REF] Hauschildt | Semilinearity of the reachability set is decidable for Petri nets[END_REF][START_REF] Lambert | Vector Addition Systems and Semi-Linearity[END_REF]. Moreover, the reachability set is effectively computable when it is semilinear. Observe that regularity, boundedness or reversal-boundedness imply semilinearity.

Another direction consists in considering a richer class of models. It is shown in [START_REF] Finkel | Mixing coverability and reachability to analyze VASS with one zero-test[END_REF] that checking whether an initialized VASS with one zero-test is reversal-bounded is decidable, but with a nonprimitive recursive worst-case complexity, the existence of an ExpSpace upper bound being open; see also recent results on VASS with one zero-test [START_REF] Bonnet | Decidability of LTL model checking for vector addition systems with one zero-test[END_REF][START_REF] Bonnet | The reachability problem for vector addition systems with one zero-test[END_REF].

Besides, various subclasses of VASS exist for which decision problems are of lower complexity. For instance, in [START_REF] Praveen | Modelchecking counting properties of 1-safe nets with buffers in paraPSPACE[END_REF], the boundedness problem is shown to be in PSpace for a class of VASS with so-called bounded benefit depth. It is unclear for which subclasses of VASS, the generalized unboundedness problem can be solved in polynomial space too.

Figure 3 :

 3 Figure 3: 5 reversals in a row

  introduce intervals in place of such constraints. An interval is an expression of one of the forms ] -∞, +∞[, [a, +∞[, ] -∞, b] or [a, b] for some a, b ∈ Z interpreted as a subset of Z (with the obvious interpretation). Definition 3.1. A generalized unboundedness property P = (I 1 , . . . , I K ) is a nonempty sequence of n-tuples of intervals. ∇

  Guess a transition t ∈ T ; If x c + t N n then abort; (b) i := i + 1; x c := x c + t. 4. y := x c ; 5. While i < L ′′ do (a) Guess a transition t ∈ T ; If x c + t N n then abort; (b) i := i + 1; x c := x c + t. 6. Return y ≺ x c .

  satisfies the approximation property A[P, l, INCR, I, B] (also abbreviated by A) def ⇔ the conditions below are verified:

Lemma 4 . 2 .

 42 Let T be a VAS of dimension n ≥ 2, P be a generalized unboundedness property of length K, l ∈ [1, K], B ≥ 2, I, INCR ⊆ [1, n] and ρ be a pseudo-run satisfying A[P, l, INCR, I, B]. Then, there exists a pseudo-run starting by the same pseudo-configuration, satisfying A[P, l, INCR, I, B] and of length at most (1 + K) × (scale(T ) × scale(P) × B) n C 1 for some constant C 1 independent of K, scale(P), scale(T ), B and n. The length expression in Lemma 4.2 can be certainly refined in terms of card(INCR), card(I) and l but these values are anyhow bounded by n and K respectively, which is used in Lemma 4.2. The proof below is essentially a refinement of the proof of [45, Lemma 4.4]. Proof. Let P = (I 1 , . . . , I K ), l ∈ [1, K], I, INCR ⊆ [1, n] and ρ be the pseudo-run described below satisfying A[P, l, INCR, I, B]:

  we obtain a pseudo-run satisfying A[P, l, INCR, I, B] whose length is bounded by the value below:(K + 1)B n + K[(B n + 1) 2 + number of effects (1 + 2 × scale(T )) n B n 2 × maximal number of copies per effect [(1 + 2 × scale(T ) × scale(P)) n B 2n 2 ] C2n ×bound on the length of simple loop (B n + 1) ]

Lemma 4 .Lemma 4 . 4 .

 444 4 below is an extension of [45, Lemmas 4.6 & 4.7], see also [3, Lemma 7]. Let I, INCR ⊆ [1, n], l ∈ [1, K] and ρ be a pseudo-run satisfying A[P, l, INCR, I, +∞]. Then, there exists a pseudo-run ρ ′ starting from the same pseudo-configuration, satisfying the property A[P, l, INCR, I, +∞] and of length at most g(card(I)).

Case 1 :

 1 Every configuration z in ρ satisfies z(J) ∈ [0, B -1] J , i.e., ρ satisfies A[P, l, INCR, I, B]. Obviously, the case J = ∅ is captured here. By Lemma 4.2, there is a pseudo-run ρ ′ starting atx 2l-2 satisfying A[P, l, INCR, I, B] of length at most (1 + K) × (scale(T ) × scale(P) × B) n C 1 , which is bounded by µ × (maxneg(T ) × g(i)) n C 1 .Case 2: A value for some component in J is strictly greater than B-1 for the first time within the path π ′ D for some D ∈ [l -1, K -1]. Let α be the minimal position such that u α+1 (J) [0, B -1] J and α + 1 ∈ [ f (2D) + 1, f (2D + 1)], say u α+1 (i 0 ) ≥ B for some i 0 ∈ J. The pseudo-run ρ can be decomposed as follows with π ′ D = π 1 D t α+1 π 2 D (INCR ′ is defined few lines below):

Corollary 5 . 1 .

 51 The regularity detection problem and the strong promptness detection problem are in ExpSpace. The simultaneous unboundedness problem is ExpSpace-complete. For each fixed n ≥ 1, their restriction to VASS of dimension at most n are in PSpace.

Theorem 5. 2 .

 2 (I) Reversal-boundedness detection problem for VASS is ExpSpace-complete.(II) For each fixed n ≥ 1, its restriction to VASS of dimension at most n is in PSpace.(III) (I) and (II) hold true for weak reversal-boundedness.

Acknowledgments: I would like to thank Thomas Wahl (U. of Oxford) and anonymous referees for their suggestions and remarks about a preliminary version of this work.

1 Complete version of the conference paper [13]. Work partially supported by ANR project REACHARD ANR-11-BS02-001.

By induction on i, we can show that g(i) ≤ (ν i+1 ) n (2i+1)C 2 with ν = 2µ × maxneg(T ). For i = 0 this is obvious. Otherwise,

Let us conclude the section by the main result of the paper. Proof. (I, upper bound) Let (V, (q, x)) be an initialized VASS of dimension n and P be a generalized unboundedness property. By Lemma 3.2, one can compute in logarithmic space an initialized VAS ((T , x ′ ), P ′ ) such that (V, (q, x)) satisfies P iff (T , x ′ ) satisfies P ′ , T has dimension n + 3, P and P ′ have the same length and scale(T ) = max((card(Q) + 1) 2 , scale(V)). The propositions below are equivalent:

1. T has a run satisfying P ′ .

2. T has a pseudo-run weakly satisfying P ′ (see Lemma 3.7).

T has a pseudo-run satisfying

4. T has a pseudo-run weakly satisfying P ′ whose length is bounded by

(by Lemma 4.5).

Then, we guess a witness pseudo-run weakly satisfying P ′ whose length is bounded by

This can be done in exponential space in the combined size of (V, (q, x)) and P. By Savitch's Theorem [START_REF] Savitch | Relationships between nondeterministic and deterministic tape complexities[END_REF], we get the ExpSpace upper bound. It is indeed sufficient to adapt the nondeterministic algorithm designed at the beginning of Section 4.3 in order to consider the abovementionned length. Actually, one needs to consider K + 1 intermediate pseudo-configurations and a current set of components among [1, n + 3] in order to record which components can be strictly increased in preceeding loops.

(II) Easy consequence of the proof of (I, upper bound).

(I, lower bound) A first temptation is to state ExpSpace-hardness from ExpSpace-hardness of the unboundedness problem for VAS. However, we are looking for a logarithmic-space manyone reduction and an instance of unboundedness can be naturally reduced to n instances of the generalized unboundedness problem with property of length 1 and scale 1. We shall directly adapt [START_REF] Lipton | The reachability problem requires exponential space[END_REF][START_REF] Esparza | Decidability and complexity of Petri net problems -an introduction[END_REF] to obtain the lower bound.