Jérôme Leroux

Vincent Penelle

Grégoire Sutre

The Context-Freeness Problem is coNP-complete for Flat Counter Systems

Bounded languages have recently proved to be an important class of languages for the analysis of Turing-powerful models. For instance, bounded context-free languages are used to under-approximate the behaviors of recursive programs. Ginsburg and Spanier have shown in 1966 that a bounded language

, and only if, its Parikh image is a stratifiable semilinear set. However, the question whether a semilinear set is stratifiable, hereafter called the stratifiability problem, was left open, and remains so. In this paper, we give a partial answer to this problem. We focus on semilinear sets that are given as finite systems of linear inequalities, and we show that stratifiability is coNP-complete in this case. Then, we apply our techniques to the context-freeness problem for flat counter systems, that asks whether the trace language of a counter system intersected with a bounded regular language is context-free. As main result of the paper, we show that this problem is coNP-complete.

Introduction

The class of bounded languages was introduced in 1964 by Ginsburg and Spanier to study context-free languages [START_REF] Ginsburg | Bounded ALGOL-like languages[END_REF]. Nowadays, this class plays an important role in the analysis of Turing-powerful models. Recall that a language is bounded if it is contained in σ * 1 • • • σ * d for some words σ 1 , . . . , σ d . The restriction of a model to behaviors contained in a bounded language produces a so-called flat model that is often amenable to automatic verification. Indeed, the reachability sets of such restrictions are usually computable through acceleration techniques [START_REF] Boigelot | Symbolic verification with periodic sets[END_REF][START_REF] Bouajjani | Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations[END_REF][START_REF] Comon | Multiple counters automata, safety analysis and Presburger arithmetic[END_REF][START_REF] Annichini | TReX: A tool for reachability analysis of complex systems[END_REF][START_REF] Finkel | Well-abstracted transition systems: Application to FIFO automata[END_REF][START_REF] Bardin | Fast: acceleration from theory to practice[END_REF][START_REF] Bozga | Fast acceleration of ultimately periodic relations[END_REF]. Following the same approach, bounded languages have recently been used for the analysis of recursive concurrent systems, and more generally as a way to unify various recent and promising "bounded verification" techniques [START_REF] Esparza | A perfect model for bounded verification[END_REF].

In these applications, the class of semilinear bounded languages is central. Recall that a semilinear set is a finite union of sets of the form b+Np 1 +• • •+Np k where b, p 1 , . . . , p k are vectors in N d . Semilinear sets coincide with the sets definable in Presburger arithmetic [START_REF] Ginsburg | Semigroups, Presburger formulas and languages[END_REF]. A semilinear bounded language is a language of the form {σ n1 1 • • • σ n d d | (n 1 , . . . , n d ) ∈ S} where σ 1 , . . . , σ d are words and S is a semilinear set. The class of semilinear bounded languages admits several characterizations through language acceptors [START_REF] Cadilhac | Bounded parikh automata[END_REF][START_REF] Ibarra | Characterizations of bounded semilinear languages by one-way and two-way deterministic machines[END_REF][START_REF] Esparza | A perfect model for bounded verification[END_REF]. From a language-theoretic viewpoint, semilinear bounded languages are incomparable with context-free languages. Indeed, the language {a n b n c n | n ∈ N} is well-known to be noncontext-free, and, conversely, the language {a, b} * is not a bounded language. However, bounded context-free languages are semilinear bounded languages, by Parikh's theorem and closure under inverse morphism of context-free languages.

Ginsburg and Spanier have established in [START_REF] Ginsburg | Semigroups, Presburger formulas and languages[END_REF][START_REF] Ginsburg | The Mathematical Theory of Context-Free Languages[END_REF] a characterization of bounded context-free languages in terms of semilinear sets satisfying a "stratification" requirement. We call such semilinear sets stratifiable. The existence of a decision procedure for determining whether a given semilinear set is stratifiable was left open in [START_REF] Ginsburg | Semigroups, Presburger formulas and languages[END_REF][START_REF] Ginsburg | The Mathematical Theory of Context-Free Languages[END_REF], and has remained open since then. Rephrased in terms of languages, this decision problem is equivalent to the question whether a given semilinear bounded language is context-free. The latter problem is known to be decidable for some subclasses of semilinear bounded languages, with a notable example being the trace languages of flat Petri nets. In fact, the context-freeness problem is decidable for trace languages of arbitrary Petri nets [START_REF] Schwer | The context-freeness of the languages associated with vector addition systems is decidable[END_REF][START_REF] Leroux | On the context-freeness problem for vector addition systems[END_REF], and was recently shown to be ExpSpace-complete for them [START_REF] Leroux | A relational trace logic for vector addition systems with application to context-freeness[END_REF].

Contributions. In this paper, we provide a partial answer to the question whether a given semilinear set is stratifiable, hereafter called the stratifiability problem. We focus on semilinear sets that are integral polyhedra, in other words, that are given as finite systems of linear inequalities. Our contributions are twofold.

As main technical result of the paper, we show that the stratifiability problem for integral polyhedra is coNP-complete. The proof is decomposed in two steps. First, we reduce the stratifiability of an integral polyhedron {x ∈ N d | Ax ≥ b} to a stratification-like property, called nestedness, that only involves the matrix A. We then provide a criterion for nestedness, and show how to express this criterion by a polynomial-size quantifier-free formula in the first-order theory of the rational numbers with addition and order. This way, we obtain that the stratifiability problem for integral polyhedra is solvable in coNP. The proof of coNP-hardness is by reduction from the emptiness problem for integral polyhedra.

Building on this result, we then investigate the context-freeness problem for flat counter systems, that asks whether the trace language of a counter system intersected with a bounded regular language is context-free. In our setting, counter systems are a generalization of Petri nets where transitions are guarded by integral polyhedra. Such guards can express zero tests, so counter systems are Turing-powerful since they subsume Minsky machines. By exploiting the restriction to bounded languages required by flatness, we show that the contextfreeness problem for flat counter systems is coNP-complete, and remains so for flat Petri nets.

Related Work. The class of semilinear bounded languages was recently characterized through various language acceptors, namely, Parikh automata [START_REF] Cadilhac | Bounded parikh automata[END_REF], reversal-bounded counter machines [START_REF] Ibarra | Characterizations of bounded semilinear languages by one-way and two-way deterministic machines[END_REF], and multi-head pushdown automata [START_REF] Esparza | A perfect model for bounded verification[END_REF]. The class of semilinear sets was shown in [START_REF] Liu | A characterization of semilinear sets[END_REF] to coincide with the finite intersections of stratifiable semilinear sets. It follows that the class of bounded context-free languages is a generating class for the semilinear bounded languages. In [START_REF] Ibarra | On the open problem of Ginsburg concerning semilinear sets and related problems[END_REF], the stratifiability problem is shown to be equivalent to the existence of a 0-synchronized n-tape pushdown automaton equivalent to a given n-tape finite-state automaton whose language is contained in a

* 1 × • • • × a * n .
In a recent paper [START_REF] Leroux | On the context-freeness problem for vector addition systems[END_REF], we proved that the trace language of a Petri net is context-free if, and only if, it has a context-free intersection with every bounded regular language. Building on this characterization, we then established in [START_REF] Leroux | A relational trace logic for vector addition systems with application to context-freeness[END_REF] that the contextfreeness problem for Petri nets is ExpSpace-complete, but the complexity was left open for the subcase of flat Petri nets. Here, we show that the context-freeness problem for flat Petri nets is coNP-complete. Related to our work is the question whether a given model is a posteriori flat, in other words, whether the set of all its behaviors is a bounded language. This question is shown in [START_REF] Chambart | Forward analysis and model checking for trace bounded WSTS[END_REF] to be decidable for the class of complete and deterministic well-structured transition systems.

Outline. The paper is organized as follows. Preliminary notations are given in Section 2. We recall the definition of stratifiable semilinear sets in Section 3. The stratifiability problem for integral polyhedra is shown to be decidable in Section 4, and it is proved to be coNP-complete in Section 5. We then address the context-freeness problem for flat counter systems, and show in Section 6 that it is coNP-complete. Section 7 concludes the paper with directions for future work.

Preliminaries

We let N, Z and Q denote the usual sets of nonnegative integers, integers and rational numbers, respectively. We write N 1 for the set of positive integers and Q ≥0 for the set of nonnegative rational numbers. Vectors (of rational numbers), sets of vectors and matrices are typeset in bold face. The ith component of a vector v is written v(i). The support of a vector v, written supp(v), is the set of indices i such that v(i) = 0. We let e i denote the ith unit vector, defined by e i (i) = 1 and e i (j) = 0 for all indices j = i.

A partial-order on a set S is a binary relation on S that is reflexive, antisymmetric and transitive. As usual, we write s ≺ t when s t and t s. A well-partial-order on S is a partial-order on S such that every infinite sequence s 0 , s 1 , s 2 , . . . in S contains an increasing pair s i s j with i < j.

Stratifiable Semilinear Sets

Building on earlier work with Spanier [START_REF] Ginsburg | Semigroups, Presburger formulas and languages[END_REF], Ginsburg provides, in his book [START_REF] Ginsburg | The Mathematical Theory of Context-Free Languages[END_REF], a characterization of bounded context-free languages in terms of semilinear sets satisfying a "stratification" requirement. We call such semilinear sets stratifiable. The existence of a decision procedure for determining whether a given semilinear set is stratifiable was left open in [START_REF] Ginsburg | Semigroups, Presburger formulas and languages[END_REF][START_REF] Ginsburg | The Mathematical Theory of Context-Free Languages[END_REF], and has remained open since then. We provide a partial answer to this problem in Sections 4 and 5. Before that, we recall in this section the definition of stratifiable semilinear sets, and how they can be used to characterize bounded context-free languages.

Given a finite set P = {p 1 , . . . , p k } of vectors in N d , we let P denote the set of finite sums of vectors in P , i.e., P = Np 1 + • • • + Np k . A linear set is a set of the form b + P where b is a vector in N d and P is a finite subset of N d . The vector b is called the basis, and the vectors in P are called periods. A semilinear set is a finite union of linear sets. Recall that semilinear sets coincide with the sets definable in FO (N, 0, 1, +, ≤), also known as Presburger arithmetic [START_REF] Ginsburg | Semigroups, Presburger formulas and languages[END_REF].

Definition 3.1 ( [START_REF] Ginsburg | Semigroups, Presburger formulas and languages[END_REF][START_REF] Ginsburg | The Mathematical Theory of Context-Free Languages[END_REF]). A finite subset P of N d is stratified if every vector in P has at most two non-zero components, and it holds that

p(r) = 0 ∧ p(t) = 0 ∧ q(s) = 0 ∧ q(u) = 0 ⇒ ¬(r < s < t < u)
for every vectors p, q ∈ P and indices r, s, t, u ∈ {1, . . . , d}.

Example 3.2. The following examples are from [START_REF] Ginsburg | The Mathematical Theory of Context-Free Languages[END_REF]. The set {(2, 1, 0), (0, 3, 3)} is stratified, but the set {(1, 1, 1), (1, 0, 2)} is not stratified, since (1, 1, 1) has three non-zero components. The set {(3, 0, 0, 2), (0, 1, 5, 0), (4, 7, 0, 0)} is stratified, but the set {(2, 0, 3, 0), (0, 3, 0, 2)} is not stratified.

We call a semilinear set stratifiable when it is a finite union of linear sets, each with a stratified set of periods. Formally, a semilinear set S is stratifiable if there exits a finite family {(b i , P i )} i∈I of vectors b i in N d and finite stratified subsets P i of N d such that S = i∈I (b i + P i ). The following lemma shows that stratifiable semilinear sets enjoy nice closure properties.

Lemma 3.3. The class of stratifiable semilinear sets is closed under union, under projection, under inverse projection, and under intersection with Cartesian products of intervals.

Proof. These closure properties are easily derived from the definition of stratifiable semilinear sets.

The stratifiability problem asks whether a given semilinear set S is stratifiable. The decidability of the stratifiability problem was raised in [START_REF] Ginsburg | Semigroups, Presburger formulas and languages[END_REF][START_REF] Ginsburg | The Mathematical Theory of Context-Free Languages[END_REF], and has been open for nearly fifty years. Stratifiability is linked to the following characterization of bounded context-free languages.

We consider words over a finite alphabet Σ. Recall that a language

L ⊆ Σ * is bounded if L ⊆ σ * 1 • • • σ * d for some words σ 1 , . . . , σ d in Σ * .
In his book [START_REF] Ginsburg | The Mathematical Theory of Context-Free Languages[END_REF], Ginsburg characterizes which bounded languages are context-free, in terms of semilinear sets. The reader is referred to [START_REF] Ginsburg | The Mathematical Theory of Context-Free Languages[END_REF] for further details.

Theorem 3.4 ([14, p. 162]). Consider a language L ⊆ σ * 1 • • • σ * d , where each σ i ∈ Σ * . Then L is context-free if, and only if, the set of all vectors (n 1 , . . . , n d ) in N d such that σ n1 1 • • • σ n d d ∈ L is a stratifiable semilinear set. Example 3.5. Take Σ = {a, b, c}. The language {a n b m c n | n, m ∈ N} is context- free since the set {(n 1 , n 2 , n 3 ) ∈ N 3 | n 1 = n 3 }
is the linear set P where P = {(1, 0, 1), (0, 1, 0)} is stratified. The language {a n b n c n | n ∈ N} is known to be non-context-free. This means the semilinear set N(1, 1, 1) is not stratifiable.

In this section, we show that stratifiability is decidable for a subclass of semilinear sets, namely the sets of integral solutions of finite systems of linear inequalities. Formally, an integral polyhedron is a set of the form {x ∈ N d | Ax ≥ b} where A ∈ Z n×d is a matrix and b ∈ Z d is a vector. Every linear system Ax ≥ b can be encoded into Presburger arithmetic, so integral polyhedra are semilinear sets. The stratifiability problem for integral polyhedra asks, given a matrix A ∈ Z n×d and a vector b ∈ Z d , both encoded in binary, whether the integral polyhedron {x ∈ N d | Ax ≥ b} is stratifiable. The remainder of this section reduces this problem to a decision problem that only involves the matrix A ∈ Z n×d .

First, we show that stratifiability for integral polyhedra can be reduced to the particular case of homogeneous linear inequalities. Formally, an integral cone is a set of the form {x ∈ N d | Ax ≥ 0} where A ∈ Z n×d is a matrix. The following lemma shows that every integral cone is a linear set, and provides a way to decompose integral polyhedra into integral cones.

{x ∈ N d | Ax ≥ b} = B + P and P = {x ∈ N d | Ax ≥ 0}
We have considered so far integral solutions of finite systems of linear inequalities. To simplify our analysis, we now move from integers to rational numbers. A cone is a set of the form {x ∈ Q d ≥0 | Ax ≥ 0} where A ∈ Z n×d is a matrix. Given a finite set P = {p 1 , . . . , p k } of vectors in N d , we let P denote the set of linear combinations of vectors in P with nonnegative rational coefficients, i.e.,

P = Q ≥0 p 1 + • • • + Q ≥0 p k .
Put differently, P is defined as P except that Q ≥0 p i replaces Np i . Observe that P = Q ≥0 P for every finite subset P of N d . Let us recall the following well-known property.

Property 4.2 (Farkas-Minkowski-Weyl Theorem

). A subset X of Q d
≥0 is a cone if, and only if, X = P for some finite subset P of N d .

In order to extract the asymptotic directions of an integral polyhedron, we associate to every finite subset P ⊆ N d a partial-order P on N d defined by x P y if y ∈ x + P . Observe that when P = {e 1 , . . . , e d }, the partial-order P coincides with the classical partial order ≤ on N d , which is known to be a well-partial-order on N d = N d ∩ P , by Dickson's lemma. This observation can be generalized to any finite subset P of N d , as follows. We refer the reader to the proof of Lemma 1.2 from [START_REF] Hopcroft | On the reachability problem for 5-dimensional vector addition systems[END_REF] for details.

Lemma 4.3 ([15]

). The partial-order P on N d is a well-partial-order on N d ∩ P , for every finite subset P of N d .

To show that the stratifiability problem for integral polyhedra is decidable, we decompose cones into "maximal stratifiable parts". The formal definition of these parts requires some additional notations. A binary relation R on {1, . . . , d} is called nested if it satisfies the two following conditions:

(s, t) ∈ R ⇒ s ≤ t (1) (r, t) ∈ R ∧ (s, u) ∈ R ⇒ ¬(r < s < t < u) (2)
An example of a nested relation is depicted in Figure 1a. Given a cone X ⊆ Q d ≥0 and a nested binary relation R on {1, . . . , d}, we introduce the set X R defined as follows:

X R = r∈R X r
where, for each pair r = (s, t) of indices satisfying 1 ≤ s ≤ t ≤ d, the set X r is given by:

X r =    x ∈ X j ∈{s,t} x(j) = 0   
Intuitively, the "maximal stratifiable parts" mentioned previously are the sets X R . The "stratification" property of X R is expressed by the following lemma.

Lemma 4.4. For every cone X ⊆ Q d ≥0 and every nested binary relation R on {1, . . . , d}, it holds that X R = P R for some finite stratified subset

P R of N d . Proof. Consider a cone X = {x ∈ Q d ≥0 | Ax ≥ 0}
and a nested binary relation R on {1, . . . , d}. First, notice that X r is a cone for every r = (s, t) in R. Indeed, every constraint x(j) = 0 may be expressed as the conjunction of x(j) ≥ 0 and -x(j) ≥ 0. By adding these inequalities to the matrix A for every j ∈ {s, t}, we obtain a matrix witnessing that X r is a cone. It follows from Property 4.2 that X r = P r for some finite subset P r ⊆ N d . Therefore, X R = P R where P R is the finite subset of N d defined by P R = r∈R P r . Since R is nested, we derive that P R is stratified, which concludes the proof of the lemma.

We are now ready to provide a decidable characterization of stratifiable integral polyhedra. Given a cone X ⊆ Q d ≥0 , we say that X is nested if X = R X R . It is understood that the union ranges over nested binary relations on {1, . . . , d}. Observe that each X R is contained in X, since cones are closed under addition. So nestedness only requires that X is contained in R X R . The cone nestedness problem asks, given a matrix A ∈ Z n×d encoded in binary, whether the cone

{x ∈ Q d ≥0 | Ax ≥ 0} is nested. Theorem 4.5. An integral polyhedron {x ∈ N d | Ax ≥ b} is stratifiable if, and only if, it is empty or the cone {x ∈ Q d ≥0 | Ax ≥ 0} is nested.
Proof. For brevity, we let S denote the integral polyhedron {x ∈ N d | Ax ≥ b}, and X denote its associated cone {x ∈ Q d ≥0 | Ax ≥ 0}. We first prove the "if" direction of the theorem. If S is empty then it is trivially stratifiable. Let us assume that X is nested. According to Lemma 4.1, the integral polyhedron S can be decomposed into a sum S = B +H where B ⊆ N d is a finite set and H is the integral cone {x ∈ N d | Ax ≥ 0}. Observe that X = R X R since X is nested, and that H ⊆ X by definition. We derive that H can be decomposed into H = R H R where H R = H ∩ X R . By Lemma 4.4, there exists a finite stratified set P R ⊆ N d such that X R = P R . Lemma 4.3 entails that P R is a well-partial-order on N d ∩ X R . It follows that the set of minimal elements of H R for this well-partial-order is a finite set. Moreover, writing B R this finite set, we obtain that H R ⊆ B R + P R . We have proved the inclusion H ⊆ R (B R + P R ). Since the converse inclusion is immediate, the set H is stratifiable. From S = B + H, we deduce that S is stratifiable.

We now prove the "only if" direction of the theorem. Let us assume that S is non-empty and stratifiable. Since S is stratifiable, it can be decomposed into

i∈I (b i + P i ) where I is finite, b i ∈ N d and P i ⊆ N d is a finite stratified set.
Let us first show that P i ⊆ R X R . Define R i to be the set of pairs (s, t), with 1 ≤ s ≤ t ≤ d, such that p(s) = 0 ∧ p(t) = 0 for some vector p ∈ P i . It is readily seen that R i is a nested binary relation on {1, . . . , d}, since P i is stratified. Let p ∈ P i . For each n ∈ N, it holds that b i + np ∈ S. Thus, Ab i + nAp ≥ b for every n ∈ N. We deduce that Ap ≥ 0, hence, p ∈ X. By definition of R i , we get that p ∈ X Ri . Since X Ri is closed under addition, we obtain that P i ⊆ X Ri .

To prove that X ⊆ R X R , it is enough to show that N d ∩ X ⊆ R X R , since cones are closed under multiplication with nonnegative rational numbers. Let x ∈ N d ∩ X. Since S is non-empty, there exists s ∈ S. For every n ∈ N, we have A(s + nx) ≥ b, hence, s + nx ∈ S. By the pigeon-hole principle, there exists i ∈ I and an infinite set N ⊆ N such that s + nx ∈ b i + P i for every n ∈ N . Lemma 4.3 entails that P i is a well-partial-order on N d ∩ P i . Since x n = sb i + nx is in P i ⊆ N d ∩ P i for every n ∈ N, we deduce that there exists n, m ∈ N such that n < m and x n P i x m . It follows that (m -n)x = x m -x n ∈ P i . Since P i ⊆ R X R , we obtain that x ∈ R X R . We have shown that N d ∩ X ⊆ R X R , and we conclude that X is nested.

Given a cone X = {x ∈ Q d ≥0 | Ax ≥ 0}, we may compute from the matrix A a formula in the theory FO (Q, 0, 1, +, ≤) expressing the equality X = R X R . Since this theory is decidable by Fourier-Motzkin quantifier elimination, we obtain that the cone nestedness problem is decidable. It follows from Theorem 4.5 that the stratifiability problem for integral polyhedra is decidable. We show, in the next section, that this problem is coNP-complete.

A Criterion for Cone Nestedness Decidable in coNP

We provide, in this section, a criterion for checking whether a given cone is nested. This criterion leads to a coNP decision procedure for the cone nestedness problem, and similarly for the stratifiability problem for integral polyhedra. We also show that the latter upper bound is tight.

To every cone X ⊆ Q d ≥0 , we associate the set ı X = R X R . Recall that X is non-nested precisely when X ⊆ ı X. We show that non-nestedness of a cone X can always be witnessed by a vector in X \ ı X of a special form. We will need the following easy facts. An illustration of the first lemma is given in Figure 1a.

Lemma 5.1. Assume that d ≥ 3. A binary relation R on {1, . . . , d} is nested if, and only if, there exist a pivot p with 1 < p < d and two nested binary relations U and V on {1, . . . , p} and {p, . . . , d}, respectively, such that R ⊆ {(1, d)} ∪ U ∪ V . Lemma 5.2. For every x ∈ ı X, there exists a nested binary relation R on3 supp(x) such that x ∈ X R .

Proof (sketch). If x ∈ ı

X then x = r∈R x r for some nested binary relation R on {1, . . . , d} and some vectors x r ∈ X r . We can assume, w.l.o.g., that x r (s) = 0 and x r (t) = 0 for each pair r = (s, t). Indeed, if x r = 0 then r can be removed from R, and, otherwise, if x r (s) = 0 or x r (t) = 0 then r can be replaced by (t, t) or (s, s), respectively. It follows that R is a nested binary relation on supp(x).

Consider a cone X ⊆ Q d ≥0 . Given a pair r = (s, t) of indices with 1 ≤ s ≤ t ≤ d, we call r-decomposition 4 any triple (a, y, z) of vectors in X r × X × X such that supp(y) ⊆ {s, . . . , p} and supp(z) ⊆ {p, . . . , t} for some pivot p satisfying s < p < t. Since cones are closed under addition, the vector a + y + z is in X for every decomposition (a, y, z). The following lemma shows that membership in ı X is also preserved by decomposition.

Lemma 5.3. For every r-decomposition (a, y, z), it holds that

(a + y + z) ∈ ı X if y ∈ ı X and z ∈ ı X.
Proof. Assume that y ∈ ı X and z ∈ ı X. By Lemma 5.2, there exists two nested binary relations U on supp(y) and V on supp(z) such that y ∈ X U and z ∈ X V . Since (a, y, z) is an r-decomposition, there exists a pivot p with s < p < t, where r = (s, t), such that supp(y) ⊆ {s, . . . , p} and supp(z) ⊆ {p, . . . , t}. It follows that the field 5 of U and the field of V are contained in {s, . . . , p} and {p, . . . , t}, respectively. We derive from Lemma 5.1 that the binary relation R = {(s, t)} ∪ U ∪ V is nested. Observe that a, y and z are all in X R . Since X R is closed under addition, we obtain that (a + y + z) ∈ X R , which concludes the proof of the lemma.

We call a vector x ∈ X reducible 4 when supp(x) has cardinality at most two, or there exists a pair (s, t) of indices in supp(x), with 1 ≤ s ≤ t ≤ d, and an (s, t)-decomposition (a, y, z) such that x = a + y + z. The latter condition is depicted in Figure 1b. Note that this condition entails that supp(x) ⊆ {s, . . . , t}. A vector x ∈ X is called irreducible 4 when it is not reducible. The following theorem characterizes which cones are nested, in terms of irreducible vectors. Before that, we illustrate these notions on a few examples.

Example 5.4. Let X and Y be the cones given by

X = {x ∈ Q 3 ≥0 | x(1) = x(3)} and Y = {x ∈ Q 3 ≥0 | x(1) = x(2) = x(3)}.
The vector (1, 0, 1) is reducible for both cones, since it contains only two non-zero components. The vector (1, 1, 1) is reducible for X. This is witnessed by the (1, 3)-decomposition (a, y, y) where a = (1, 0, 1) and y = (0, 0.5, 0). The same vector (1, 1, 1) is irreducible for Y . Theorem 5.5. A cone is nested if, and only if, it contains no irreducible vector.

Proof. Consider a cone X ⊆ Q d ≥0 . We first prove the "only if" direction of the theorem. Assume that X is nested, and let x ∈ X. If supp(x) has cardinality at most two, then x is trivially reducible. Suppose, on the contrary, that x contains at least three non-zero components. Since X ⊆ ı X, we obtain from Lemma 5.2 that there exists a nested binary relation R on supp(x) such that x ∈ X R . Moreover, R is not empty since x = 0. Let F denote the field 5 of R, and define s = min F and t = max F . Observe that both s and t are in supp(x). Notice also that t ≥ s + 2 since x contains at least three non-zero components. We derive from Lemma 5.1 that there exist a pivot p with s < p < t, a nested binary relation U on {s, . . . , p} and a nested binary relation V on {p, . . . , t}, such that R ⊆ {(s, t)} ∪ U ∪ V . We derive that x ∈ (X (s,t) + X U + X V ), which entails that x is reducible.

Let us now prove the "if" direction of the theorem. Assume that X is not nested. This means that X ⊆ ı X. Among the vectors x in X \ ı X, pick one such that supp(x) is minimal for inclusion. Let us show that x is irreducible. By contradiction, suppose that x is reducible. Observe that supp(x) has cardinality at least three since x ∈ (X \ ı X). Therefore, there exists a pair (s, t) of indices in supp(x), with 1 ≤ s ≤ t ≤ d, and an (s, t)-decomposition (a, y, z) such that x = a + y + z. It is readily seen that supp(y) and supp(z) are both strictly contained in supp(x). By minimality of x, we get that y and z are in ı X. We derive from Lemma 5.3 that x ∈ ı X, which contradicts the assumption that x is in X \ ı X.

The previous theorem allows us to reduce the cone nestedness problem to the question whether a given cone contains only reducible vectors. In the remainder of this section, we explain how to solve the latter problem in coNP. Consider a matrix A ∈ Z n×d encoded in binary, and let X = {x ∈ Q d ≥0 | Ax ≥ 0}. We build, in time polynomial in the size of A, a quantifier-free formula6 ρ(x) in FO (Q, 0, 1, +, ≤) that is valid if, and only if, X contains only reducible vectors. This will entail a coNP upper bound for the cone nestedness problem, since satisfiability of quantifier-free formulas in FO (Q, 0, 1, +, ≤) is solvable in NP (see, e.g., [21, p. 120]). First, we build a formula ϕ(x), containing quantifiers, whose models are precisely the vectors in X that are reducible. Let B be the the matrix in Z (n+d)×d obtained from A by appending the identity matrix to the bottom of

A. Note that X = {x ∈ Q d | Bx ≥ 0}. The formula ϕ(x) is: Bx ≥ 0 ∧ 1≤s≤t≤d   Ñ i ∈{s,t} x(i) = 0 é ∨ (x(s) > 0 ∧ x(t) > 0 ∧ ψ B,s,t (x))  
where, for each pair (s, t) of indices with 1 ≤ s ≤ t ≤ d, the formula ψ B,s,t (x), given below, expresses that there exists an (s, t)-decomposition (a, y, z) such that x = a + y + z. The formula ψ B,s,t (x) is:

i<s ∨ i>t x(i) = 0 ∧ t-1 p=s+1 ∃µ ∃ν ∃π           B(µe s + νe t ) ≥ 0 B Ñ s≤i<p x(i)e i -µe s + πe p é ≥ 0 B Ñ p≤i≤t x(i)e i -πe p -νe t é ≥ 0          
Here, it is understood that the sub-formula in brackets stands for the conjunction of the three systems of linear inequalities. It is routinely checked that, for every vector x ∈ Q d , the formula ϕ(x) holds if, and only if, x is a reducible vector of X.

Notice that each disjunct ∃µ∃ν∃π [• • • ] contains a constant number of quantifiers, namely three. So, with Fourier-Motzkin quantifier elimination, we can transform, in polynomial time, each formula ψ B,s,t (x) into an equivalent quantifier-free formula ψ B,s,t (x). Let ϕ (x) denote the formula obtained from the definition of ϕ(x) by replacing each ψ B,s,t (x) by ψ B,s,t (x). The desired formula ρ(x) is (Bx ≥ 0) ⇒ ϕ (x). We have shown the following theorem.

Theorem 5.6. The cone nestedness problem is solvable in coNP.

We now have all the necessary ingredients to prove the following corollary, which is the main technical result of the paper.

Corollary 5.7. The stratifiability problem for integral polyhedra is coNP-complete.

Proof. We start by recalling that the emptiness problem for integral polyhedra is coNP-complete (see, e.g., [21, p. 245]). This problem asks, given a matrix A ∈ Z n×d and a vector b ∈ Z d , both encoded in binary, whether the integral polyhedron {x ∈ N d | Ax ≥ b} is empty.

Let us now prove the corollary. The upper bound follows from Theorem 4.5, Theorem 5.6, and closure under union of coNP. The lower bound is obtained by reduction from the emptiness problem for integral polyhedra. First of all, we observe that by increasing d by 3 and by slightly modifying the pair (A, b), the emptiness problem for integral polyhedra can be reduced, in linear time, to the particular case of integral polyhedra X satisfying the following condition:

X = ∅ or {(x(1), x(2), x(3)) | x ∈ X} = N(1, 1, 1) (3)
Recall that the linear set N(1, 1, 1) is not stratifiable (see Example 3.5). It follows from Lemma 3.3 that every integral polyhedron satisfying (3) is empty if, and only if, it is stratifiable. We have thus reduced, in linear time, the emptiness problem for integral polyhedra to the stratifiability problem for them.

Application to Flat Counter Systems

In this section, we investigate the context-freeness problem for flat counter systems. This problem asks whether the trace language of a given counter system intersected with a given bounded regular language is context-free. In our setting, counter systems are a generalization of Petri nets where transitions are guarded by integral polyhedra. Such guards can express zero tests, so counter systems subsume Minsky machines and, therefore, are Turing-powerful. We show that the context-freeness problem for flat counter systems is coNP-complete, and remains so for flat Petri nets.

We exploit the restriction to bounded languages required by flatness to reduce the context-freeness problem for flat counter systems to the stratifiability problem for integral polyhedra. This reduction is performed in two steps. It is well-known that bounded regular languages are finite unions of languages of the form [START_REF] Ginsburg | Bounded regular sets[END_REF]. As a first step, we consider a subproblem of the context-freeness problem for flat counter systems, where the given bounded regular language is of the form w

w 1 σ + 1 • • • w d σ + d
1 σ + 1 • • • w d σ + d .
We provide a reduction of this subproblem to the stratifiability problem for integral polyhedra. The contextfreeness problem for flat counter systems is then reduced to this subproblem by providing polynomial bounds on the size of the languages w

1 σ + 1 • • • w d σ + d .
A counter system is a formal model manipulating a finite set of counters ranging over the natural numbers. Given a number of counters c ∈ N, a configuration is a vector x ∈ N c , and a transition is a triple θ = (A, b, v) where A ∈ Z m×c is a matrix, and b ∈ Z m and v ∈ Z c are two vectors. Informally, a transition (A, b, v) represents the guarded translation "Ax ≥ b ; x := x + v ; x ≥ 0". Formally, a counter system is a triple S = c, Θ, x init where c ∈ N is a number of counters, Θ ⊆ Z m×c × Z m × Z c is a finite set of transitions, and x init ∈ N c is an initial configuration. The operational semantics of S is given by the labeled

transition relation → ⊆ N c × Θ × N c , defined by x (A,b,v) -----→ y if Ax ≥ b and y = x + v.
A run is a finite, alternating sequence (x 0 , θ 1 , x 1 , . . . , θ k , x k ) of configurations and transitions, satisfying x i-1 θi -→ x i for all i. The word θ 1 • • • θ k is called the label of the run. We introduce, for every word σ ∈ Θ * , the binary relation σ -→ between configurations, defined by x σ -→ y if there exists a run from x to y labeled by σ. A trace from a configuration x is the label of some run that starts with x. We let T (S, x) denote the set of all traces from x. The set T (S, x init ) of all traces from the initial configuration, shortly written T (S), is called the trace language of S. The context-freeness problem for counter systems asks whether the trace language of a given counter system is context-free. This problem is easily shown to be undecidable, by reduction from the reachability problem for (deterministic) Minsky machines.

For the subclass of Petri nets, the context-freeness problem was shown to be decidable by Schwer in [START_REF] Schwer | The context-freeness of the languages associated with vector addition systems is decidable[END_REF]. In our settings, a Petri net is a counter system c, Θ, x init where Θ is a set of transitions of the form (A, b, v) such that A is the identity matrix. Informally, Petri net transitions are guarded translations "x ≥ b ; x := x + v ; x ≥ 0". In a recent paper [START_REF] Leroux | On the context-freeness problem for vector addition systems[END_REF], we revisited the contextfreeness problem for Petri nets, and gave a simpler proof of decidability based on bounded regular languages. We showed that the trace language of a Petri net is context-free if, and only if, it has a context-free intersection with every bounded regular language. Based on this characterization, the context-freeness problem for Petri nets was then shown to be ExpSpace-complete [START_REF] Leroux | A relational trace logic for vector addition systems with application to context-freeness[END_REF]. However, the complexity of the context-freeness problem for flat Petri nets was left open.

This motivates our study of the context-freeness problem for flat counter systems. Formally, we define this problem as follows:

Input: a counter system S = c, Θ, x init , and a finite-state automaton 7 A recognizing a bounded regular language L(A) ⊆ Θ * , Output: whether the language T (S) ∩ L(A) is context-free.

The size of the input is the obvious one, where integers are encoded in binary. In the sequel, this problem is reduced to a subproblem, called the context-freeness problem for flat-linear counter systems, which is defined as follows:

Input: a counter system S = c, Θ, x init , and a finite sequence w 1 , σ 1 , . . . , w d , σ d of words in Θ * , Output: whether the language T (S) ∩ w

1 σ + 1 • • • w d σ + d is context-free.
The size of the input is, again, the obvious one, with integers encoded in binary. The decidability of this last problem requires the following variant of Ginsburg's characterization of bounded context-free languages (cf. Theorem 3.4).

Remark 6.8. Our setting requires a single initial configuration. Let us consider a variant without any specific initial configuration. An uninitialized counter system is a pair S = c, Θ where c ∈ N is a number of counters and Θ is a finite set of transitions. Its trace language is defined by T (S) = xinit∈N c T (S, x init ). The context-freeness problem for uninitialized flat counter systems is defined exactly as the context-freeness problem for flat counter systems except that it takes an uninitialized counter system as input. This problem can be shown to be decidable by adapting techniques developed in this paper. In fact, just observe that the set N = {(n 1 , . . .

Conclusions and Future Work

The decidability of the stratifiability problem for semilinear sets was raised in [START_REF] Ginsburg | Semigroups, Presburger formulas and languages[END_REF][START_REF] Ginsburg | The Mathematical Theory of Context-Free Languages[END_REF] almost fifty years ago, and is still open. Rephrased in terms of languages, this decision problem is equivalent to the question whether a given semilinear bounded language is context-free. In this paper, we have shown that the stratifiability problem for the subclass of integral polyhedra is coNP-complete. Building on this result, we have then established that the context-freeness problem for flat counter systems is coNP-complete, and remains coNP-hard for the subcase of flat Petri nets.

To solve the stratifiability problem for integral polyhedra, we have reduced it to the particular case of integral cones. While the latter is in coNP, its exact complexity is open.

  Lemma 4.1 ([21, p. 237]). For every matrix A ∈ Z n×d and every vector b ∈ Z d , there exists two finite subsets B and P of N d such that:

Fig. 1 :

 1 Fig. 1: Decomposition of nested relations and of reducible vectors

, n d ) ∈ N d 1 | w 1 σ n1 1 •

 11 • • w d σ n d d ∈ T (S)} can be denoted by a Presburger formula ϕ(n 1 , . . . , n d ) = ∃x init A(x init , n 1 , . . . , n d ) ≥ b for a matrix A and a vector b that are both computable in polynomial time. Decidability of the context-freeness problem for uninitialized flat counter systems follows by quantifier elimination on ϕ. However, the complexity is open.

This work was supported by the ANR project ReacHard (ANR-11-BS02-001).

Recall that supp(v) denotes the support of v, i.e, the set of indices i with v(i) = 0.

This notion is defined relative to a cone X, which is left implicit to reduce clutter.

The field of a binary relation is the union of its domain and range.

In this paper, we assume that all integer constants in formulas are encoded in binary.

Recall that a finite-state automaton is a quintuple A = Q, I, F, Σ, → where Q is a finite set of states, I ⊆ Q and F ⊆ Q are finite sets of initial and final states, Σ is a finite alphabet, and → ⊆ Q × Σ × Q is a finite set of transitions. We let L(A) denote the language recognized by A.

The context-freeness problem for flat Petri nets is defined exactly as the contextfreeness problem for flat counter systems except that the input counter system is required to be a Petri net.

Lemma 6.1. Consider a language L ⊆ w 1 σ + 1 • • • w d σ + d , where each w i ∈ Σ * and each σ i ∈ Σ * . Then L is context-free if, and only if, the set of all vectors (n 1 , . . . , n d ) in

L is a stratifiable semilinear set. The context-freeness problem for flat-linear counter systems is shown to be decidable in coNP by a polynomial-time reduction to the stratifiability problem for integral polyhedra, which is solvable in coNP by Corollary 5.7. Let us consider an input of this problem, namely a counter system S = c, Θ, x init and a finite sequence w 1 , σ 1 , . . . , w d , σ d of words in Θ * . By Lemma 6.1, the language

, and only if, the following set is stratifiable:

This set is shown to be an integral polyhedron in Corollary 6.3. This result follows from the following "acceleration" lemma.

Lemma 6.2. There exists a polynomial-time algorithm that, given a counter system S = c, Θ, x init and a word σ ∈ Θ * , computes a matrix A ∈ Z n×c and three vectors a, b ∈ Z n and v ∈ Z c such that:

Proof (sketch). By encoding the effect of a word σ ∈ Θ * into a single transition, we deduce the lemma thanks to [START_REF] Bardin | Fast: acceleration from theory to practice[END_REF]. The crucial observation is the convexity of the guard of this transition.

Corollary 6.3. There exists a polynomial-time algorithm that, given a counter system S = c, Θ, x init and a sequence w 1 , σ 1 , . . . , w d , σ d of words in Θ * , computes a matrix A ∈ Z n×d and a vector b ∈ Z n such that:

Proof. We derive in polynomial time from Lemma 6.2, a tuple

such that for every n ∈ N 1 and any x, y ∈ N c we have x

and only if,

, and only if, the following linear system is satisfiable where y i = x init + 1≤j<i (u j + n j v j ) and

Now, just observe that such a linear system can be written as a linear system of the form A(n 1 , . . . , n d ) ≥ b.

We deduce the following theorem. Theorem 6.4. The context-freeness problem for flat-linear counter systems is coNP-complete.

Proof. Since the language L is context-free if, and only if, the integral polyhedron N is stratifiable, it follows from Corollary 5.7 that the context-freeness problem for flat-linear counter systems is in coNP. The problem is shown to be coNP-hard by a direct reduction from the stratifiability problem for integral polyhedra, which is coNP-hard by Corollary 5.7.

The context-freeness problem for flat counter systems can be reduced to the flat-linear case thanks to the following lemma, which provides polynomial bounds on the decomposition of bounded regular languages into languages of the form Now, consider an instance (S, A) of the context-freeness problem for flat counter systems. Recall that L(A) is bounded. We derive from the previous Lemma that T (S) ∩ L(A) is not context-free if, and only if, there exists an accepting run q 0

d can be checked in NP, we obtain that the context-freeness problem for flat counter systems is in coNP. A matching lower bound is obtained by reduction from 3-Sat. Lemma 6.6. The context-freeness problem for flat Petri nets 8 is coNP-hard.

Proof (sketch). Given a 3-Sat formula ϕ, an instance (S, A) of the contextfreeness problem for flat Petri nets is computed in polynomial time in such a way that the language T (S) ∩ L(A) is non-empty, and in this case not context-free, if, and only if, the formula ϕ is satisfiable. Since 3-Sat is NP-hard, the contextfreeness problem for flat Petri nets is coNP-hard.

We have shown the following theorem, which is the second main result of the paper.

Theorem 6.7. The context-freeness problem for flat counter systems is coNPcomplete, and remains so for flat Petri nets.


J Leroux

Ph Schnoebelen

On Functions Weakly Computable by Petri Nets and Vector Addition Systems

We show that any unbounded function weakly computable by a Petri net or a VASS cannot be sublinear. This answers a long-standing folklore conjecture about weakly computing the inverses of some fast-growing functions. The proof relies on a pumping lemma for sets of runs in Petri nets or VASSes.

Introduction

Petri nets (PN), Vector Addition Systems (VAS) and Vector Addition Systems with States (VASS) are essentially equivalent computational models based on simple operations on positive integer counters: decrements and increments. Such systems can be used to compute number-theoretical functions, exactly like with Minsky machines or Turing machines. However, they cannot compute all recursive functions since they are less expressive than Minsky machines. In particular they lack zero-tests, or, more precisely, they cannot initiate a given action on the condition that a counter's value is zero, only on the condition that it is not zero.

The standard definition for a function computed by a Petri net or a VASS is due to Rabin and is called "functions weakly computable by a Petri net", or just "WCPN functions" (all definitions will be found in the following sections). This notion has been used since the early days of Petri nets and has proved very useful in hardness or impossibility proofs: The undecidability of equivalence problems for nets and VASSes, and the Ackermann-hardness of the same problems for bounded systems, have been proved using the fact that multivariate polynomials with positive integer coefficients -aka positive Diophantine polynomials-and, respectively, the fast-growing functions (F i ) i∈N in the Grzegorczyk hierarchy, are all WCPN [START_REF] Hack | The equality problem for vector addition systems is undecidable[END_REF][START_REF] Mayr | The complexity of the finite containment problem for Petri nets[END_REF][START_REF] Jančar | Nonprimitive recursive complexity and undecidability for Petri net equivalences[END_REF].

The above results rely on showing how some useful functions are WCPN. But not much is known about exactly which functions are WCPN or not. It is known that all WCPN functions are monotonic. They are all primitive-recursive. The class of WCPN functions is closed under composition. A folklore conjecture states that the inverses of the fast-growing functions are not WCPN. It is stated as fact in [30, p.252] but no reference is given. In this paper, we settle the issue by proving that if f : N → N is WCPN and unbounded then it is in Ω(x), i.e., f (x) eventually dominates c • x for some constant c > 0. Thus any function that is sublinear, like x → √ x , or x → log x , are not WCPN. In particular, this applies to the inverse F -1 i of any fast-growing function with i ≥ 2. The proof technique is interesting in its own right: it relies on a pumping lemma on sets of runs in VASSes or Petri nets.

Work supported by the ReacHard project, ANR grant 11-BS02-001-01.

Beyond Petri nets and VASSes. Petri nets and VASSes are a classic example of wellstructured systems [START_REF] Abdulla | Algorithmic analysis of programs with well quasi-ordered domains[END_REF][START_REF] Finkel | Well-structured transition systems everywhere![END_REF]. In recent years, weakly computing numerical functions has proved to be a fundamental tool for understanding the expressive power and the complexity of some families of well-structured systems that are more powerful than Petri nets and VASSes [START_REF] Ph | Revisiting Ackermann-hardness for lossy counter machines and reset Petri nets[END_REF][START_REF] Haddad | The ordinal-recursive complexity of timed-arc Petri nets, data nets, and other enriched nets[END_REF][START_REF] Ch | The power of priority channel systems[END_REF]. For such systems, the hardness proofs rely on weakly computing fast-growing functions (F α ) α∈Ord that extend Grzegorczyk's hierarchy. These hardness proofs also crucially rely on weakly computing the inverses of the F α 's.

There are several extensions of Petri nets for which reachability (or coverability or termination) remains decidable: pushdown VASSes [START_REF] Leroux | Hyper-Ackermannian bounds for pushdown vector addition systems[END_REF], nets with nested zerotests [START_REF] Reinhardt | Reachability in Petri nets with inhibitor arcs[END_REF], recursive VASSes [START_REF] Bouajjani | Analysis of recursively parallel programs[END_REF] and Branching VASSes [START_REF] Demri | The covering and boundedness problems for branching vector addition systems[END_REF], VASSes with pointers to counters [START_REF] Demri | Reasoning about data repetitions with counter systems[END_REF], etc. In many cases, it is not known how these extensions compare in expressive power and in complexity. We believe that weakly computable functions can be a useful tool when addressing theses questions.

Outline of the paper. Section 2 recalls the standard definitions for VASSes and fixes some notations. Section 3 recalls the definitions for WCPN functions and the classic results about them. Our main result is proved in Section 4.

Vector Addition Systems with States

Following Hopcroft and Pansiot [START_REF] Hopcroft | On the reachability problem for 5-dimensional vector addition systems[END_REF], we adopt Vector Addition Systems with States (VASS) as our mathematical setting (rather than Petri nets or plain VASes) because they offers a good compromise between ease of description for specific systems, and convenient mathematical notation for reasoning about them. Nevertheless, all these models are essentially equivalent for our purposes.

Vectors of integers. Z and N denote the sets of integers and, resp., non-negative integers. For d ∈ N, a d-dimensional vector is a tuple a = a 1 , . . . , a d in Z d . We use 0 to denote 0, . . . , 0 when the dimension is understood. Vectors can be concatenated: for a ∈ Z In the following, we reserve x, y, . . . for vectors in N d and write x , y , . . . , for their norms, defined by x 1 , . . . , x

d def = x 1 + • • • + x d .
VASSes and their operational semantics. A VASS is a triple A = d, Q, T where d ∈ N is a dimension (i.e., a number of counters), Q is a non-empty finite set of (control) locations, and T ⊆ Q × Z d × Q is a finite set of (transition) rules. We usually write q, q , . . . for locations, and t, u, . . . for rules.

Fix some VASS A = d, Q, T . The operational semantics of A is given in the form of a transition system (Conf , -→). Formally, Conf Steps are defined by (q, x) a -→ (q , y) def ⇔ (q, a, q ) ∈ T ∧ y = x + a. The a vector in a rule (q, a, q ) is called a translation. Graphical description. It is convenient to present VASSes in graphic form. See an example in Fig. 1. Here the locations and rules are depicted as a directed graph, as is standard with such automata-theoretical notions. Indeed, we see a d-dim VASS as being an automaton acting on d registers, or counters, capable of storing a natural number. These counters are named in our graphical depictions (see x and z in Fig. 1) so that we may use programming languages notations for the translation a in a rule (q, a, q ). For example, in Fig. 1, the loop labeled with "x--;x--;z++" is a rule (q 2 , a, q 2 ) with a = -2, 1 , the other rule being (q 1 , 0, q 2 ). Runs and reachability. For k ∈ N, a length-k run from c to c is a sequence ρ of the form c 0 a 1 c 1 • • • a k c k that alternates between configurations and vectors and such that c 0 = c, c k = c , and c i-1 ai -→ c i for all i = 1, . . . , k. For a run ρ as above, we let src(ρ) and tgt(ρ) denote c 0 and, respectively, c k . We write c * -→ c when there is a run ρ from c to c , in which case we say that c is reachable from c.

Continuing our previous example, the reachability relation for the VASS from Fig. 1 can be captured 3 with the following:

(q i , x, z) * - → (q j , x , z ) iff 0 ≤ x -x = 2(z -z) if j = 2, or x = x ∧ z = z if i = j = 1. (1)
Lifting steps and runs. It is well known and easy to see that steps can be lifted up by vectors z ∈ N d . For a configuration c = (q, x), we write c + z for the configuration (q, x + z).

c a - → c implies c + z a - → c + z , (2)
c * - → c implies c + z * - → c + z . (3)

Weakly Computable Functions

In this section we recall the classic notion of weak PN computers and weakly computable functions. We recall the main known results, most of them from the 70's or early 80's, when the applications were limited to a few hardness or impossibility proofs. This material is classic but has been partly forgotten.

As we argued in the introduction, the notion of weakly computable functions has recently gained new relevance with the development of well-structured systems that go beyond Petri nets and VASSes in expressive power, while sharing some of their characteristics. In particular, we expect that it will help understanding the expressive power of extensions like VASSes with nested zero-tests [START_REF] Reinhardt | Reachability in Petri nets with inhibitor arcs[END_REF] or with a pushdown stack [START_REF] Leroux | Hyper-Ackermannian bounds for pushdown vector addition systems[END_REF].

Weak PN Computers and Weakly Computable Functions

The expected way for a finite-state register machine A to compute a numerical function f : N → N is to start in some initial location with some input value n stored in a designated input counter and from that configuration eventually reach a final or accepting location with f (n) in a designated output counter. In order for A to be correct, it should be impossible that it reaches its accepting location with a value differing from f (n) in the output counter. In that case, we say that A strongly computes f . This notion of correctness is fine with Minsky machines but it is too strong for VASSes and does not lead to an interesting family of computable functions. In fact, Petri nets and VASSes are essentially nondeterministic devices, and the above notion of strongly computing some function does not accommodate nondeterminism nicely.

With this in mind, Rabin defined a notion of "weakly computing f " that combines the following two principles:

Completeness: For any n ∈ N, there is a computation with input n and output f (n); Safety: Any computation from input n to some output r satisfies r ≤ f (n).

This leads to our first definition: Definition 3.1 (Weak PN computers). Let f : N n → N m be a total function. A weak PN computer for f is a d-dimensional VASS A, with d ≥ n + m and two designated locations q init and q final , that satisfies the following two properties. Here we write for d -n -m, and we decompose vectors w ∈ N d as concatenations w = x, y, z where

x ∈ N n , y ∈ N and z ∈ N m . ∀x : ∃x , y : (q init , x, 0, 0) * - → (q final , x , y , f (x)) , (CO) ∀x, x , y , z : (q init , x, 0, 0) * - → (q final , x , y , z ) implies z f (x) . (SA)
We say that f is weakly computable, or WCPN for short, if there is a weak PN computer for it.

For convenience, Definition 3.1 assumes that the (n-dimensional) input is given in the first n counters of A, and that the m-dimensional result is found in its last m counters. Note that A may use its extra counters for auxiliary calculations.

Example 3.2 (A weak computer for halving). The VASS from Fig. 1 is a weak computer for f : x → x 2 . We just have to designate q 1 and q 2 as the required q init and, resp., q final . To show that (CO) and (SA) hold, one sets z = 0 in Eq. ( 1). This gives

(q 1 , x, 0) * - → (q 2 , x , z ) iff z = x -x 2 ,
entailing both (CO) -pick x = (x mod 2)and (SA) -since z , x ∈ N-in one go.

Only monotonic functions can be weakly computed in the above sense. This is an immediate consequence of the monotonicity of steps in VASSes (see Fact 2.1).

Proposition 3.3 (Monotonicity of WCPN functions). If f : N n → N m is WCPN then x x implies f (x) f (x ).
Proof. Assume that x x and pick any weak PN computer for f . By (CO), there is a run (q init , x, 0, 0) * -→ (q final , v, y, f (x)). By Eq. ( 3), there is also a run (q init , x , 0, 0) * -→ (q final , v + xx, y, f (x)). Thus f (x) f (x ) by (SA).

More weakly computable functions

Example 3.4 (A weak computer for multiplication, from [START_REF] Müller | Weak Petri net computers for Ackermann functions[END_REF]). Fig. 2 describes A × , a weak computer for f :

x 1 , x 2 → x 1 × x 2 .
To show that (SA) holds, we associate with any configuration c of A × a value M (c) ∈ N given by

M (q, x 1 , x 2 , y, z) def = z + (x 1 + y) • x 2 + y if q = q 2 , z + (x 1 + y) • x 2 otherwise. ( 4
)
By considering all rules of A × in turn, one checks that c -→ c implies M (c) ≥ M (c ). Thus given an arbitrary run from c 0 = (q init , x 1 , x 2 , 0, 0

) to c k = (q final , x 1 , x 2 , y , z ) it holds that M (c 0 ) ≥ M (c k ), i.e., x 1 • x 2 ≥ z + x 1 • x 2 + y • x 2 . This entails z ≤ x 1 • x 2 as required by (SA).
We let the reader check that (CO) holds. [Hint: steps c -→ c that only use the rule from q 1 to q 2 when x 1 = 0, and from q 2 to q 1 when y = 0, satisfy M (c) = M (c ).]

Weakly computing functions has mainly been used in hardness or impossibility proofs. For example, weakly computing multiplication can be used to show that reachability sets are not always semilinear: it is easy to adapt the construction underlying A × and design a VASS that, starting from a fixed c 0 , generates the set of triples { y 1 , y 2 , y ∈ N 3 | 0 ≤ y ≤ y 1 • y 2 } in some designated counters. The reachability set of this VASS cannot be semilinear. Proof (Idea). The obvious way of gluing a weak PN computer for g after a weak PN computer for f produces a weak PN computer for g • f . To prove that the resulting VASS satisfies (SA), one observes that any run can be reordered by firing all rules in the f part before the rules in the g part.

Since the class of WCPN functions contains addition, multiplication, projections, and tuplings, one deduces that all positive Diophantine polynomials (multivariate polynomials with coefficients in N) are weakly computable. This was used by Rabin in his reduction of Hilbert's 10th Problem to the inclusion problem for VASS reachability sets [START_REF] Baker | s proof of the undecidability of the reachability set inclusion problem of vector addition systems[END_REF][START_REF] Hack | The equality problem for vector addition systems is undecidable[END_REF]. Hack strengthened this reduction to show that already the equality problem was undecidable [START_REF] Hack | The equality problem for vector addition systems is undecidable[END_REF]. (Later, Jančar showed that all behavioural equivalences are undecidable for VASSes -already for dimension d = 5-, using a simpler reduction with some notion of weak computer that is not numerical [START_REF] Jančar | Undecidability of bisimilarity for Petri nets and some related problems[END_REF].)

Iterable weak PN computers

There are other easy and useful examples of WCPN functions that are not positive Diophantine polynomials, like min and max, or even half seen previously. In order to show the weak computability of more functions, in particular functions that are not polynomially or exponentially bounded, Mayr [START_REF] Mayr | The complexity of the finite containment problem for Petri nets[END_REF] introduced the following notion: Definition 3.6 (Iterable Weak PN Computers). Let f : N → N be a weakly computable unary function. A weak PN computer A for f is iterable if it satisfies ∀w, w :(q init , w) * -→ (q final , w ) implies w ≤ f ( w ) .

(IT)

A unary function is iterably weakly computable, or IWCPN, if there exists an iterable weak PN computer for it.

In Definition 3.6, w counts all the tokens (using Petri net terminology) in the starting configuration. The property stated by Eq. (IT) is useful in constructions that include A and where one cannot guarantee that all computations by A will start from clean configurations with zeroes in y and z.

Example 3.7 (Halving). The weak PN computer for halving (Fig. 1) is not iterable since, by Eq. ( 1), it has runs like (q init , 0, 1) * -→ (q final , 0, 1) and (q init , 1, 0) * -→ (q final , 1, 0) that have w = w = 1, hence w ≤ f ( w ) = 1 2 = 0. In fact, it is impossible to design an iterable weak PN computer for halving, as a consequence of the following proposition.

Proposition 3.8 (Strict Monotonicity of IWCPN functions). If

f : N → N is IWCPN then f (x) < f (x + 1) for all x ∈ N.
Proof. Assume a given iterable weak PN computer for f and let x ∈ N. From (CO), we derive (q init , x, 0, 0) * -→ (q final , x , y , f (x)). By lifting, we get (q init , x + 1, 0, 0) * -→ (q final , x + 1, y , f (x)). Now (IT) gives x + 1 + y + f (x) ≤ f (x + 1), which entails f (x) < f (x + 1).

Example 3.9 (Doubling is IWCPN). One may design an iterable weak computer for qinit qfinal

x--;z++;z++

0 z 4 x Fig. 3. A dbl , a VASS weakly computing x → 2 • x.
x → 2 • x (doubling) by a slight modification of Fig. 1. The resulting VASS, called A dbl , is depicted in Fig. 3. It satisfies

(q init , x, z) * - → (q final , x , z ) iff 0 ≤ 2(x -x ) = z -z .

These runs have thus

w = x + z = 2x -x + z. On the other hand f ( w ) = f (x + z) = 2x + 2z. Hence w ≤ f ( w ) as required by (IT).
As expected, the functions weakly computed by iterable weak PN computers are iterable. Given a unary f and some n ∈ N, we write f n (x) for the n-fold application f (f (f (• • • (x) • • • ))) of f . In particular f 0 (x) = x. One can then show the following: Proposition 3.10 ( [START_REF] Mayr | The complexity of the finite containment problem for Petri nets[END_REF][START_REF] Müller | Weak Petri net computers for Ackermann functions[END_REF]). If f is IWCPN, then iter (f ) : x, y → f x (y) is IWCPN.

Indeed, the whole point of (IT) is to entail the correctness of the obvious construction for iterating a weak PN computer.

With Proposition 3.10, and since doubling is IWCPN, we deduce that iter (dbl ) :

x, y → dbl x (y) = 2 x y is IWCPN. From that we deduce that tower : x → 2 2 ••• 2 x times is IWCPN. Continuing, all the fast-growing functions (F i ) i∈N in the Grzegorczyk hierarchy are IWCPN. This was used by Mayr to show that the inclusion problem for finite reachability sets is not primitive recursive [START_REF] Mayr | The complexity of the finite containment problem for Petri nets[END_REF][START_REF] Mayr | The complexity of the finite containment problem for Petri nets[END_REF]. The problem is in fact F ωcomplete in the recent classification of Schmitz [START_REF] Schmitz | Complexity hierarchies beyond elementary[END_REF]. Using the same IWCPN functions, Jančar showed that all behavioural equivalences are Ackermann-hard between bounded VASSes [START_REF] Jančar | Nonprimitive recursive complexity and undecidability for Petri net equivalences[END_REF].

While the fast-growing hierarchy extends beyond the (F i ) i∈N , the functions at the higher levels -starting with F ω which is one possible form for Ackermann's functionare not WCPN. The following Proposition is folklore, but we could not find it explicitly stated in the literature: Proposition 3.11. Any weakly computable function f is primitive recursive.

Proof. For a VASS A and a starting configuration c 0 ∈ Conf , let S A (c 0 ) ∈ N be the maximum norm of a configuration occurring in the Karp-Miller tree T KM (c 0 ) rooted in c 0 . (We assume familiarity with Karp-Miller trees, otherwise see []. Note that they really contain "extended configurations" in Q × (N ∪ {ω}) d but one only uses the finite values for their norm, as in, e.g., (q, 7, ω, 2) = 7 + 2 = 9.)

For k ∈ N, let now S A (n) def = max {S A (c) | c ≤ k}.
It is shown in [10, Section 7C] that S A : N → N is primitive recursive (using a different norm for vectors, but this is of no consequence here). If now A is a weak PN computer for some f : N n → N m , then by (CO) and for any x ∈ N n , the tree T KM ((q init , x, 0, 0)) contains an extended configuration c x = (q final , x , y , z ) that covers (q final , 0, 0, f (x)) since every reachable configuration is covered in T KM . Furthermore, by (SA), no configuration reachable in q final can have values above f (x) in the last m counters. Hence the z part of c x has no ω's and z = f (x). Finally, one can compute f (x) by building a Karp-Miller tree of size that is primitive recursive in x and by reading f (x) on one of its leaves.

Alternative Definitions

The literature contains other proposals for a notion of weakly computable functions, all of them based on Rabin's seminal idea. For example, it is possible -as in [START_REF] Hack | The equality problem for vector addition systems is undecidable[END_REF]-to define the function weakly computed by A as the maximum number of times a transition (or all transitions, as in [START_REF] Hack | Decidability Questions for Petri Nets[END_REF]) can be fired between (q init , x, 0) and q final . This does not give a larger class of weakly computable functions.

In the rest of this section, we discuss alternative notions that lead to larger families of functions.

Weakly Computing

Eagerly. An interesting notion is that of "eagerly" weakly computable functions. For this, we modify the Correctness and Safety requirement in Definition 3.1, replacing them with ∀x : (q init , x, 0, 0) * -→ (q final , 0, 0, f (x)) , (CO') ∀x, z : (q init , x, 0, 0) * -→ (q final , 0, 0, z ) implies z f (x) , (SA') and we say that f is EWCPN.

The idea here is that A must consume inputs and auxiliary counters at the end of the computation. This is meaningful in some reductions -e.g., reducing reachability in VASSes to some problem on some weakly computable function-. To the best of our knowledge, it has never been considered in the literature on VASSes and Petri nets. The fact is that it does not behave as nicely as the classical definition (see below). However, it is a natural option with some extensions like VASSes extended with resets as in [START_REF] Araki | Some decision problems related to the reachability problem for Petri nets[END_REF][START_REF] Dufourd | Reset nets between decidability and undecidability[END_REF], or with nested zero-tests as in [START_REF] Reinhardt | Reachability in Petri nets with inhibitor arcs[END_REF]. Fact 3.12 The class of EWCPN functions strictly extends the WCPN functions.

Proof. Obviously, any WCPN function can be computed eagerly: a weak PN computer for f is made eager by adding decrementing rules that can empty the input and auxiliary counters. To see that the extension is strict, note that EWCPN functions are not always monotonic. For example, parity : x → x mod 2 is easily seen to be EWCPN.

Because EWCPN functions are not necessarily monotonic, it is not clear whether the composition of two EWCPN functions is EWCPN itself. In the next section we prove our main result even for the larger class of EWCPN functions.

Families of Weak PN Computers. Very often reductions showing hardness do not need a fixed weak PN computer for some f . They can accommodate a family (A i ) i∈N such that each A i weakly computes f (i), or f (x) for all x = 0, . . . , i. The family needs to be simple in computational terms -typically "polynomial-time uniform"so that it can be used in reductions. Since the A i 's that weakly compute the fast-growing F i 's are uniformly generated, they provide a family weakly computing the function F ω (equivalently, Ackermann's function) defined by F ω (x) = F x (x).

For slow-growing functions, one often needs a family that is polynomial-time uniform in the size of f (x). A recent example is Lazić's polynomial-time uniform family of pushdown VASSes (VASSes extended with a stack) that weakly computes the inverse

of tower : x → 2 2 ••• 2 x times [21].

Well-Quasi-Ordering Runs in VASSes

Recall that a quasi-order (qo) on a set S is a binary relation on S that is reflexive and transitive. A partial order is an antisymmetric quasi-order. A well-quasi-order (wqo) on S is a quasi-order such that every infinite sequence s 0 , s 1 , s 2 , . . . in S contains an increasing pair s i s j for some i < j. See [START_REF]The theory of well-quasi-ordering: A frequently discovered concept[END_REF] or [START_REF] Schmitz | Algorithmic aspects of WQO theory[END_REF] for more on wqos.

Example 4.1. It is well-known that (N, ≤) is a wqo, while (Z, ≤) or (Q ≥0 , ≤) are not. As another example, the pigeonhole principle shows that the partial order (S, =) is a wqo if, and only if, S is finite.

In practice, many wqos are defined by applying well-known constructions on standard, already known, wqos.

(s 1 , . . . , s n ) × (s 1 , . . . , s n ) def ⇔ s 1 1 s 1 ∧ . . . ∧ s n n s n .
It is well-known that (S × , × ) is a wqo if all (S i , i ) are. This last result is standardly called Dickson's Lemma, after Dickson's proof of his "Lemma A" in [START_REF] Dickson | Finiteness of the odd perfect and primitive abundant numbers with n distinct prime factors[END_REF], showing in essence that any subset of N d has finitely many minimal elements. For our purpose, Dickson's Lemma shows that (N d , ) is a wqo. Definition 4.3 (Sequence extensions of wqos and Higman's Lemma). The sequence extension (S * , * ) of a qo (S, ) has for its support the set S * of all finite sequences s 1 • • • s k over S, and these sequences are ordered by

s 1 • • • s k * s 1 • • • s def ⇔ there are indexes 1 ≤ n 1 < • • • < n k ≤ such that s 1 s n1 ∧ • • • ∧ s k s n k .
It is well-known that (S * , * ) is a wqo if (S, ) is. This last result is called Higman's Lemma.

In the rest of this section, we assume a fixed VASS A = (d, Q, T ). We now define three orderings, respectively between the configurations of A, between its steps, and between its runs, in the following way:

(q 1 , x 1 ) (q 2 , x 2 ) def ⇔ q 1 = q 2 ∧ x 1 x 2 , (5)
(c 1 a1 -→ c 1 ) (c 2 a2 -→ c 2 ) def ⇔ c 1 c 2 ∧ a 1 = a 2 ∧ c 1 c 2 . (6)
Since Q and T are finite, (Q, =) and (T, =) are wqos, hence (Conf , ) and (Conf × T × Conf , ) are wqos by Dickson's Lemma.

Definition 4.4 (Ordering runs, see Fig. 4). For two runs ρ, ρ of A, we write ρ ¢ ρ if ρ = c 0 a 1 c 1 . . . a k c k and ρ can be factored as some ρ = ρ 0 a 1 ρ 1 . . . a k ρ k where, for all j = 0, . . . , k, the ρ j factor is a run such that c j src(ρ j ) and c j tgt(ρ j ).

Lemma 4.5. The relation ¢ is a wqo over the runs of A.

Proof. This is essentially [START_REF] Leroux | Vector addition systems reachability problem (a simpler solution)[END_REF]Lemma 4.1] or [START_REF] Jančar | Decidability of a temporal logic problem for Petri nets[END_REF]Theorem 6.5]. A more direct proof is by observing that

ρ ¢ ρ iff src(ρ) src(ρ ) ∧ tgt(ρ) tgt(ρ ) ∧ (c 0 a1 -→ c 1 )(c 1 a2 -→ c 2 ) • • • (c k-1 a k -→ c k ) * (c 0 a 1 -→ c 1 ) • • • (c -1 a -→ c ) ,
where * is the sequence extension of the ordering of steps defined with Eq. ( 6). Since (over steps) and (over configurations) are wqos, ¢ is a wqo over the runs of A.

The ordering on runs comes with the following Pumping Lemma 4.7:

Lemma 4.6. Let c ∈ Conf and u, v ∈ N d . Then c + u * - → c + v implies ∀x ∈ N : c + x • u * - → c + x • v . (7)
Proof. From c+u * -→ c+v and with Eq. (3) one obtains c+u+iu+jv * -→ c+iu+v+jv for any i, j ∈ N. Chaining such runs yields Proof. In [START_REF] Jančar | Decidability of a temporal logic problem for Petri nets[END_REF]Lemma 6.7], it is proved that if ρ ¢ ρ ¢ ρ r for some run ρ x , then there exists a run ρ x+1 such that ρ x ¢ ρ x+1 , src(ρ x+1 ) = src(ρ x ) + u, and tgt(ρ x+1 ) = tgt(ρ x ) + v. An immediate induction over x ∈ N, starting with ρ 0 = ρ and ρ 1 = ρ provides a run ρ x witnessing src(ρ)

c + xu * - → c + (x -1)u + v * - → c + (x -2)u + 2v * - → • • • * - → c + xv .
+ x • u * - → tgt(ρ) + x • v.
We provide a direct proof of Lemma 4.7 as follows. Assume that ρ ¢ ρ is witnessed by factoring ρ of the form ρ 0 a 1 ρ 1 . . . a k ρ k . For j = 0, . . . , k, write u j and v j for the vectors in N d such that src(ρ j ) = c j + u j and tgt(ρ j ) = c j + v j . Since there is a run ρ j of the form c j + u j * -→ c j + v j , by Lemma 4.6 there is also

c j + x • u j * - → c j + x • v j for all x ∈ N.
For j = 1, . . . , k, u j = v j-1 + a j , since there are steps c j-1 aj -→ c j and c j-

1 + v j-1 = tgt(ρ j-1 ) aj -→ src(ρ j ) = c j + u j , we conclude that u j = v j-1 . Hence c j-1 aj -→ c j can be lifted to c j-1 + x • v j-1 aj -→ c j + x • u j . Chaining these runs give c 0 + x • u * - → c k + x • v as required.
Theorem 4.8. Let f : N → N be an unbounded unary EWCPN function. Then there exist r, s ∈ N with s > 0 and such that f (r + s • x) is in Ω(x).

Proof. Fix an eager weak PN computer A for f . For every r ∈ N, A has a run ρ r of the form (q init , r, 0, 0) * -→ (q final , 0, 0, f (r)). Since f is unbounded, there exists an infinite subset R ⊆ N such that (f (r)) r∈R is strictly increasing. Since the runs are well-ordered by ¢ (Lemma 4.5) there exists two indexes r < r in R such that ρ r ¢ ρ r . By introducing s = r -r, Lemma 4.7 shows that for every x ∈ N, we have q init , r + s • x, 0, 0 * -→ q final , 0, 0, f (r) + x • f (r ) -f (r) .

With (SA'), we deduce that f (r + s • x) ≥ f (r) + x • [f (r ) -f (r)] for every x ∈ N. The lemma follows from f (r ) -f (r) > 0.

Corollary 4.9. Let f : N → N be an unbounded unary WCPN function. Then f (x) is in Ω(x).

Proof. Direct from Theorem 4.8 since, by Proposition 3.3, f is non-decreasing.

Thus any sublinear function like x → √ x or x → log x is not weakly computable even in the eager sense. (We note that any monotonic bounded function is WCPN, e.g., as a max of finitely many threshold functions of the form "x → if u x then v hi else v lo " with v lo v hi .) Corollary 4.9 can be extended beyond unary functions as follows. A function f : N n → N is said to be unbounded on a component i, with 1 ≤ i ≤ n, if, for some natural numbers r 1 , . . . , r i-1 , r i+1 , . . . , r n ∈ N, the following unary function is unbounded:

x → f (r 1 , . . . , r i-1 , x, r i+1 , . . . , r n ).

For example, (x 1 , x 2 ) → x 1 is a WCPN function that is unbounded on the first component. From Corollary 4.9, and the monotonicity property given by Proposition 3.3, it follows that every WCPN function f : N n → N has f (x 1 , . . . , x n ) in Ω(max i∈I x i ), where I is the set of unbounded components for f .

Concluding Remarks

We proved that Petri nets and VASSes cannot weakly compute numerical functions that are sublinear. This was a folklore conjecture that, to the best of our knowledge, had not yet been settled.

Traditionally, weakly computable functions have been used to prove hardness results. Recent hardness proofs for well-structured systems crucially rely on the ability to weakly compute both fast-growing and slow-growing functions. For Petri nets and VASSes, our negative result is consistent with the current situation where, for the reachability problem, no lower bounds above EXPSPACE are known. This lack of expressive power is also consistent with the fact that all WCPN functions can already be weakly computed by the Lossy VASSes of [START_REF] Bouajjani | Model checking lossy vector addition systems[END_REF].

Our negative result raises the question of whether more functions can be weakly computed in extensions of VASSes like the pushdown VASSes of [START_REF] Leroux | Hyper-Ackermannian bounds for pushdown vector addition systems[END_REF] or the nets with nested zero-tests of [START_REF] Reinhardt | Reachability in Petri nets with inhibitor arcs[END_REF].

  d and b ∈ Z d we may write a, b for the vector a 1 , . . . , a d , b 1 , . . . , b d ∈ N d+d . Vectors in Z d are ordered with a = a 1 , . . . , a d b = b 1 , . . . , b d def ⇔ a 1 ≤ b 1 ∧ • • • ∧ a d ≤ b d , and can be added with (a + b) def = a 1 + b 1 , . . . , a d + b d . Note that (Z d , +, 0) is a commutative monoid, having (N d , +, 0) as submonoid. Clearly, a ∈ N d iff 0 a. By Dickson's Lemma, (N d , ) is a well-ordering (more details in Section 4).

def=

  Q × N d is the set of configurations, with typical elements c, c , . . . The labeled transition relation -→ ⊆ Conf × Z d × Conf is a set of triples (c, a, c ) called steps. As is standard, we write c a -→ c rather than (c, a, c ) ∈-→.

Fig. 1 .

 1 Fig. 1. A VASS depicted as an automaton acting on counters.

Fact 2 . 1 (

 21 Lifting steps and runs) For all c, c ∈ Conf , a ∈ Z d , and z ∈ N d :

Fig. 2 .

 2 Fig. 2. A×, a VASS weakly computing x1, x2 → x1 × x2.

Proposition 3 . 5 .

 35 The class of WCPN functions is closed by composition.

Definition 4 . 2 (

 42 Products of wqos and Dickson's Lemma). Let (S 1 , 1 ), . . . , (S n , n ) be qos. Their product is the qo (S × , × ) with S × def = S 1 × • • • × S n and × given by

¢Fig. 4 .

 4 Fig. 4. Example for Def. 4.4: A factorization of ρ = ρ0a1ρ1a2ρ2 witnessing ρ ¢ ρ .

Lemma 4 . 7 (

 47 Pumping Lemma). Let ρ ¢ ρ and let u, v ∈ N d such that src(ρ ) = src(ρ) + u and tgt(ρ ) = tgt(ρ) + v. Then∀x ∈ N : src(ρ) + x • u * -→ tgt(ρ) + x • v .

The "⇒" direction is proved by induction on the length of the run, where every additional step respects the invariant stated by Eq. 1. The "⇐" direction is obvious when j = 1, and proved by concatenating steps of the form (q2, x, z) -→ (q2, x -2, z + 1) when j = 2.