Pierre Bourreau
email: bourreau@labri.fr

Laura Kallmeyer
email: kallmeyer@phil.uni-duesseldorf.de

Sylvain Salvati
email: salvati@labri.fr

On IO-copying and mildly-context sensitive formalisms

Keywords: mildly context-sensitive languages, abstract families of languages, IO substitution, PMCFG

The class of mildly context-sensitive languages is commonly accepted as fulfilling the requirements to describe natural language. Many formalisms are known to generate languages which belong to this class, such as tree-adjoining grammars, multiple context-free grammars or abstract categorial grammars. All these formalisms share the property of being describe thanks to linear transformations, i.e. which avoid erasing or copying of material along derivations. We show that restricted copying operations allow defining mildly context-sensitive languages, thanks to the introduction of a new operation: IO-substition of languages.

Introduction

The question of the amount of expressive power needed in order to deal with natural languages is still an open question. In this context, the notion of mild-context-sensitivity has been proposed. A grammar formalism is mildly context-sensitive if a) it is more powerful that CFG, b) it generates only languages of constant growth, c) it can generate languages that describe a limited amount of cross-serial dependencies and d) it is polynomially parsable. A well-known class of formalisms that is still mildly contextsensitive is the class containing Linear Context-Free Rewriting Systems (LCFRS) and equivalent formalisms such as Multiple Context-Free Grammars (MCFG), Minimalist Grammar (MG) and set-local multicomponent Tree Adjoining Grammars (MCTAG).

This paper explores ways to characterize formally and linguistically interesting extensions of the class of LCFRL/MFCL that are still mildly context-sensitive. It follows ideas from [START_REF] Kallmeyer | On mildly context-sensitive non-linear rewriting[END_REF] where a mildly context-sensitive LCFRS extension is defined that allows for a limited amount of copying during derivations. The definition of this formalisms called Literal Movement Grammars of constant non-linearity (CNL-LMG) is, however, based on properties of possible derivations in a grammar. Furthermore, it lacks an independent characterization of the resulting class of string languages.

In this paper, we define first an operation on string languages that amounts to copying a substring into different places, called IO-substitution. The idea is roughly that we generate some string w 2 and a string w 1 that contains several occurrences of a variable x. This variable marks all the positions where the string w 2 gets copied to. An important point is that the string that gets copied does not increase while being copied. Once we have such a copying operation, we define the closure of MCFL/LCFRL under this operation as a new class IO-MCFL. We show that the languages in this class still have the constant-growth property.

As an example, consider the languages (xd) * x and a * . IO-substitution of x in the first language by all possible words from the second language means fixing a word a n from the second and replacing all occurrences of x in words from the first by a n . As a result, we obtain {(a n d) m a n | n, m ≥ 0} which is a generalization of the counting language that is not a MCFL [START_REF] Kallmeyer | On mildly context-sensitive non-linear rewriting[END_REF].

In parallel to the definition of IO-substitution on strings, we then characterize possible rules in Literal Movement Grammars (LGM), an MCFG-extension, that describe exactly the IO-subsitition operation. Based on this, a new grammar formalism is defined that turns out to be mildly context-sensitive while being a proper extension of MCFG.

The structure of the paper is as follows: ... to be written ...

Preliminaries

Mildly context-sensitive languages

Let us consider a countable set Σ, called an alphabet. We write Σ * = (Σ, •, ǫ) the (free) monoid on Σ, where • is the operation of concatenation, and ǫ the identity element. Any set L ⊆ Σ * is called a language on Σ.

Given a language L ∈ Σ * , and w one of its elements (called words), we define the usual notions of length and number of occurrences of a letter a ∈ Σ in w by induction on w:

|ǫ| = 0, |w| = 1 if w ∈ Σ and |w 1 • w 2 | = |w 1 | + |w 2 |, for the length of w and |ǫ| a = 0, |w| a = 1 if w = a, |w| a = 0 if w ∈ Σ -{a} and |w 1 • w 2 | a = |w 1 | a + |w 2 | a for the number of occurrences of a in w.
The class MCSL of mildly context-sensitive languages [START_REF] Aravind | Tree-adjoining grammars: How much context-sensitivity is required to provide reasonable strucutral descriptions? Natural Language Parsing: Psychological, Computational and Theoretical Perspectives[END_REF][START_REF] Weir | Characterizing Mildly Context-Sensitive Grammar Formalisms[END_REF] is defined as the smallest set such that:

-MCSL contains all context-free languages.

some restricted crossing-dependencies are taken in account by the languages L ∈ MCSL every language L ∈ MCSL verifies the constant-growth property.

every language L ∈ MCSL is recognizable in polynomial-time.

The first property specifies that MCSL falls between the classes of context-free languages and context-sensitive languages in Chomsky's hierarchy: CFL ⊆ MCSL ⊆ CSL. While vague, the second property ensures this class is bigger than the class of context-free languages. Hence, these two properties are easily ensured when defining some new formalisms. This work mainly focuses on the last two properties. For the constant-growth property, we consider the following definition [START_REF] Kallmeyer | On mildly context-sensitive non-linear rewriting[END_REF], which is stronger than the original definition in [START_REF] Weir | Characterizing Mildly Context-Sensitive Grammar Formalisms[END_REF], and is based on the commonly-known notion of the Parikh image:

1. - → p (w) = - → x + - → y and 2. for every i ≥ 1, - → x + i - → y ∈ - → p (L).
The constant-growth property is a property weaker than the condition of semilinearity:

Definition 3. A set L of vectors on a vector space N k is called a linear set if L = { - → x 0 + k 1 - → x 1 + . . . + k n - → x n | n ∈ N, k 1 , . . . , k n ∈ N -{0}}.
A semilinear set is a finite union of linear sets.

Definition 4. A language L is said semilinear if -→ p (L) is a semilinear set.

Many formalisms were created to generate languages that belong to MCSL, among which are tree-adjoining grammars (TAGs) [START_REF] Aravind | Tree adjunct grammars[END_REF], multiple context-free grammars (MCFGs) [START_REF] Seki | On multiple context-free grammars[END_REF], which will be introduced in the next section, or abstract categorial grammars (ACGs) [START_REF] De | Towards abstract categorial grammars[END_REF][START_REF] Muskens | Lambda Grammars and the Syntax-Semantics Interface[END_REF]. It is known that the class of multiple context-free languages (i.e. languages generated by MCFGs), which we will write MCFL, strictly entails the class of tree-adjoining languages (i.e. languages generated by TAGs). Hence, we consider MCFL as the best approximation of MCSL.

An important property of languages which belong to the class MCFL is that they are semilinear. In this paper, we introduce the operation of IO-substitution on languages in the class MCFL of languages; we will see that this operation allow the definition of a new class of languages which are not semilinear, but verify the constant-growth property.

Multiple context-free tree languages

In what follows, we define a multiple context-free language as the yield of a tree language derived by a linear multiple context-free tree language (linear MCFTG). Thanks to this definition, we will then prove that some specific MCFTGs are polynomial. The tree languages derived by Linear MCFTGs are exactly the tree languages derived by abstract categorial grammars [START_REF] De | Towards abstract categorial grammars[END_REF][START_REF] Muskens | Lambda Grammars and the Syntax-Semantics Interface[END_REF] of trees, and we write this class of languages MCFTL.

In order to define the formalism of MCFTG, let us first define trees and tree contexts. These objects will be defined as particular λ-terms types with simple types built on the single type o: given an atomic type o, we define the set of types on o as the smallest set

T o such that o ∈ T o and (α → β) ∈ T o if α, β ∈ T o .
Tthe usual convention of parenthesis are taken: a type α 1 → (α 2 → α 3 ) will be written α 1 → α 2 → α 3 . Given a type α ∈ T o , we define the order ord(α) by induction on α as ord(o) = 1, and ord(α

1 → α 2 ) = max(1 + ord(α 1 ), ord(α 2 )). Definition 5. An alphabet Σ is said typed if to every element a in Σ is associated a type of T o , written τ(a). A typed alphabet is called an n-order alphabet (where n ≥ 0) if max a∈Σ (ord(τ(a))) ≤ n. In what follows, a type α → . . . → α n → γ ∈ T o will be abreviated into α n → γ.
Given a typed alphabet Σ and n > 0, we note by Σ n the smaller subset of Σ which contains all the elements of Σ which associated type is of order less or equal to n. Definition 6. Let us consider an enumerable typed alphabet Σ and a type α ∈ T o . We define T α (Σ) the trees of type α on Σ as the smallest set such that:

-c ∈ T α (Σ) if c ∈ Σ and τ(c) = α -(t 1 t 2 ) ∈ T α (Σ) if t 1 ∈ T γ→α (Σ) and t 2 ∈ T γ (Σ). The set T(Σ) of trees on Σ is defined as T(Σ) = T o (Σ). Moreover, if Σ is 2-order, we say that T(Σ) is a pure set of trees.
We take the usual conventions for parenthesis so that a tree (t 1 t 2 )t 3 is written as t 1 t 2 t 3 . The general form of a tree in T(Σ) is therefore ct 1 . . . t n , where c ∈ Σ, τ(c) = α 1 → . . . → α n → o and for every 1

≤ i ≤ n, t i ∈ T α i (Σ).
Given a type α ∈ T o and a tree t ∈ T α (Σ) and a ∈ Σ, we define |t| a as the number of occurrences of a in t by induction on t:

|a| a = 1, |c| a = 0 if c ∈ Σ -{a}, and |t 1 t 2 | a = |t 1 | a |t 2 | a .
The yield function is a function which takes a tree t as its inputs and returns the sequence of leafs of t from left to right. Formally, given a typed alphabet Σ, we define yield :

T(Σ) → Σ * , as yield(c) = c if c ∈ Σ, yield(t 1 t 2 ) = yield(t 2 ) if t 1 = c ∈ Σ and yield(t 1 t 2 ) = yield(t 1 )
• yield(t 2 ) otherwise. We extend this notion to sets of trees: given a set of trees L, yL = {yield(t) | t ∈ L}. Definition 7. Let us consider a finite second-order alphabet Σ and a type α ∈ T o . We define the set T α [] (Σ) of tree contexts of type α for T(Σ) as the smallest set of terms such that λx 1 . . .

x n .t is in T α [] (Σ) if X = {x 1 , . . . , x n } is a typed alphabet, where for every 1 ≤ i ≤ n, τ(x i ) = α i , α = α 1 → . . . , → α n → o, and t ∈ T(Σ ∪ X).
The set of tree contexts on (Σ) is defined by

(T α [] (Σ)) α∈T o . Finally, such a tree context λx 1 . . . x n .t is said: -linear if |t| x i = 1 for every 1 ≤ i ≤ n -almost affine if for every 1 ≤ i ≤ n, |t| x i > 1 iff x i ∈ Σ 1 ∪ X 1 Remark 1.
In what follows, we will note trees by t, t ′ , t 1 , . . ., contexts by C,C ′ ,C 1 , . . .. Moreover, finite sequences of variables x 1 , . . . , x n will often be written as x, and identically, finite sequences of contexts of the form C 1 , . . . ,C m will be noted by C.

It is important to remark that T(Σ) = T o

[] (Σ). Moreover, tree contexts are defined as particular simply-typed λ-terms. In the rest of the document, we will take as granted the usual notions of substitutions, α-conversion, β-reduction and η-conversions defined in the simply-typed λ-calculus (see [START_REF] Barendregt | λ-calculus: its syntax and semantics[END_REF][START_REF] Heine | Lectures on the Curry-Howard isomorphism[END_REF] for details). These notions will be used to define a tree context substition: given a typed alphabet X, σ = [x 1 := C 1 , . . . , x n := C n ] (where

x i ∈ X and C i ∈ T τ(x i )
[] (Σ) for every i ∈ {1, . . . , n}) is a term substitution from X to T [] (Σ); the application of σ to a tree context C is defined as |C • σ| β , i.e. the normal form of the application of the λ-term substitution σ to the λ-term C. Finally, we define the application of tree contexts C 1 , . . . ,C n to a tree context λx 1 . . .

x n .t by app(C,C 1 , . . . ,C n ) = |C • [x 1 := C 1 , . . . , x n := C n ]| β .
Definition 8. An alphabet Σ is said multi-typed if to every element a in Σ is associated a natural number n ∈ N, called the rank of a (written r(a)), and to every pair (a, i), where a ∈ Σ and

1 ≤ i ≤ r(a) is associated a type in T o (written τ(a, i))
We are in position of defining MCFTGs. These grammars can be seen as MCFGs on tree contexts. Definition 9. A multiple context-free tree grammar (MCFTG for short) is a tuple G = (N, Σ, Y, P, S ) where:

-N is a finite multi-typed alphabet of elements called non-terminals.

-Σ is a finite second-order alphabet of elements called terminals.

-Y is an enumerable typed alphabet of variables disjoint from Σ.

-S ∈ N is called the starting non-terminal of G and verifies r(S ) = 1.

-P is a finite set of production rules of the form:

A 0 (C 1 , . . . ,C r 0 ) → A 1 (x 1,1 , . . . , x 1,r 1 ), . . . , A n (x n,1 , . . . , x n,r n ) where • for very 0 ≤ i ≤ n, r(A i ) = r i . • for every 1 ≤ k ≤ r, C k ∈ T α i [] (Σ ∪ Y)
, where α i = t(A 0 , k). • for every i ∈ {1, . . . , n} and j ∈ {1, . . . , r i }, x i, j ∈ Y is of type t(A i , j) and verifies

Σ 1≤k≤r 0 |C k | x i , j = 1. Moreover, given i 1 , i 2 ∈ {1, . . . , n} and j 1 ∈ {1, . . . , r i 1 }, j 2 ∈ {1, . . . , r i 2 }, we have x i 1 , j 1 = x i 2 , j 2 iff i 1 = i 2 and j 1 = j 2
Such a grammar is said linear (resp. almost affine) if for every rule π ∈ P of the form A 0 (C 1 , . . . ,C r 0 ) → A 1 (x 1,1 , . . . , x 1,r 1 ), . . . , A n (x n,1 , . . . , x n,r n ), the contexts C 1 , . . . ,C r 0 are linear (resp. almost affine).

Example 1. Let us consider the MCFTG G = (N, Σ, Y, P, S ) where b,c,d,ǫ, e, f }, and P is made of the following production rules:

N = {S , A 1 , A 2 }, Σ = {a,
S (ex 1 x 2 x 3 x 4 ) → A 1 (x 1 , x 3 ), A 2 (x 2 , x 4 ) A 1 (ǫ, ǫ) A 1 ( f ax 1 , f cx 3 ) → A 1 (x 1 , x 3 ) A 1 (ǫ, ǫ) A 1 ( f bx 2 , f dx 4 ) → A 1 (x 2 , x 4 ) This MCFTG is a linear MCFTG. Moreover, r(S ) = 1, r(A 1 ) = r(A 2 ) = 2 and τ(S , 1) = τ(A 1 , 1) = τ(A 1 , 2) = τ(A 2 , 1) = τ(A 2 , 2) = o.
Definition 10. Given a MCFTG G = (N, Σ, Y, P, S ), and a non-terminal A ∈ N of arity r, we define the relation of derivation → * G by: 1

. if A(C 1 , . . . ,C r ) is a production rule in P, then → * G A(C 1 , . . . ,C n ) 2. → * G A(C 1 • σ, . . . ,C r • σ) if: -σ is a substitution from Y to T [] (Σ)
there exists a rule A(C 1 , . . . ,C r ) → A 1 (x 1,1 , . . . , x 1,r 1 ), . . . , A n (x n,1 , . . . , x n,r n ) in P for every

1 ≤ i ≤ n, the relation → * G A i (x 1,1 • σ, . . . , x i,r i • σ) is verified. The language L(G) generated by a MCFTG G = (N, Σ, Y, P, S ) is defined as the set {t ∈ T [] (Σ) | → * G S (t)}.
The class of tree languages MCFTL is defines as the smallest set which contains every language derived by some MCFTG.

In the previous example, the language L(G) derived by the MCFTG G is

{c( f a( f a . . . f a m ǫ)...)( f b( f b . . . f b n ǫ)...)( f c( f c . . . f c m ǫ)...)( f d( f d . . . f d m ǫ)...) | n, m ∈ N}
Moreover, we can remark that yL(G) = {a m b n c m d n l n, m ∈ N} which is known to be a MCFL. This result is generalized in the following theorem:

Theorem 1 ([dGP04,Kan06]). A language L belongs to MCFL iff there is a linear MCTFG G such that yL(G) = L.
Finally, we give the following theorem related to the complexity of the recognition problem of tree languages derived by a MCFTG.

Theorem 2 ([Kan07,Yos06], [START_REF] Bourreau | A Datalog recognizer for almost affine λ-CFGs[END_REF]). The recognition problem of an almost affine MCFTG is LOGCFL.

Because the class of problems LOGCFL is a sub-class of the problem solvable in polynomial-time, this theorem will be of particular importance so as to prove that the new class of language we define in this article is recgnizable in polynomial time, and is hence included in MCSL.

3 IO-substitutions, semilinearity and constant-growth

IO-substitution and copies

In this section, we introduce a new operation on languages, which we will use to define constant-growth languages. This operation, which we call IO-substitution enables a specific kind of copying operation. Thanks to this operation, we want to capture some languages which do not belong to MCFL, but still verify the constant-growth property, as shown in [START_REF] Kallmeyer | On mildly context-sensitive non-linear rewriting[END_REF]:

Example 2. The language L a,b {(a n b n ) m | n, m ∈ N -{0}} is not a MCFL. Nevertheless, it is a semilinear language, as its Parikh's image is {(1, 1) + k(1, 1) | k ∈ N}.
The language L count = {(a n d) m a n | n, m ∈ N} is not a semilinear language, but verifies the constant-growth property.

The language L exp = {a 2 n | n ∈ N} is neither a semilinear, nor a language which verifies the constant-growth property.

Interestingly, those languages are also known to be generated by IO-macro grammars [START_REF] Fischer | Grammars with macro-like productions[END_REF][START_REF] Michael | Grammars with macro-like productions[END_REF], in which copying operations are allowed in a specific way, which we will not discuss in detail in this article. In brief words, Fischer makes a clean distinction between IO derivations, in which every copies of the same occurrence of a non-terminal are replaced using the same rewriting rule, and an OI derivation, in which such a constraint does not exist. For instance, let us consider a word w = α 1 Aα 2 Aα 3 , where A does not appear in α 1 α 2 α 3 , and the two occurrences of A are supposed to result from a copying operation. We consider the rewritings of A as w 1 or w 2 . An IO derivation forces the two occurrences of A to be rewritten using the same rewriting rule; it hence defines the language {α 1 wα 2 wα 3 | w ∈ {w 1 , w 2 }}. An OI derivation would lead to the derivation of the language

{α 1 w ′ 1 α 2 w ′ 2 α 3 | w ′ 1 , w ′ 2 ∈ {w 1 , w 2 }}.
We use the same ideas to define the IO-substitution on languages, as contrasted with the classic susbstitution, which can be seen as an OI-substitution.

Definition 11. Let us consider an alphabet Σ and a variable x, and two languages L 1 ∈ (Σ ∪ {x}) * and L 2 ∈ Σ * . Given words w 1 ∈ L 1 , w 2 ∈ L 2 and x ∈ χ, we define the word w 1 [x := w 2 ] IO ∈ Σ by induction:

-x[x := w 2 ] IO = w 2 -a[x := w 2 ] IO = a if a x -ww ′ [x := w 2 ] IO = w[x := w 2 ] IO w ′ [x := w 2 ] IO The language L 1 [x := L 2 ] IO is then defined as {w 1 [x := w 2 ] IO ∈ Σ | w 1 ∈ L 1 , w 2 ∈ L 2 }.
Based on this operation, we can build the languages L a,b and L count easily from context-free languages. Indeed, given

L 1 = {x n | n ∈ N -{0}} and L 2 = {a m b m | m ∈ N -{0}}, the language L a,b is the language L 1 [x := L 2 ] IO . In the same way, L count = L ′ 1 [x := L ′ 2 ] IO , where L ′ 1 = {(xd) m x | m ∈ N} and L ′ 2 = {a n | n ∈ N}.
On the other hand, there is no trivial way to use the IO-substitution operation on context-free languages or mildly context-sensitive languages to generate L exp . One can also remark that L 1 , L 2 , L ′ 1 and L ′ 2 are context-free languages, and are therefore semilinear languages (hence, verifiy the constant-growth property). It is therefore natural to investigate the conditions under which semilinearity and the constant-growth propery are preserved by the IOsubstitution operation.

Preserving the semilinearity and constant-growth properties

In the previous examples, we have seen that the newly introduced operation of IOsubstitution allows, in some cases, building semilinear languages or constant-growth languages from semilinear languages. We now investigate the conditions which allow preserving these properties.

Definition 12. Let us consider a semilinear language L ⊆ Σ * and its Parikh image p(L) = i∈I S i (I ⊂ N finite), where for every i ∈ I,

S i = { --→ v i,0 + n 1 --→ v i,1 + . . . + n r i --→ v i,r i | n 1 , . . . , n r i ∈ N}
Given a ∈ Σ, L is said a-isolating if, for every i ∈ I, there exists a unique l i ∈ {0, . . . , r i } such that:

for every j ∈ {0, . . .

r l }, -→ v i, j (k a ) 0 iff j = l i . -for every c ∈ Σ -{a}, --→ v i,l i (k c ) = 0
Example 3. The language {x n | n ∈ N} is obviously x-isolating. The language abx(a) * x * is not x-isolating as its Parikh image is {(1, 1, 1)+n(1, 0, 0)+m(0, 0, 1) | n, m ∈ N}. Finally, the language (xa) * x is not x-isolating, its Parikh image being {(0, 1)

+ n(1, 1) | n ∈ N}.
Remark 2. Given a language L ∈ Σ * and a ∈ Σ such that L is a-isolating, each linear set S ∈ {S 1 , . . . , S l }, such that l i=1 S i = p(L) can be written as:

Σ i∈I n i - → x i + n t - → x t
where n 0 = 1, t I, for every i ∈ I ∪ {t} -→ x i (k a ) 0 iff i = t, and -→ x t (k c ) = 0 for every c ∈ Σ -{a}.

We now show that the IO-substitution of a letter a by a semilinear language, on a a-isolating language generates a semilinear language.

Theorem 3. Given a semilinear language L 1 ∈ (Σ ∪ {x}) * , x-isolating, and a semilinear language L 2 , the language L 1 [x := L 2 ] IO is semilinear.

Proof. Let us consider the language L = L 1 [x := L 2 ] IO , and a word w ∈ L. By definition, there exist w 1 ∈ L 1 and w 2 ∈ L 2 such that w = w 1 [x := w 2 ] IO . Because L 1 and L 2 are semilinear, for p(L 1 ) and p(L 2 ) the Parikh images of L 1 and L 2 respectively, there exist linear sets S 1 ⊂ p(L 1 ) and S 2 ⊂ p(L 2 ) such that p(w 1 ) ∈ S 1 and p(w 2 ) ∈ S 2 ; hence:

-p(w 1 ) ∈ { - → x 0 + n 1 - → x 1 + . . . + n p -→ x p | n 1 , . . . , n p ∈ N} -p(w 2 ) ∈ { - → y 0 + m 1 - → y 1 + . . . + m r - → y r | m 1 , . . . , m r ∈ N} Moreover, because L 1 is x-isolating, we can write p(w 1 ) ∈ {Σ i∈I n i - → x i + n t - → x t | for all i ∈ I ∪ {t}, n i ∈ N and n 0 = 1}
where t I, I ∪ {t} = {0, . . . , p}, -→ x i (k x ) = 0 for every i ∈ I, and -→ x t (k c ) = 0 for every c ∈ Σ.

Then, by construction, the Parikh image of w can be written as

p(w) = - → z 0 + n 1 - → z 1 + . . . + n p - → z p
where, for every i ∈ {0, . . . , p}, -

→ z i = - → x i + - → x i (k x ) - → p (w 2 ). Let us write - → x i (k x ) = K i , for every i ∈ {0, . . . , p}
The Parikh image of w can be rewritten according to the following results:

1. - → z i = - → x i , for every i ∈ I, because K i = 0 2. - → z t = K t - → p (w 2 ), because - → x t (k a ) = 0 for every a x. Hence, - → z t = K t ( - → y 0 + m 1 - → y 1 + . . . + m r - → y r ) = K t - → y 0 + m 1 K t - → y 1 + . . . + m r K t - → y r Finally, p(w) ∈ {Σ i∈I n i - → x i + n t Σ j∈{1,...,r} m j K t - → y j | ∀i ∈ {1, . . . , r}, j ∈ I ∪ {t}, m i , n j ∈ N} ∈ {Σ i∈I n i - → x i + n t Σ j∈{1,...,r} m j -→ y jt | ∀i ∈ {1, . . . , r}, j ∈ I ∪ {t}, m i , n j ∈ N} ∈ {Σ i∈I n i - → x i + Σ j∈{1,r} m j -→ y ′ jt | ∀i ∈ {1, . . . , r}, j ∈ I ∪ {t}, m i , n j ∈ N} belongs to a linear set. Moreover, for w ′ = w ′ 1 [x := w ′ 2 ]
IO , where -→ p (w ′ 1 ) and -→ p (w ′ 2 ) belong to the same linear sets as -→ p (w 1 ) and -→ p (w 2 ), it is easy to verify that -→ p (w ′ ) belongs to the same linear set as -→ p (w). The set of linear sets built in the proof is trivially finite because -→ p (L 1 ) and -→ p (L 2 ) are finite. Hence L is a semilinear language.

We now show that the preservation of the constant-growth property is more direct, as substituting a letter by a constant-growth language, in a constant-growth language suffices. Theorem 4. Given a constant-growth language L 1 ⊆ (Σ ∪ {x}) * , and a constant-growth language L 2 ⊆ Σ * . The language L 1 [x := L 2 ] IO is constant-growth.

Proof. Let us a consider a word w 1 in L 1 , and a word w 2 in L 2 . We note by k the number of occurrences of x in w 1 (i.e. -→ p (w 1 )(k x ) = k).

By definition of a constant-growth language, for every i ∈ {1, 2}, there exists a constant c i ∈ N such that, for every word

w ′ i ∈ L i verifying |w ′ i | ≥ c i , there exist - → x , - → y ∈ N |Σ| such that - → p (w ′ i ) = - → x + - → y and, for every k ≥ 1, - → x + k - → y ∈ - → p (L i ). Let us first suppose |w 2 | ≥ c 2 . Then - → p (w 1 [x := w 2 ] IO ) = - → z + k - → p ′ (w 2 ) = - → z + k - → x ′ 2 + k - → y ′ 2 ,
where -→ z is the Parikh image of w 1 on Σ, and -→ p ′ (w 2 ) is the Parikh image of w 2 on the same alphabet. By hypothesis, we can consider an integer i ≥ 1 and a word w

′ 2 ∈ L 2 such that - → p (w ′ 2 ) = - → x 2 + i - → y 2 . Then, - → p (w 1 [x := w ′ 2 ] IO ) = - → z + k - → p ′ (w ′ 2 ) = - → z + k - → x ′ + ki - → y ′ . Otherwise, suppose |w 2 | < c 2 and |w 1 | ≥ c 1 . Then - → p (w 1 ) = x 1 + y 1 , and given i > 1, there exist a word w ′ 1 ∈ L 1 such that - → p (w ′ 1 ) = - → x 1 + i - → y 1 . We give k 1 = - → x 1 (x) and k 2 = - → y 1 (x). Then -- → p (w 1 [x := w 2 ] IO ) = - → x ′ 1 + k 1 - → p ′ (w 2 ) + - → y ′ 1 + k 2 - → p ′ (w 2 ) -- → p (w ′ 1 [x := w 2 ] IO ) = - → x ′ 1 + k 1 - → p ′ (w 2 ) + i - → y ′ 1 + ik 2 - → p ′ (w 2 )
where given -→ x a Parikh vector on Σ ∪ {x}, -→ x ′ is the same vector on Σ; and -→ p ′ (w 2 ) is the Parikh image of w 2 on the same alphabet.

As a conclusion, L 1 [w := L 2 ] IO is a constant-growth language. We can consider the constant associated to the growth of this language as c 1 c 2 .

Thanks to the two previous theorems, we proved that the constant-growth and semilinearity properties of languages can be preserved by the IO-substitution operation. In the following section, we seek a class of languages bigger than MCFL which is included in MCSL, by using this operation.

IO-Multiple Context-Free Languages

Definition

In the previous section, we proved some properties on the IO-substitution which allows preserving the semilinearity or constant-growth properties. As mentionned in the first section, we can consider the class of multiple context-free languages as the biggest class approximating mildly context-sensitive languages. We now extend the class MCFL by using the IO-substition operation.

Definition 13. We consider the family of IO-mildly context sensitive languages (written IO-MCFL) as the smallest family such that L ∈ IO-MCFL if:

-L ∈ MCFL or -if L = L 1 [x := L 2 ] IO where L 1 , L 2 ∈ IO-MCFL.
Thanks to this definition, languages L a,b and L count can be considered to belong to IO-MCFL. The following theorem is a direct corrolary of Theorem 4.

Theorem 5. Every language L in IO-MCFL verifies the constant-growth property.

Proof. We proceed by induction on L. If L ∈ MCFL, the result is given by the fact that L is semilinear. Otherwise, there exist L 1 ∈ IO-MCFL and L 2 ∈ IO-MCFL such that L = L 1 [x := L 2 ] IO . By induction hypothesis, L 1 and L 2 verify the constant-growth property. According to Theorem 4, L is constant-growth.

In order to see if IO-MCFL is a better approximation of the class MCSL, we then need to know if such languages are tractable in polynomial time. In order to do so, we give a formalism which exactly captures the IO-MCFL class of languages, thanks to the multiple context-free tree languages given in section 2.2.

IO-MCFGs as quasi-affine MCFTGs

As mentionned in section 2.2, the class MCFTL is connected to MCFL through theorem 1. In what follows, we seek the characterization of some MCFTGs which yield are exactly IO-MCFLs.

Intuitively, given a language L 1 ∈ Σ ∪ {x}, where L 1 and L 2 are MCFLs, we can remark that the letter x may have many occurrences in w 1 ∈ L 1 . Given a MCFTG G 1 such that yL(G 1 ), the idea is too consider x not as a leaf in the trees derived by G 1 , but by a variable which can be substituted by a word w 2 ∈ L 2 . Therefore, we need to build a MCFTG G ′ 1 such that t ∈ L(G 1 ) iff λx.t ∈ L(G ′ 1 ), and then apply a simple S (x 1 x 2 ) → S ′ 1 (x 1 ), S (x 2 ) where S ′ 1 and S 2 are the starting non-terminals of G ′ 1 and G 2 respectively.

Remark that, because x will now be considered as a variable, the contexts appearing in the left-hand side of a production rule in G ′ 1 will not be linear anymore. But x being a leaf, its type is τ(x) = o, and the contexts will therefore be almost affine, which still ensures the recognizability problem belongs to LOGCFL, hence to the class of problems solvable in polynomial-time. • abs(t 1 t 2 , x) = abs(t 1 , x)abs(t 2 , x). Finally a rule A 0 (C 1 , . . . ,C r ) → A 1 (x 1,1 , . . . , x 1,r 1 ), . . . , A n (x n,1 , . . . , x n,r n ) belongs to P iff A ′ 0 (C ′ 1 , . . . ,C ′ r ) → A ′ 1 (x ′ 1,1 , . . . , x ′ 1,r 1 ), . . . , A ′ n (x ′ n,1 , . . . , x ′ n,r n )

belongs to abs(P, x), where A ′ i = abs(A i , x) and x ′ i, j = abs(x i, j , x) for every 0 ≤ i|eqn and 1 ≤ j ≤ r i , and C ′ k = abs(C k , x) for every1 ≤ k ≤ r. The transformation given by abs intuitively result in considering x as a variable, on which tree context substitutions can be applied. This is made explicit in the following theorem. Proof. We consider the general form of a MCFTG so that the language derived is a tuple of tree contexts, and We proceed by induction on the derivation of such a tuple C ∈ L. Let us consider the last rule π used to derive C in G, which general form is: If n 0; by induction hypothesis, for every 1 ≤ k ≤ n, the following statement stands: → * G A k (C k,1 , . . . ,C k,r k ) iff → * abs(G,x) abs(A k , x)(λx.C k,1 , . . . , λx.C k,r k ). Therefore, given a tree context substitution σ = [x 1,1 := C 1,1 , . . . , x 1,r 1 := C 1,r 1 , . . . ,C n,1 , . . . , x n,r n := C n,r n ], such that C = (C 1 • σ, . . . ,C r • σ), we build σ ′ = [x ′ 1,1 := λx.C ′ 1,1 , . . . , x ′ n,r n := λx.C ′ n,r n ] where x ′ i, j := abs(x i, j , x) and C ′ i, j := abs(C i, j , x), for every 1 ≤ i ≤ n and every 1 ≤ j ≤ r i . By construction, we obtain C = (λx.C 1 , . . . , λx.C r ).

Definition 14 .

 14 Given a MCFTG G = (N, Σ ∪ {x}, Y, P, S ) where τ(x) = α, we define the MCFTG abs(G, x) = (abs(N, x), Σ, abs(Y, x), abs(P, x), abs(S , x))as follows:-given a type α = α 1 → . . . → α n → α 0 in T o , we define abs(α, x) = τ(x) → α 1 → . . . → α n → α 0 . for every A ∈ N, abs(A, x) = A such that r(A ′ ) = r(A) and for every 1 ≤ i ≤ r(A), t(A ′ , i) = abs(t(A, i), x).Finally, abs(N, x) = {abs(A, x) | A ∈ N}. y ∈ Y and τ(y) = γ in Y iff y ∈ abs(Y, x) and τ(y) = abs(y, x) in abs(Y, x). given a tree context C in T [] (Σ ∪ Y), we define abs(C, x) ∈ T [] (Σ ∪ abs(Y, x)), as λx.abs(C, x), where: • abs(λy.C ′ , x) = λy.abs(C ′ , x), for C ′ ∈ T [] (Σ ∪ Y}) • abs(c, x) = c for c Y • abs(y, x) = (yx), for y ∈ Y.

Lemma 1 .

 1 Given a MCFTG G = (N, Σ ∪{x}, Y, P, S ), the language L(abs(G, x)) is equal to {λx.C ∈ T [] (Σ) | C ∈ L(G)}.

A 0 (

 0 C 1 , . . . ,C r ) → A 1 (x 1 ), . . . , A n (x n ) If n = 0, then C = (C 1 , . . . ,C r ) and abs(π, x) = abs(A 0 , x)(C ′ 1 , . . . ,C ′ r ), where for every1 ≤ i ≤ r, C ′ i = abs(C i , x). Moreover, C ′ i ∈ T [] (Σ) and C ′ i = λx.C i by construction.The tuple (λx.C 1 , . . . , λx.C r ) is therefore recognized by abs(G, x).

  Notation 21 Let us consider an alphabet Σ and the vector space N |Σ| .

	Given a letter → v on the coordinate → v [a] the scalar of -→ v on N |Σ| , we note by -a ∈ Σ and a vector -
	associated to a.
	Definition 1. Let us consider a word w in a language L ⊆ Σ * . The Parikh image of w, written -→ p (w) is such that, for every a ∈ Σ, -→ p (w)[a] = |w| a . The Parikh image of L is defined as -→ p (L) = { -→ p (w) | w ∈ L}.
	Definition 2. A language L ∈ Σ * is said to verify the constant-growth property if there
	exists a constant c ∈ N -{0} such that, for every word w ∈ L verifying |w| > c, there exists -→ x , -→ y ∈ N |Σ| for which:

We now need to build the MCFTG which produces the substitution of x in a tree context C 1 derived in abs(G 1 , x) by a tree context C 2 derived by G 2 . In particular, if ¢tau(x) = o, x may appear in the yield of any tree derived by G 1 , and replacing every occurrence of x in t 1 = C 1 by the tree t 2 = C 2 , resumes to yt 1 [x := yt 2 ] IO .

First, we define disjunction of MCFTGs as follows: given two MCFTGs G 1 = (N 1 , Σ 1 , Y 1 , P 1 , S 1 ) and G 2 = (N 2 , Σ 2 , Y 2 , P 2 , S 2 ), G 1 and G 2 are said disjoint if N 1 ∩ N 2 = ∅. Remark that such a relation implies P 1 ∩ P 2 = ∅ and S 1 S 2 .

), S 2 (x 2 ). We now prove that this formalism exactly captures tree languages which yield form IO-MCFLs:

Proof. We proceed by induction on L. If L is a MCFL, there exists a linear MCFTG G such that yL(G) = L, and G si a IO-MCFTG by definition. Conversely, for G a linear MCFTG, yL(G) is a IO-MCFL. If there exist L 1 ⊆ (Σ ∪ {x}) * and L 2 ⊆ Σ * two MCFLs, such that L = L 1 [x := L 2 ] IO , by induction hypothesis, there exist two MCFTGs G 1 = (N 1 , Σ ∪ {x}, Y 1 , P 1 , S 1 ) and G 2 = (N 2 , Σ, Y 2 , P 2 , S 2 ), which can be considered disjoint, and such that L 1 = yL(G 1 ) and L 2 = yL(G 2 ). According to Lemma 1, L(abs

such that S abs(N 1 , x) ∪ N 2 and π = S (x 1 x 2 ) ∪ abs(S 1 , x)(x 1 ), S 2 (x 2 ). A t tree is recognized by this grammar iff there exist t 1 ∈ L(G 1 ) and t 2 ∈ L(G 2 ) such that t = app(t 1 , t 2 ) which is the result of substituting every occurrence of x in t 1 by t 2 . Finally,

Conversely, the yield of the language of an IO-MCFTG is an IO-MCFL.

It now suffices to show that the recognizability problem in this formalism can be solved in polynomial-time, which is a direct consequence of the following lemma.

Lemma 2. If G is an almost affine MCFTG, then abs(G, x) is an almost affine MCFTG.

Proof. In order to prove this property, it suffices to prove that, given an almost affine tree context C in T [] (Σ ∪ {x}), λx.abs(C, x) is a tree context in T [] (Σ). Therefore, given the general form λx α 1 1 . . . x α n n .t of C, if a variable y α Σ ∪ {x}) verifies |C| y 1 then there exists 1 ≤ j ≤ n such that y = x j and α j = o. Moreover, x might have a number of occurrences in C different from 0, which implies the same property is verified on λx.C, which therefore remains almost affine.

Corollary 1. The recognition problem of an IO-MCFL belongs to LOCGCFL.

As a conclusion, we proved that MCFL IO-MCFL ⊆ MCSL. This new class of languages can therefore be taken as the best approximation of the class of mildly context-sensitive languages.

While we proved that the recognition problem can be solved in polynomial-time, we next prove some usual properties taken to test the robustness of parsing in a given formalism, so as to explore additional proeprties of IO-MCFL.

Closure properties

In what follows, we study other properties enjoyed by IO-MCFLs. In particular, we are interested in the usual closure properties so as to know whether IO-MCFLs define a full abstract family of languages.

Definition 16. A family of languages L is called a (full)-abstract family of languages (written (full)-AFL) if L is closed by homomorphism, inverse homomorphism, intersection with a regular set, union, concatenation and the Kleene star.

In what follows, we show that most of this properties are verified. we consider a homomorphism H : Σ * → Σ * , and show that H (L) ∈ IO-MCFL by induction on L. If L is a MCFL, the property is verified as the family of MCFLs is an AFL. Otherwise, there exist

-We show that L 1 ∪ L 2 ∈ IO-MCFL. We can consider the general form L i = L ′ i [x i := L 2 ] IO , for i ∈ {1, 2}. Moreover, x 1 and x 2 can be renamed so that x 1 (resp. x 2 ) has no occurrence in L 2 (resp. L 1 ). Then

in a similar way:

2 is a IO -MCLF by induction hypothesis, (the result is given in the case L ′ 1 and L ′ 2 are MCFLs) which implies L 1 ∩ L 2 belongs to IO-MCFL by construction.

we show L 1 • L 2 belongs to IO-MCFL in a similar way: Proof. Let us consider a IO-MCFL L and a regular language L. We prove that L ∩ R belongs to IO-MCFL, by induction on L. If L is a MCFL, the result is given by the fat that MCFLs form a AFL. Let us suppose L = L 1 [x := L 2 ] IO . We consider M R = (M , •, ǫ) the syntactic monoid of R, where M is finite according to Myhill-Nerode. Then, there exists a homomorphism φ : Σ → M R and N ⊆ M R such that R = φ -1 (N ). Given m ∈ M let us consider the homomorphism φ m : Σ ∪ {x} → M R defined by φ m (x) = m and for every a ∈ Σ, φ m (a) = φ(a). We consider the regular set R m = φ -1 m (N ). By induction hypothesis, L 1,m = L 1 ∩ R m is in IO-MCFL. The language L 2,m = L 2 ∩ φ -1 ({m}) enjoys the same property, and by construction, L m = L 1,m [x := L 2,m ] IO belongs to IO-MCFL. Finally, because L ∩ R = m∈M L m , which is a finite union, and IO-MCFL is closed by union, we can conclude that L ∩ R is a IO-MCFL. While all these properties can be proved in quite easily, the closure under inverse homomorphism does not seem as trivial. Actually, we can conjecture that such a property does not stand.


Jérôme Leroux

Vector Addition System Reversible Reachability Problem

Keywords: 1998 ACM Subject Classification: 68R99, 68Q05, 03D99 Vector addition system, reachability, boundedness, cover

The reachability problem for vector addition systems is a central problem of net theory. This problem is known to be decidable but the complexity is still unknown. Whereas the problem is EXPSPACE-hard, no elementary upper bounds complexity are known. In this paper we consider the reversible reachability problem. This problem consists to decide if two configurations are reachable one from each other, or equivalently if they are in the same strongly connected component of the reachability graph. We show that this problem is EXPSPACE-complete. As an application of the introduced materials we characterize the reversibility domains of a vector addition system.

INTRODUCTION

Vector addition systems (VASs) or equivalently Petri nets are one of the most popular formal methods [START_REF] Esparza | Decidability issues for Petri nets -a survey[END_REF] for the representation and the analysis of parallel processes. Their reachability problem is central since many computational problems (even outside the realm of parallel processes) reduce to the reachability problem. Sacerdote and Tenney provided in [START_REF] Sacerdote | The decidability of the reachability problem for vector addition systems (preliminary version)[END_REF] a partial proof of decidability of this problem. The proof was completed in 1981 by Mayr [START_REF] Mayr | An algorithm for the general Petri net reachability problem[END_REF] and simplified by Kosaraju [START_REF] Kosaraju | Decidability of reachability in vector addition systems (preliminary version)[END_REF] from [START_REF] Sacerdote | The decidability of the reachability problem for vector addition systems (preliminary version)[END_REF][START_REF] Mayr | An algorithm for the general Petri net reachability problem[END_REF]. Ten years later [START_REF] Luc | A structure to decide reachability in Petri nets[END_REF], Lambert provided a further simplified version based on [START_REF] Kosaraju | Decidability of reachability in vector addition systems (preliminary version)[END_REF]. This last proof still remains difficult and the upper-bound complexity of the corresponding algorithm is just known to be non-primitive recursive. Nowadays, the exact complexity of the reachability problem for VASs is still an open-problem. The problem is known to be EXPSPACE-hard [START_REF] Cardoza | Exponential space complete problems for Petri nets and commutative semigroups: Preliminary report[END_REF]. Note that the existence of a primitive recursive upper bound of complexity for the reachability problem is still open since the Zakaria Bouziane's paper [START_REF] Bouziane | A primitive recursive algorithm for the general Petri net reachability problem[END_REF] introducing such a bound was proved to be incorrect by Petr Jančar [START_REF] Jančar | Bouziane's transformation of the Petri net reachability problem and incorrectness of the related algorithm[END_REF].

Recently, in [START_REF] Leroux | Vector addition systems reachability problem (a simpler solution)[END_REF], a new proof of the reachability problem based on the notion of transformer relations inspired by Hauschildt [START_REF] Hauschildt | Semilinearity of the Reachability Set is Decidable for Petri Nets[END_REF] was published. That proof shows that reachability sets are almost semilinear, a class of sets introduced in that paper that extends the class of Presburger sets. An application of that result was provided; a final configuration is proved to be not reachable from an initial one if and only if there exists a forward inductive invariant definable in the Presburger arithmetic that contains the initial configuration but not the final one. Since we can decide if a Presburger formula denotes a forward inductive invariant, we deduce that there exist checkable certificates of non-reachability in the Presburger arithmetic. In particular, there exists a simple algorithm for deciding the general VAS reachability problem based on two semi-algorithms. A first one that tries to prove the reachability by enumerating finite sequences of actions and a second one that tries to prove the non-reachability by enumerating Presburger formulas. The Presburger inductive invariants presented in that paper is obtained thanks to strongly connected subreachability graphs (called witness graph and recalled in Section 7). As a direct consequence, configurations in these graphs are reachable one from each other.

In this paper we consider the reversible reachability problem that consists to decide if two configurations are reachable one from each other. We prove that this problem is EXPSPACE-complete. This result extends known result for the subclasses of reversible and cyclic vector addition systems [START_REF] Bouziane | Cyclic Petri net reachability sets are semi-linear effectively constructible[END_REF][START_REF] Cardoza | Exponential space complete problems for Petri nets and commutative semigroups: Preliminary report[END_REF]. We also prove that the general coverability problem reduces to the reversible reachability problem (see Section 3). As an application of the introduced materials we characterize the reversibility domains of a vector addition system in the last Section 11.

PROJECTED VECTORS

We denote by Z and N the set of integers and natural numbers. In this paper, some components of vectors in Z d are projected away. In order to avoid multiple dimensions, we introduce an additional element ⋆ ∈ Z, the set Z ⋆ = Z ∪ {⋆}, and the set Z d I of vectors z ∈ Z d ⋆ such that I = {i | z(i) = ⋆}. Operations on Z are extended component-wise into operations on Z d I by interpreting ⋆ as a projected component. More formally we denote by z 1 + z 2 where z 1 , z 2 ∈ Z d I the vector z ∈ Z d I defined by z(i) = z 1 (i) + z 2 (i) for every i ∈ I. Symmetrically given z ∈ Z d I and an integer k ∈ Z, we denote by kz the vector in Z d I defined by (kz)(i) = k(z(i)) for every i ∈ I. The usual order ≤ over Z is extended over Z ⋆ into the unique total order ≤ satisfying z ≤ ⋆ for every z ∈ Z ⋆ . The relation ≤ is extended component-wise over Z d * . Example 2.1. We have k(⋆, 1) = (⋆, k) even if k = 0. We also have (⋆, 5) -(⋆, 2) = (⋆, 3) and (⋆, 1) + (⋆, 2) = (⋆, 3). We have

• • • ≤ -1 ≤ 0 ≤ 1 ≤ • • • ≤ ⋆.
The projection of a vector z ∈ Z d I by eliminating components indexed by L ⊆ {1, . . . , d} is the vector in Z d I∪L defined by π L (z)(i) = z(i) for every i ∈ L. The projection of a set Z ⊆ Z d I by eliminating components indexed by L is defined as expected by π

L (Z) = {π L (z) | z ∈ Z}.
Example 2.2. Let L = {1}. We have π L (1000, 1) = (⋆, 1) and π L (4, ⋆) = (⋆, ⋆). We also have π L ({(2, 0), (1, 1), (2, 0)}) = {(⋆, 0), (⋆, 1), (⋆, 2)}.

(ρ) = π L (c 0 ) . . . π L (c k ). Observe that if ρ is the run x σ -→ y then π L (ρ) is the run π L (x) σ -→ π L (y).
The following lemma provides a simple way to deduce a converse result.

Lemma 3.1. Let L be a set of indexes and c be a configuration such that there exists a run from π L (c) labelled by a word σ. If c(i) ≥ |σ| ||A|| ∞ for every i ∈ L then there exists a run from c labelled by σ.

Proof. Let c ∈ N d I be a configuration such that there exists a path from π L (c) labelled by a word σ = a 1 . . . a k where a j ∈ A. Let us introduce the vector c j = c + π I (a 1 + . . . + a j ). Since there exists a run from π L (c) labelled by σ we deduce that π L (c j ) ∈ N d I∪L . Observe that for every j ∈ {0, . . . , k} and for every i ∈ I we have

c j (i) ≥ c(i) -|σ| ||A|| ∞ . In particular if c(i) ≥ |σ| ||A|| ∞ for every i ∈ L\I we deduce that c j ∈ N d I . Therefore ρ = c 0 . . . c k is the run from c labelled by σ. Example 3.1. ρ = (2, 0)(1, 1)(0, 2) is the run (2, 0) (-1,1)(-1,1) --------→ (0, 2). Let L = {1} and observe that π L (ρ) = (⋆, 0)(⋆, 1)(⋆, 2) is the run (⋆, 0) (-1,1)(-1,1) --------→ (⋆, 2).
Let x and y be two standard configurations. When there exists a run from x to y we say that y is reachable from x and if there also exists a run from y to x we say that (x, y) is in the reversible reachability relation. The problem of deciding this last property is called the reversible reachability problem. This problem is shown to be EXPSPACE-hard by introducing the coverability problem. Given two standard configurations x and y we say that y is coverable by x if there exists a standard configuration in y + N d reachable from x. The coverability problem is known to be EXPSPACEcomplete [START_REF] Cardoza | Exponential space complete problems for Petri nets and commutative semigroups: Preliminary report[END_REF][START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF]. By reducing the coverability problem to the reversible reachability problem we get the following lemma.

Lemma 3.2. The reversible reachability problem is EXPSPACE-hard.

Proof. We consider a vector addition system A. We first observe that we can add to the vector addition system A additional actions of the form (0, . . . , 0, -1, 0, . . . , 0) without modifying the coverability problem. Thanks to this transformation a standard configuration y is coverable from a standard configuration x if and only if y is reachable from x. We introduce the VAS V in dimension d + 2 defined by V = ((0, 0

) × A) ∪ {(-1, 1, -y), (1, -1, x)}.
Let us prove that (1, 0, x) and (0, 1, 0) are in the reversible reachability relation of V if and only if y is coverable from x in A. In fact if y is coverable from x in A, then y is reachable from x thanks to the additional actions (0, . . . , 0, -1, 0, . . . , 0). Hence there exists a run from x to y labelled by a word a 1 . . . a k of actions a j ∈ A. The following runs shows that (1, 0, x) and (0, 1, 0) are in the reversible reachability relation of V:

(1, 0, x) (0,0,a 1 )...(0,0,a k ) ----------→ (1, 0, y)

(-1,1,-y) ------→ (0, 1, 0) (1,-1,x) -----→ (1, 0, x)
Converselly, let us assume that (1, 0, x) and (0, 1, 0) are in the reversible reachability relation of V. Hence there exists a run from (1, 0, x) to (0, 1, 0) labelled by a word σ. We consider the maximal prefix w of σ in ((0, 0) × A) * . This word has the special form w = (0, 0, a 1 ) . . . (0, 0, a k ). Observe that w is the label of a run from (1, 0, x) to a standard configuration of the form (1, 0, z). We deduce that a 1 . . . a k is a the label of run in A from x to z. Moreover, since (1, 0, z) = (0, 1, 0) we deduce that w is a strict prefix of σ. Let v ∈ V such that wv is a prefix of σ. By maximality of σ we deduce that v ∈ {(-1, 1, -y), (1, -1, x)}. Since (1, 0, z) + v ≥ 0, we get v = (-1, 1, -y). Thus z ≥ y and we have proved that y is coverable from x in A.

(1, 1, 0) (0, 2, 1) (1, 0, 1) (0, 1, 2) (-1, 1, 1) (1, -1, -1) (1, -1, -1) (0, -1, 1) (0, 1, -1) (1, ⋆, ⋆) (0, ⋆, ⋆) (-1, 1, 1) (1, -1, -1) (0, -1, 1) (0, 1, -1)
As a direct consequence, the reversible reachability problem is EXPSPACE-hard.

SUBREACHABILITY GRAPHS

A subreachability graph is a graph G = (Q, T ) where Q ⊆ N d I is a non empty finite set of configurations called states and

T ⊆ Q × A × Q is a finite set of triples (x, a, y) ∈ Q × A × Q satisfying x a -→ y called transitions.
The set I is called the set of projected components of G and the subreachability graph is said to be standard if I is empty. A witness graph is a strongly connected subreachability graph (see Fig. 1 for examples). The projection π L (t) of a transition t = (x, a, y) by eliminating components indexed by L ⊆ {1, . . . , d} is defined by π L (t) = (π L (x), a, π L (y)) and the projection of the set of transitions T is defined by π

L (T ) = {π L (t) | t ∈ T }. The projection π L (G) of a subreachability graph G = (Q, T ) is the subreachability graph π L (G) = (π L (Q), π L (T )).
Example 4.1. A standard subreachability graph G = (Q, T ) and the subreachability graph π L (G) obtained from G by eliminating components indexed by L = {2, 3} are depicted in Fig. 1.

A path in a subreachability graph G from a configuration x ∈ Q to a configuration y ∈ Q labelled by a word σ = a 1 . . . a k of actions a j ∈ A is a word p = t 1 . . . t k of transitions t j ∈ T of the form t j = (c j-1 , a j , c j ) with c 0 = x and c k = y.
We observe that the word p is unique. This path is denoted by

x σ -→ G y. Let us observe that in this case ρ = c 0 . . . c k is the unique run x σ -→ y.
In particular if a path x σ -→ G y exists then the run x σ -→ y also exists. Note that conversely if there exists a run x σ -→ y then there exists a subreachability G such that x σ -→ G y. Such a G is obtained by introducing the set of states Q = {c 0 , . . . , c k } and the set of transitions T = {t 1 , . . . , t k } where

t j = (c j-1 , a j , c j ). A path x σ -→ G y is called a cycle if x = y. The cycle is said to be simple if c j 1 = c j 2 with j 1 < j 2 implies j 1 = 0 and j 2 = k. The projection π L (p) of a path p = t 1 . . . t k in G by eliminating components indexed by L ⊆ {1, . . . , d} is the path π L (p) = π L (t 1 ) . . . π L (t k ) in π L (G). Observe that the projection of a path x σ -→ G y by eliminating components indexed by L is the path π L (x) σ -→ π L (G) π L (y).
The Parikh image of a path is the function µ : T → N defined by µ(t) is the number of occurrences of t in this path. A cycle is said to be total if its Parikh image µ satisfies µ(t) ≥ 1 for every t ∈ T .

Example 4.2. Let us come back to the standard witness graph G depicted in Fig. 1. Let us consider the cycle (1, 1, 0)

(-1,1,1)(1,-1,-1) -----------→ G (1, 1, 0) in G. Its projection by eliminating components indexed by L = {2, 3} is the cycle (1, ⋆, ⋆) (-1,1,1)(1,-1,-1) -----------→ π L (G) (1, ⋆, ⋆) in the witness graph π L (G) also depicted in Fig. 1. A word σ ∈ A * is said to be forward iterable from a configuration c if there exists a run c σ -→ y such that c ≤ y. In this case the configuration c ⋆ = π L (c) where L = {i | c(i) = y(i)} is called the forward limit of σ from c.
We observe that σ is forward iterable from c if and only if for every n ∈ N there exists a run c σ n -→ y n . In that case L is the minimal set of indexes such that π L (y n ) does not depend on n. Symmetrically σ is said to be backward iterable from a configuration c if there exists a run

x σ -→ c such that c ≤ x. In this case the configuration c ⋆ = π L (c) where L = {i | c(i) = x(i)} is called the backward limit of σ from c. Example 4.3. The action a = (0, -1, 1) is forward iterable from x = (0, ⋆, 0) since (0, ⋆, 0) a -→ (0, ⋆, 1). Observe that in this case (0, ⋆, 0) a n -→ (0, ⋆, n) for every n ∈ N. The forward limit of a from (0, ⋆, 0) is (0, ⋆, ⋆).
A configuration c is said to be forward pumpable by a cycle q σ -→ G q if σ is forward iterable from c with a forward limit equals to q. Note that in this case q is unique since it satisfies q = π I (c) where I is the set of projected components of G. Symmetrically a configuration c is said to be backward pumpable by a cycle q σ -→ G q if σ is backward iterable from c with a backward limit equals to q.

Example 4.4. Let us come back to the witness graph π L (G) depicted in Fig. 1. Observe that (0, ⋆, 0) is forward pumpable by (0, ⋆, ⋆)

(0,-1,1) -----→ π L (G) (0, ⋆, ⋆).

OUTLINE

The remainder of this paper is a proof that the reversible reachability problem is in EXPSPACE. We prove that if a pair (x, y) of standard configurations are in the reversible reachability relation then there exist runs from x to y and from y to x with lengths bounded by a number double exponential in the size of (x, A, y) with the binary encoding for numbers. Using the fact that NEX-PSPACE=EXPSPACE, and that double exponential numbers can be stored in exponential space, one obtain the EXPSPACE upper bound. These "short" runs are obtained as follows.

Theorem 6.2 gives a bound on the size of the Parikh image of a cycle in a witness graph to achieve a particular displacement vector, using a result of Pottier [START_REF] Pottier | Minimal solutions of linear diophantine systems: Bounds and algorithms[END_REF]. This result is used in Section 7, which considers the special case of reversible witness graphs in which each path can be followed by another path such that the total displacement is zero. In Theorem 7.2 it is shown that a reversible witness graph possesses a "short" total cycle that has a zero displacement.

Section 9 takes an arbitrary witness graph G and asserts the existence of a set of indexes J such that the witness graph π J (G) has a "small" number of states and such that states q of G that are not "too" large are forward and backward pumpable by "short" cycles in π J (G).

The development culminates with the main result in Section 10. There, we consider a reversible witness graph where x and y are two states. This graph is finite but potentially very large. One then uses the result from Section 9 to generate a reversible witness graph π J (G) satisfying the previous conditions in such a way that x and y can be considered as not "too" large configurations. Most of the work involves showing how to replace arbitrary path between x and y by "short" paths by exploiting the fact that x and y are pumpable to move from π J (G) back to G.

DISPLACEMENT VECTORS

A displacement vector of a witness graph G is a finite sum of vectors of the form ∆(σ) = k j=1 a j where σ = a 1 . . . a k is a word labelling a cycle in G. We denote by Z G the set of displacement vectors. Observe that Z G is a submonoid of (Z d , +). Displacement vectors are related to Kirchhoff functions as follows. A Kirchhoff function for a witness graph As a direct consequence of the Euler's Lemma, we deduce that a vector z ∈ Z d is a displacement vector of G if and only if there exists a Kirchhoff function µ for G satisfying the following equality:

G = (Q, T ) is a function µ : T → N such that the functions in(µ), out(µ) : Q → N defined bellow are equal. in(µ)(x) = t∈T ∩(Q×A×{x}) µ(t) out(µ)(x) = t∈T ∩({x}×A×Q) µ(t) A Kirchhoff function µ : T → N is said to be total if µ(t)
z = t=(x,a,y)∈T µ(t)a
In this case z is called the displacement of µ.

Example 6.1. Let us come back to the witness graph π L (G) depicted in Fig. 1

. A function µ : π L (T ) → N is a Kirchhoff function for π L (G) if and only if µ(t 1 ) = µ(t 2 ) where t 1 = ((1, ⋆, ⋆), (-1, 1, 1), (0, ⋆, ⋆)) and t 2 = ((0, ⋆, ⋆), (1, -1, -1), (1, ⋆, ⋆)). In particular the set of displacement vectors of π L (G) satisfies Z π L (G) = {z ∈ Z 3 | z(1) = 0 ∧ z(2) + z(3) = 0}.
The following theorem shows that the displacement vectors z ∈ Z G are displacement of Kirchhoff functions µ for G such that ||µ|| ∞ = max t∈T µ(t) is bounded by a polynomial in |Q|, ||A|| ∞ , and ||z|| ∞ with a degree depending on d. Theorem 6.2. Vectors z ∈ Z G are displacement of Kirchhoff functions µ such that the following inequality holds where q = |Q|, a = ||A|| ∞ , and m = ||z|| ∞ :

||µ|| ∞ ≤ (q d+1 a(1 + 2a) d + m) d
Proof. We first recall a "Frobenius theorem" proved in [START_REF] Pottier | Minimal solutions of linear diophantine systems: Bounds and algorithms[END_REF]. Let H ∈ Z d×n be a matrix and let us denote by h i,j for each i ∈ {1, . . . , d} and j ∈ {1, . . . , n} the element of H at position (i, j). We denote by ||H|| 1,∞ the natural number max 1≤i≤d n j=1 |h i,j |. Given a vector v ∈ N n , we introduce the natural number ||v|| 1 = n j=1 v(j). Let V be the set of vectors v ∈ N n such that Hv = 0. Recall that V is a submonoid of (N n , +) generated by the finite set min(V\{0}) of minimal elements for ≤. From [START_REF] Pottier | Minimal solutions of linear diophantine systems: Bounds and algorithms[END_REF] we deduce that vectors v ∈ min(V\{0}) satisfy the following inequality where r is the rank of H:

||v|| 1 ≤ (1 + ||H|| 1,∞ ) r
Observe that if a = 0 then z = 0 and the theorem is proved with the Kirchhoff function µ defined by µ(t) = 0 for every t ∈ T . So we can assume that a ≥ 1. Since every cycle labelled by a word σ can be decomposed into a finite sequence of simple cycles labelled by words σ 1 , . . . , σ k such that ∆(σ) = k j=1 ∆(σ j ) we deduce that the set of displacement vectors Z G is the submonoid of (Z d , +) generated by the set Z of non-zero vectors z = ∆(σ) where σ is the label of a simple cycle. Since the length of a simple cycle is bounded by the cardinal q of Q, we get ||Z|| ∞ ≤ qa. As a corollary we deduce that the cardinal k of Z is bounded by k ≤ (1 + 2qa) d -1 (the -1 comes from the fact that vectors in Z are non-zero).

Let us consider a vector z ∈ Z G and let us introduce a whole enumeration z 1 , . . . , z k of the vectors in Z and the following set V where n = k + 1:

V = {v ∈ N n | d i=1 k j=1 v(j)z j (i) -v(n)z(i) = 0}
We observe that V is associated to a matrix H ∈ Z d×n . The rank of H is bounded by d and ||H|| 1,∞ ≤ kqa + m. We deduce from the Frobenius theorem that vectors v ∈ min(V\{0}) satisfy the following inequality:

||v|| 1 ≤ (1 + kqa + m) d ≤ (q d+1 a(1 + 2a) d + m) d Since z ∈ Z G
and Z G is the submonoid generated by (Z d , +) generated by z 1 , . . . , z k , we deduce that there exists v 1 , . . . , v k ∈ N such that z = k j=1 v j z j . Observe that the vector v ∈ N n defined by v(j) = v j if j ∈ {1, . . . , k} and v(n) = 1 is in V. Hence, there exists v ∈ V such that v(n) = 1. In particular there exists another vector v ∈ min(V\{0}) such that v(n) = 1. Observe that for every j ∈ {1, . . . , k} there exists a function λ j that is the Parikh image of a simple cycle such that z j is the displacement of λ j . We introduce the Kirchhoff function µ = k j=1 v(j)λ j . Since v ∈ V and v(n) = 1 we deduce that the displacement of µ is z. The theorem is proved by observing that µ(t) = k j=1 v(j)λ j (t) ≤ ||v|| 1 since λ j (t) ∈ {0, 1}.

REVERSIBLE WITNESS GRAPHS

A witness graph G is said to be reversible if for every path x u -→ G y there exists a path y v -→ G x such that ∆(u) + ∆(v) = 0. Observe that standard witness graphs are reversible since the condition ∆(u) + ∆(v) = 0 is implied by the two paths. Let us recall that a submonoid Z of (Z d , +) is said to be a subgroup if -z ∈ Z for every z ∈ Z.

The following lemma provides two characterizations of the reversible witness graphs.

Lemma 7.1. A witness graph G is reversible if and only if Z G is a subgroup of (Z d , +) if and only if the zero vector is the displacement of a total Kirchhoff function.

Proof. Assume first that G is reversible and let us prove that Z G is a subgroup of (Z d , +). Let us consider a cycle x u -→ G x. Since G is reversible, there exists a cycle x v -→ G x such that ∆(u) + ∆(v) = 0. We deduce that -Z G = Z G since vectors in Z G are finite sums of vectors ∆(u) where u is the label of a cycle in G. Therefore Z G is a subgroup of Z d . Now let us assume that Z G is a subgroup of (Z d , +) and let us prove that the zero vector is the displacement of a total Kirchhoff function. Since G is strongly connected, there exists a total cycle

x u -→ G x. Observe that z = ∆(u) is in Z G . Since Z G is a subgroup we deduce that -z ∈ Z G .
Hence -z is the displacement of a Kirchhoff function λ. Let λ ′ be Parikh image of x u -→ G x and observe that µ = λ+λ ′ is a total Kirchhoff function. Moreover the displacement of µ is -z+z = 0.

Finally, let us assume that the zero vector is the displacement of a total Kirchhoff function µ and let us prove that G is reversible. Let us consider a path x The following theorem shows that if G is a reversible witness graph then the zero vector is the displacement of a total Kirchhoff function µ such ||µ|| ∞ can be bounded by a polynomial in |Q| and ||A|| ∞ with a degree depending on d.

Theorem 7.2. Let G be a reversible witness graph. The zero vector is the displacement of a total Kirchhoff function µ such that the following inequality holds where q = |Q| and a = ||A|| ∞ :

||µ|| ∞ ≤ (q(1 + 2a)) d(d+1)
Proof. Since G is strongly connected, every transition t ∈ T occurs in at least one simple cycle. We denote by λ t the Parikh image of such a simple cycle and we introduce the Kirchhoff function λ = t∈T λ t . We have λ(t) ∈ {1, . . . , |T |} for every t ∈ T . We introduce the displacement z of λ. Since G is reversible, we deduce that -z is the displacement vector of a Kirchhoff function for G by Lemma 7.1. As ||z|| ∞ ≤ |T |qa, |T | ≤ q|A|, and |A| ≤ (1 + 2a) d we deduce that ||z|| ∞ ≤ q 2 a(1 + 2a) d . Theorem 6.2 shows that -z is the displacement of a Kirchhoff function λ ′ satisfying the following inequalities:

||λ ′ || ∞ ≤ (q d+1 a(1 + 2a) d + q 2 a(1 + 2a) d ) d ≤ (q d+1 2a(1 + 2a) d ) d
Let us consider the total Kirchhoff function µ = λ + λ ′ . Observe that the displacement of µ is the zero vector and since ||λ|| ∞ ≤ |T | ≤ q(1 + 2a) d ≤ (q d+1 (1 + 2a) d ) d we get the theorem with:

||µ|| ∞ ≤ (q d+1 2a(1 + 2a) d ) d + (q d+1 (1 + 2a) d ) d ≤ (q(1 + 2a)) d(d+1)

EXTRACTORS

In this section we introduce a way for extracting "large" components of configurations. An extractor is a non increasing sequence λ = (λ n ) 1≤n≤d of natural numbers λ n ∈ N. Let X ⊆ N d I . An excluding set for (λ, X) is a set of indexes J such that x(i) < λ |J|+1 for every i ∈ J and for every x ∈ X (notice that even if λ d+1 is not defined, when |J| = d the domain of the universal quantifier "for every i ∈ J" is empty). Since λ is non increasing we deduce that the class of excluding sets for a couple (λ, X) is stable by intersection. As this class contains {1, . . . , d} we deduce that there exists a unique minimal excluding set J for (λ, X). By minimality of this set we deduce that for every i ∈ J there exists x ∈ X such that x(i) ≥ λ |J| (notice once again that even if λ 0 is not defined, when |J| = 0 the domain of the universal quantifier "for every i ∈ J" is empty). We denote λ(X) the set π J (X) where J is the minimal excluding set for (λ, X).

Example 8.1. Let λ = (5, 3, 2) be an extractor. We have λ({(1, 8, 1)}) = {(1, ⋆, 1)}, and λ({(1, 8, 1), (3, 1, 1)}) = {(⋆, ⋆, 1)}.

A set X ⊆ N d I is said to be normalized for λ if λ(X) = X. As a direct consequence of the following lemma we deduce that λ(X) is normalized for λ for every set X ⊆ N d I . We say that x ∈ N d I is normalized for λ if {x} is normalized for λ, i.e λ({x}) = {x} or equivalently x(i) < λ |I|+1 for every i ∈ I. Observe that if every state x ∈ X is normalized then λ(X) = X.

Lemma 8.1. Let X ⊆ N d I and let L be a set of indexes included in the minimal excluding set of (λ, X). Then λ(X) = λ(π L (X)).

Proof. Note that if X is empty the result is immediate so we can assume that X is non empty. Let J be the minimal excluding set of (λ, X) and observe that J is an excluding set for X ′ = π L (X). In particular the minimal excluding set J ′ for X ′ satisfies J ′ ⊆ J. Since J ′ is an excluding set of (λ, X ′ ) we deduce that x ′ (i) < λ |J ′ |+1 for every i ∈ J ′ . Hence π L (x)(i) < λ |J ′ |+1 for every x ∈ X. As x ≤ π L (x) we deduce that J ′ is an excluding set of (λ, X). By minimality of J we get the other inclusion J ⊆ J ′ . Thus J = J ′ and we have proved that λ(X) = λ(π L (X)).

PUMPABLE CONFIGURATIONS

In this section we show that for arbitrary witness graph G, there exists a set J of indexes such that the number of states of π J (G) is "small" and such that states with "small" size of G are pumpable by "short" cycles of π J (G). The proof of this result is inspired by the Rackoff ideas [START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF]. All other results or definitions introduced in this section are not used in the sequel.

Theorem 9.1. Let G be a witness graph with a set of states Q ⊆ N d I , and let s ∈ N >0 be a positive integer. We introduce the positive integer x = (1 + ||A|| ∞ )s. There exists a set of indexes J such that the number of states of π J (G) is bounded by x d d and such that every state q ∈ Q such that ||q|| ∞ < s is forward and backward pumpable by cycles of π J (G) with lengths bounded by dx d d .

Such a set J is obtained by introducing the class of adapted extractors. An extractor λ is said to be adapted if the following inequality holds for every n ∈ {2, . . . , d}:

λ n-1 ≥ λ d-n+1 n ||A|| ∞ + λ n
Lemma 9.2. Let λ be an adapted extractor, G be a witness graph with a set of states Q ⊆ N d I , and let J be the minimal excluding set for (λ, Q). For every state q ∈ Q there exists a run q u -→ y such that π J (q) u -→ π J (G) π J (y) and such that the bounds |u| ≤ |I|<n≤|J| λ d+1-n n , and y(j) ≥ λ |J| for every j ∈ J hold.

Proof. Since Q ⊆ N d I we deduce that I ⊆ J. We introduce a parameter k ∈ N and we prove the lemma by induction over k under the constraint |J| -|I| ≤ k. Observe that if k = 0 then I = J and the property is proved with u = ǫ and y = q. Assume the property proved for a natural number k ∈ N and let us consider a witness graph G = (Q, T ) with a set of projected components I such that |J| -|I| ≤ k + 1 where J is the minimal excluding set for (λ, Q). We consider a state q ∈ Q. If Q is normalized for λ then J = I and the property is proved. So we can assume that Q is not normalized for λ. We deduce that there exists a state in Q that is not normalized. Since G is strongly connected, there exists a path q σ -→ G p with a minimal length such that p is not normalized. Let us observe that the number of states in Q that are normalized is bounded by λ We introduce the minimal excluding set K for (λ, {p}). Observe that I is strictly included in K since p is not normalized. Moreover K is included in J since J is an excluding set for (λ, {p}). Lemma 8.1 shows that J is the minimal excluding set of (λ, π K (Q)). Observe that |J| -|K| < |J| -|I| ≤ k + 1. By applying the induction on the witness graph π K (G) and the state π K (p), we deduce that there exists a run π K (p)

u -→ y such that π J (p) u -→ π J (G) π J (y) with |u| ≤ |K|<n≤|J| λ d+1-n n
and such that y(j) ≥ λ |J| for every j ∈ J. We introduce the word

v = σu. Since I is strictly included in K we deduce that |I|<n≤|K| λ d+1-n n ≥ λ d-|I| |I|+1 . Thus |v| ≤ |I|<n≤|J| λ d+1-n n . Since λ is an adapted extractor we deduce that λ |K| ≥ ||A|| ∞ |K|<n≤|J| λ d+1-n n +λ |J| . From p(k) ≥ λ |K| for every k ∈ K we deduce that p(k) ≥ ||A|| ∞ |u| + λ |J| .
Since there exists a run from π K (p) labelled by u, Lemma 3.1 shows that there exists a run

p u -→ z. For every k ∈ K we have z(k) ≥ p(k) -||A|| ∞ |u| ≥ λ |J| . As p u -→ z we deduce that π K (p) u -→ π K (z). In particular π K (z) = y. Let j ∈ J\K.
From the previous equality we get z(j) = y(j). Moreover since y(j) ≥ λ |J| we get z(j) ≥ λ |J| . We have proved that z(j) ≥ λ |J| for every j ∈ J. Hence the induction is proved. Now let us prove Theorem 9.1. We consider a witness graph G with a set of states Q ⊆ N d I . We also consider a positive integer s ∈ N >0 and we introduce the positive integers a = ||A|| ∞ and x = (1 + a)s. Let λ be the adapted extractor defined by λ d = s and the following induction for every n ∈ {2, . . . , d}:

λ n-1 = λ d n (1 + ||A|| ∞ ) An immediate induction provides λ d+1-n n ≤ x d d for every n ∈ {1, . . . , d}. We introduce the minimal excluding set J for (λ, Q). Observe that if |J| = d then |π J (Q)| = 1 and in particular |π J (Q)| ≤ x d d . If |J| < d, the number of states in π J (Q) is bounded by λ d-|J| |J|+1 . Hence |π J (Q)| ≤ x d d
in any case. Let us consider q ∈ Q such that ||q|| ∞ < s. Lemma 9.2 shows that there exists a run q σ -→ x with x(j) ≥ λ |J| for every j ∈ J such that π J (q) σ -→ π J (G) π J (x) and such that:

|σ| ≤ |J| n=1 λ d+1-n n Since π J (G) is strongly connected there exists a path π J (x) u -→ π J (G) π J (q)
. We can assume that the length of u is minimal. In particular u = ǫ if J = {1, . . . , d} and |u| ≤ λ d-|J| |J|+1 otherwise. In both case |σu| ≤ dx d d . Since λ is an adapted extractor we deduce that x(j) ≥ |u| ||A|| ∞ for every j ∈ J and by applying Lemma 3.1 we deduce that there exists a run x u -→ y. Since π J (x) u -→ π J (q) we deduce that y(j) = q(j) for every j ∈ J. Moreover if j ∈ J\I since y(j) ≥ s and s > ||q|| ∞ we get y(j) > q(j). We deduce that q ≤ y and J\I = {i | q(i) = y(i)}. Therefore q is forward pumpable by the cycle π J (q) σu -→ π J (G) π J (q). Symmetrically we prove the backward case. We have proved Theorem 9.1.

DECIDING THE REVERSIBILITY PROBLEM

In this section, the reversible reachability problem is proved to be EXPSPACE-complete. The proof is inspired by the Kosaraju ideas [START_REF] Kosaraju | Decidability of reachability in vector addition systems (preliminary version)[END_REF]. A word α ∈ A * is said to be reversible on a configuration p if there exists a word β ∈ A * such that p αβ --→ p and ∆(α) + ∆(β) = 0. Note that if p is a standard configuration the last condition is implied by the first one.

Theorem 10.1. Let α ∈ A * be a reversible word on a configuration p. There exists another word α ′ ∈ A * reversible on p such that ∆(α) = ∆(α ′ ) and such that:

|α ′ | ≤ 17d 2 x 15d d+2 where x = (1 + 2||A|| ∞ ) (1 + ||p|| ∞ + ||∆(α)|| ∞ ).
Let us assume that α ∈ A * is a reversible word on a configuration p ∈ N d I . There exists a run p αβ --→ p satisfying ∆(α)+∆(β) = 0. From this run we extract a unique witness graph G = (Q, T ) such that p αβ --→ G p is a total cycle. In particular the Parikh image of this cycle is a total Kirchhoff function proving that G is reversible by Lemma 7.1.

We introduce a = ||A|| ∞ and s

= 1 + ||p|| ∞ + ||∆(α)|| ∞ . Let q = p + ∆ I (α). We have ||q|| ∞ ≤ ||p|| ∞ + ||∆(α)|| ∞ < s.
Let us introduce x = (1 + 2a)s. Theorem 9.1 shows that there exists a set of indexes J such that π J (G) has at most x d d states and such that p is forward pumpable by a cycle π J (p) v -→ π J (G) π J (p) and q is backward pumpable by a cycle π J (q) w -→ π J (G) π J (q) such that |v|, |w| ≤ dx d d . In particular ∆ I (v) and -∆ I (w) are two vectors in {c ∈ N d I | c(i) = 0 ⇔ i ∈ J}. For every n ∈ N we have:

p v n -→ p + n∆ I (v)
q -n∆ I (w)

w n --→ q Since the witness graph G is reversible, Lemma 7.1 shows that π J (G) is reversible. From Theorem 7.2 we deduce that the zero vector is the displacement of a total Kirchhoff function µ for π J (G) satisfying:

||µ|| ∞ ≤ (x d d (1 + 2a)) d(d+1) ≤ (x d d x) 2d 2 ≤ (x 2d d ) 2d 2 ≤ x 4d d+2 Note that |π J (T )| ≤ |π J (Q)| |A| ≤ x d d (1 + 2a) d ≤ x 2d d .
Lemma 10.2. There exists a cycle π J (q) u -→ π J (G) π J (q) such that ∆(v) + ∆(u) + ∆(w) = 0 and:

|u| ≤ 3d x 7d d+2
Proof. Let µ v , µ w be the Parikh images of π J (p) v -→ π J (G) π J (p) and π J (q) w -→ π J (G) π J (q). We introduce the function λ = (1 + 2dx d d )µ -(µ v + µ w ). Observe that λ is a Kirchhoff function for π J (G) satisfying λ(t) ≥ (1 + 2dx d d ) -2dx d d ≥ 1 for every t ∈ π J (T ). The Euler's Lemma shows that λ is the Parikh image of a total cycle π J (q) u -→ π J (G) π J (q). Observe that ∆(u) =

(1 + 2dx d d )0 -(∆(v) + ∆(w)). Hence ∆(v) + ∆(u) + ∆(w) = 0. The length of u is bounded by:

|u| = t∈π J (T ) (1 + 2dx d d )µ(t) -(µ v (t) + µ w (t)) ≤ 3dx d d ||µ|| ∞ |π J (T )| ≤ 3dx 7d d+2
Lemma 10.3. There exists a path π J (p) α -→ π J (G) π J (q) such that ∆( α) = ∆(α) and:

| α| ≤ 2x 7d d+2
Proof. Since π J (G) is strongly connected, there exists a path π J (q) β -→ π J (G) π J (p). We can assume that | β| is minimal. In particular | β| < x d d . Moreover, we know that π J (p)

α -→ π J (G) π J (q).
Observe that α β is the label of a cycle in π J (G). Hence z = ∆(α) + ∆( β) is the displacement of a Kirchhoff function for G. We have

||z|| ∞ ≤ ||∆(α)|| ∞ + ||∆( β)|| ∞ ≤ s + | β|a we get ||z|| ∞ ≤ s + x d d a ≤ x d d (1 + a)
. Theorem 6.2 shows that z is the displacement of a Kirchhoff function θ for G such that:

||θ|| ∞ ≤ ((x d d ) d+1 a(1 + 2a) d + x d d (1 + a)) d ≤ (x 2d d+1 ax d + x d d (1 + a)) d ≤ (x 3d d+1 (1 + 2a)) d ≤ (x 3d d+1 x) d ≤ x 4d d+2
We introduce the Parikh image f of the path π J (q) β -→ π J (G) π J (p). Let us add to the strongly connected graph π J (G) an additional transition t • from π J (q) to π J (p) and let G • be this new graph and T • = π J (T ) ∪ {t • } be its set of transitions. Functions θ, µ and f are extended over T

• by θ(t • ) = µ(t • ) = f (t • ) = 0. We also introduce the Parikh image f • of t • , i.e. f • (t • ) = 1 and f • (t) = 0 for every t ∈ π J (T ). Let us observe that g = θ + x d d µ -f + f • satisfies g(t) ≥ 1 for every t ∈ π J (T ) since f (t) < x d d . A g(t • ) = 1
we deduce that g is a Kirchhoff function for G • satisfying g(t) ≥ 1 for every t ∈ T • . The Euler's Lemma shows that g is the Parikh image of a total cycle. Since g(t • ) = 1 we deduce that g is the Parikh image of a cycle of the form

(π J (p) α -→ π J (G) π J (q)) t • . By definition of g we get ∆( α) = z + x d d 0 -∆( β) + 0. Hence ∆(α) = z -∆( β). Since z = ∆(α) + ∆( β) we get ∆( α) = ∆(α).
The following inequalities provide the lemma:

| α| ≤ |π J (T )| ||θ|| ∞ + x d d |π J (T )| ||µ|| ∞ ≤ x 2d d (x 4d d+2 + x d d x 4d d+2 ) ≤ 2x 7d d+2
Lemma 10.4. For every n ≥ |u|a we have:

q + n∆ I (v) u n -→ q -n∆ I (w)
Proof. Let n ≥ |u|a. We introduce the sequence (x k ) 0≤k≤n of configurations x k = q + (nk)∆ I (v) -k∆ I (w). Since π J (x k ) = π J (q) we deduce that there exists a run from π J (x k ) labelled by u. Moreover as ∆ I (v)(j) ≥ 1 and -∆ I (w)(j) ≥ 1 for every j ∈ J, we deduce that x k (j) ≥ n ≥ |u|a for every j ∈ J. Lemma 3.1 shows that there exists a run from x k labelled by u. Since ∆(v) + ∆(u) + ∆(w) = 0 we get x k u -→ x k+1 .

Lemma 10.5. For every n ≥ |α|a we have:

p + n∆ I (v) α -→ q + n∆ I (v)
Proof. Observe that π J (p + n∆ I (v)) = π J (p) and π J (p) α -→ π J (q). Moreover for every j ∈ J we have (p + n∆ I (v))(j) ≥ n ≥ |α|a. From Lemma 3.1 we deduce that there exists a run from p + n∆ I (v) labelled by α. p α -→ q we deduce that p + ∆ I (α) = q. Since ∆(α) = ∆(α) we deduce that p + ∆ I (α) = q. We deduce the run p + n∆ I (v) α -→ q + n∆ I (v).

Finally, let n = a max{| α|, |u|}. We have proved that p α ′ -→ q where α ′ = v n αu n w n . Note that ∆(α ′ ) = ∆(α) since ∆(α) = ∆(α) and ∆(v) + ∆(u) + ∆(w) = 0. We deduce that ∆(α ′ ) = ∆(α). As q β -→ p with ∆(α) + ∆(β) = 0 we deduce that α ′ is reversible on p. Note that n ≤ a3dx 7d d+2 ≤ 3dx 8d d+2 . Hence we have:

|α ′ | ≤ 2x 7d d+2 + 3dx 8d d+2 (2dx d d + 3dx 7d d+2 ) ≤ 17d 2 x 15d d+2
We have proved Theorem 10.1.

Corollary 10.6. Two standard configurations p, q are in the same strongly connected component of a standard subreachability graph if and only if there exist runs p α -→ q and q β -→ p such that:

|α|, |β| ≤ 17d 2 x 15d d+2 where x = (1 + 2||A|| ∞ )(1 + 2 max{||p|| ∞ , ||q|| ∞ }).
Theorem 10.7. The reversible reachability problem is EXPSPACE-complete.

APPLICATION : REVERSIBILITY DOMAINS

During the execution of a VAS some actions are reversible and some not. More precisely, let D a be the set of standard configurations c such that there exists a word α satisfying c Proof. Observe that if a = 0 we are done since in this case c = 0. So we can assume that a ≥ 1. We introduce the extractor λ = (λ 1 , . . . , λ d ) defined by λ d+1 = a and the following induction for n ∈ {1, . . . , d + 1}: n by introducing e = 15d d+2 and c = 17d 2 (6a) e . Hence λ 0 ≤ (ca) e d+1 ≤ (102d 2 a 2 ) e d+2 and from e d+2 ≤ (15d d+2 ) d+2 we are done.

CONCLUSION

The reversible reachability problem is proved to be EXPSPACE-complete in this paper. The proof is inspired by the Rackoff and Kosaraju ideas [START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF][START_REF] Kosaraju | Decidability of reachability in vector addition systems (preliminary version)[END_REF]. We have introduced the domain of reversibility D a of every action a ∈ A. Observe that the reflexive and transitive closure of the following relation R is a congruence and from [START_REF] Bouziane | Cyclic Petri net reachability sets are semi-linear effectively constructible[END_REF] we deduce that this relation is definable in the Presburger arithmetic. That means there exist a Presburger formula φ that exactly denotes the pair (x, y) of standard configurations in the reversible reachability relation. As a future work we are interested in characterizing precisely the size of such a formula (we already derive an elementary bound from [START_REF] Bouziane | Cyclic Petri net reachability sets are semi-linear effectively constructible[END_REF] and Theorem 11.1).

R = a∈A {(x, x + a) | x ∈ D a }
The general vector addition system reachability problem was recently proved to be decidable thanks to inductive invariants definable in the Presburger arithmetic [START_REF] Leroux | Vector addition system reachability problem: a short self-contained proof[END_REF]. The proof is based on binary relations called transformer relations over Q d ≥0 where Q ≥0 is the set of non-negative rational numbers. The transformer relation of a standard configuration c ∈ N d is the binary relation c over Q d ≥0 defined by x c y if there exists a run from c + nx to c + ny for some n ∈ N.

This relation is proved to be definable in FO (Q, +, ≤) in [START_REF] Leroux | Vector addition system reachability problem: a short self-contained proof[END_REF]. The proof is based on witness graphs. However, no upper bound on the size of these graphs are derived. As a future work we are interested in adapting techniques introduced in this paper for proving elementary upper-bounds on sizes of formulas in FO (Q, +, ≤) denoting transformer relations. Our main objective is the complexity of the general vector addition system reachability problem.

  3. VECTOR ADDITION SYSTEMSA Vector Addition System (VAS) is a finite set A ⊆ Z d . Vectors a ∈ A are called actions and vectors c ∈ N d ⋆ with N ⋆ = N ∪ {⋆} are called configurations. A configuration in N d is said to be standard and we denote byN d I the set of configurations c ∈ N d ⋆ such that I = {i | c(i) = ⋆}.Given a word σ = a 1 . . . a k of actions a j ∈ A we denote by ∆(σ) the vector in Z d defined by ∆(σ) = k j=1 a j . This vector is called the displacement of σ. We also introduce the vector ∆ I (σ) = π I (∆(σ)). A run ρ from a configuration x ∈ N d I to a configuration y ∈ N d I labelled by a word σ = a 1 . . . a k of actions a j ∈ A is a non-empty word ρ = c 0 . . . c k of configurations c j ∈ N d I such that c 0 = x, c k = y and such that c j = c j-1 + π I (a j ) for every j ∈ {1, . . . , k}. Note that in this case ρ is unique and yx = ∆ I (σ). This run is denoted by x σ -→ y. The set I is called the set of projected components of ρ. The projection π L (ρ) of a run ρ = c 0 . . . c k by eliminating components indexed by L ⊆ {1, . . . , d} is defined as expected as the run π L

Figure 1 :

 1 Figure 1: A subreachability graph G and the subreachability graph π L (G) with L = {2, 3}.

Example 7. 1 .

 1 Witness graphs depicted in Fig. 1 are reversible. The witness graph ({⋆}, {(⋆, 1, ⋆)}) is not reversible.

u-→

  G y. Since G is strongly connected, there exists a path y α -→ G x. Let us consider the Parikh image λ of the cycle x uα -→ G x and let m = 1 + ||λ|| ∞ . We observe that µ ′ = mµλ is a total Kirchhoff function and the Euler's Lemma shows that µ ′ is the Parikh image of a cycle x β -→ G x. From µ ′ = mµλ we deduce that ∆(β) = m0 -∆(uα). Let us consider v = αβ and observe that y v -→ G x and ∆(u) + ∆(v) = 0. Thus G is reversible.

  minimality of the length of σ we deduce that |σ| ≤ λ d-|I| |I|+1 .

a-

  → c + a α -→ c. We observe that the set D a is an upward closed set for the order ≤. In fact c a -→ c + a α -→ c implies the same thing by replacing c with a standard configuration x ∈ c + N d . So D a is characterized by its finite set of minimal elements min(D a ) for ≤. As an application of Theorem 10.1, we obtain the following result. Theorem 11.1. Configurations c ∈ min(D a ) satisfy the following inequality where a = ||A|| ∞ .||c|| ∞ ≤ (102d 2 a 2 ) (15d d+2 ) d+2

  λ n-1 = 17d 2 (6aλ n ) 15d d+2 Let c ∈ min(D a ) and let d = c + a. Let us consider the minimal excluding set I for (λ, {d}). By minimality of I we have d(i) < λ |I|+1 for every i ∈ I and d(i) ≥ λ |I| for every i ∈ I. We consider the standard configuration y defined by y(i) = λ |I| if i ∈ I and y(i) = d(i) if i ∈ I. Let us consider q = π I (c) and p = π I (d). Since c ∈ D a there exists a run d α -→ c. In particular p α -→ q a -→ p with ∆(α) + ∆(a) = 0.We deduce that α is reversible on p and Theorem 10.1 shows that there exists a word α ′ such that p α ′ -→ q, ∆(α ′ ) = ∆(α) and:|α ′ | ≤ 17d 2 x 15d d+2 where x = (1 + 2a)(1 + ||p|| ∞ + ||a|| ∞ ). Note that ||p|| ∞ ≤ λ |I|+1 -1. We deduce that x ≤ (1 + 2a)(λ |I|+1 + a) ≤ 6aλ |I|+1 since 1 ≤ aand a ≤ λ |I|+1 . Hence a|α ′ | ≤ λ |I| thanks to the induction defining λ. Since π I (y) = p we deduce that there exists a run from π I (y) labelled by α ′ . As y(i) ≥ λ |I| ≥ a|α ′ | for every i ∈ I, Lemma 3.1 shows that there exists a run y α ′ -→ x. Since ∆(α ′ ) = ∆(α) = -a we deduce that x = ya. From y ≤ d we get x ≤ c by subtracting a. Moreover as x a -→ y α ′ -→ x we deduce that x ∈ D a . By minimality of c we get c = x. Hence c = ya. In particular ||c|| ∞ ≤ λ |I| + a ≤ λ 0 + a. Finally let us get a bound on λ 0 . We get the equality λ n-1 = cλ e

  Let z ∈ Z d I . We denote by ||z|| ∞ the natural number equals to 0 if I = {1, . . . , d} and equals to max i ∈I |z(i)| otherwise. Given a finite set Z ⊆ Z d I we denote by ||Z|| ∞ the natural number max z∈Z ||z|| ∞ if Z is non empty and 0 if Z is empty.

Work funded by ANR grant REACHARD-ANR-11-BS02-001.


Jérôme Leroux

Acceleration For Petri Nets

The reachability problem for Petri nets is a central problem of net theory. The problem is known to be decidable by inductive invariants definable in the Presburger arithmetic. When the reachability set is definable in the Presburger arithmetic, the existence of such an inductive invariant is immediate. However, in this case, the computation of a Presburger formula denoting the reachability set is an open problem. Recently this problem got closed by proving that if the reachability set of a Petri net is definable in the Presburger arithmetic, then the Petri net is flat, i.e. its reachability set can be obtained by runs labeled by words in a bounded language. As a direct consequence, classical algorithms based on acceleration techniques effectively compute a formula in the Presburger arithmetic denoting the reachability set.

Introduction

Petri Nets are one of the most popular formal methods for the representation and the analysis of parallel processes [START_REF] Esparza | Decidability issues for petri nets -a survey[END_REF]. The reachability problem is central since many computational problems (even outside the realm of parallel processes) reduce to this problem. Sacerdote and Tenney provided in [START_REF] Sacerdote | The decidability of the reachability problem for vector addition systems (preliminary version)[END_REF] a partial proof of decidability of this problem. The proof was completed in 1981 by Mayr [START_REF] Mayr | An algorithm for the general petri net reachability problem[END_REF] and simplified by Kosaraju [START_REF] Kosaraju | Decidability of reachability in vector addition systems (preliminary version)[END_REF] from [START_REF] Mayr | An algorithm for the general petri net reachability problem[END_REF][START_REF] Sacerdote | The decidability of the reachability problem for vector addition systems (preliminary version)[END_REF]. Ten years later [START_REF] Luc | A structure to decide reachability in petri nets[END_REF], Lambert provided a further simplified version based on [START_REF] Kosaraju | Decidability of reachability in vector addition systems (preliminary version)[END_REF]. This last proof still remains difficult and the upper-bound complexity of the corresponding algorithm is just known to be non-primitive recursive. Nowadays, the exact complexity of the reachability problem for Petri nets is still an open-question. Even an Ackermannian upper bound is open (this bound holds for Petri nets with finite reachability sets [START_REF] Figueira | Ackermannian and primitive-recursive bounds with dickson's lemma[END_REF]).

Basically, a Petri net is a pair (T, c init ) where T ⊆ N d × N d is a finite set of transitions, and c init ∈ N d is the initial configuration. A vector c ∈ N d is called a configuration. Given a transition t = (p, q), we introduce the binary relations t -→ over the configurations defined by x t -→ y if there exists v ∈ N d such that x = p + v and y = q + v. Notice that in this case yx is the vector qp. This vector is called the displacement of t, and it is denoted by ∆(t). Let σ = t 1 . . . t k be a word of transitions t j ∈ T . We denote by ∆(σ) = k j=1 ∆(t j ), the displacement of σ. We introduce the binary relation Example 1.1. The Petri net depicted in Figure 1 was introduced in [START_REF] Hopcroft | On the reachability problem for 5dimensional vector addition systems[END_REF] as an example of Petri net having a reachability set which cannot be defined by a formula in the logic FO (N, +), called the Presburger arithmetic. In fact, the reachability set is equal to:

(p 1 , p 2 , p 3 , p 4 , p 5 ) ∈ N 5 | ( p 1 = 1 ∧ p 4 = 0 ∧ 1 ≤ p 2 + p 3 ≤ 2 p5 ) ∨ ( p 1 = 0 ∧ p 4 = 1 ∧ 1 ≤ p 2 + 2p 3 ≤ 2 p5+1 )
Recently, in [START_REF] Leroux | The general vector addition system reachability problem by Presburger inductive invariants[END_REF], the reachability sets of Petri nets were proved to be almost semilinear, a class of sets that extends the class of Presburger sets (the sets definable in FO (N, +)) inspired by the semilinear sets [START_REF] Ginsburg | Semigroups, Presburger formulas and languages[END_REF]. Note that in general reachability sets are not definable in the Presburger arithmetic [START_REF] Hopcroft | On the reachability problem for 5dimensional vector addition systems[END_REF] (see Example 1.1). An application of the almost semilinear sets was provided; a final configuration is not reachable from an initial one if and only if there exists a forward inductive invariant definable in the Presburger arithmetic that contains the initial configuration but not the final one. Since we can decide if a Presburger formula denotes a forward inductive invariant, we deduce that there exist checkable certificates of non-reachability in the Presburger arithmetic. In particular, there exists a simple algorithm for deciding the general Petri net reachability problem based on two semi-algorithms. A first one that tries to prove the reachability by enumerating finite sequences of actions and a second one that tries to prove the non-reachability by enumerating Presburger formulas. Such an algorithm always terminates in theory but in practice an enumeration does not provide an efficient way for deciding the reachability problem. In particular the problem of deciding efficiently the reachability problem is still an open question.

When the reachability set is definable in the Presburger arithmetic, the existence of checkable certificates of non-reachability in the Presburger arithmetic is immediate since the reachability set is a forward inductive invariant (in fact the most precise one). The problem of deciding if the reachability set of a Petri is definable in the Presburger arithmetic was studied twenty years ago independently by Dirk Hauschildt during his PhD [START_REF] Hauschildt | Semilinearity of the Reachability Set is Decidable for Petri Nets[END_REF] and Jean-Luc Lambert. Unfortunately, these two works were never published. Moreover, from these works, it is difficult to deduce a simple algorithm for computing a Presburger formula denoting the reachability set when such a formula exists.

For the class of flat Petri nets [START_REF] Fribourg | Petri nets, flat languages and linear arithmetic[END_REF][START_REF] Leroux | Flat counter automata almost everywhere![END_REF], such a computation can be performed with accelerations techniques. A Petri net (T, c init ) is said to be flat if there exist some words σ 1 , . . . , σ k ∈ T * such that for every reachable configuration c, there exists a word

σ ∈ σ * 1 . . . σ * k such that c init σ -→ c. (A language included in σ * 1 . . . σ * k
is said to be bounded [START_REF] Ginsburg | Bounded regular sets[END_REF]). Acceleration techniques provide a framework for deciding reachability properties that works well in practice but without termination guaranty in theory. Intuitively, acceleration techniques consist in computing with some symbolic representations transitive closures of sequences of actions. For Petri nets, the Presburger arithmetic is known to be expressive enough for this computation. In fact, denoting by --→ y if, and only if, the following formula holds:

∃x ′ , y ′ x σ -→ x ′ ∧ y -x = n∆(σ) ∧ y ′ σ -→ y
As a direct consequence, since the Presburger arithmetic is a decidable logic, the following algorithm can be implemented by denoting the sets C with Presburger formulas.

Acceleration(T, c init ) (1) C ← {c init } (2) while there exists c t - → c ′ with c ∈ C, t ∈ T and c ′ ∈ C (3) select σ ∈ T * (4) C ← {y ∈ N d | ∃c ∈ C c σ * -→ y} (5) return C
Naturally, when this algorithm terminates, it returns the reachability set. Moreover, under a fairness condition on line (3), this algorithm terminates on any flat Petri net. Basically, it is sufficient to assume that the infinite sequence of words σ 1 , σ 1 , . . ., selected during repeated executions of line (3), contains, as subsequences, all the finite sequences of words in T * . As a direct consequence flat Petri nets have reachability sets effectively definable in the Presburger arithmetic [START_REF] Leroux | Flat counter automata almost everywhere![END_REF]. Recently, we proved that many classes of Petri nets with known Presburger reachability sets are flat [START_REF] Leroux | Flat counter automata almost everywhere![END_REF], and we conjectured that Petri nets with reachability sets definable in the Presburger arithmetic are flat. In fact, the following theorem shows that the conjecture is true. As a direct consequence, classical tools implementing the previous acceleration algorithms always terminate on the computation of Presburger formulas denoting reachability sets of Petri nets when such a formula exists.

Theorem 1.3 ( [11]). A Petri net is flat if, and only if, its reachability set is definable in the Presburger arithmetic.

σ-→ 2 Fig. 1 .

 21 Fig. 1. The Hopcroft and Pansiot net.

  where σ ∈ T * , the following lemma shows that σ * -→ can be denoted by a formula in the Presburger arithmetic.

Lemma 1 . 2 (

 12 [START_REF] Fribourg | Petri nets, flat languages and linear arithmetic[END_REF]). For every word σ ∈ T * and n ≥ 1, we have x σ n


Jérôme Leroux

Acceleration For Petri Nets

The reachability problem for Petri nets is a central problem of net theory. The problem is known to be decidable by inductive invariants definable in the Presburger arithmetic. When the reachability set is definable in the Presburger arithmetic, the existence of such an inductive invariant is immediate. However, in this case, the computation of a Presburger formula denoting the reachability set is an open problem. Recently this problem got closed by proving that if the reachability set of a Petri net is definable in the Presburger arithmetic, then the Petri net is flat, i.e. its reachability set can be obtained by runs labeled by words in a bounded language. As a direct consequence, classical algorithms based on acceleration techniques effectively compute a formula in the Presburger arithmetic denoting the reachability set.

Introduction

Petri Nets are one of the most popular formal methods for the representation and the analysis of parallel processes [START_REF] Esparza | Decidability issues for petri nets -a survey[END_REF]. The reachability problem is central since many computational problems (even outside the realm of parallel processes) reduce to this problem. Sacerdote and Tenney provided in [START_REF] Sacerdote | The decidability of the reachability problem for vector addition systems (preliminary version)[END_REF] a partial proof of decidability of this problem. The proof was completed in 1981 by Mayr [START_REF] Mayr | An algorithm for the general petri net reachability problem[END_REF] and simplified by Kosaraju [4] from [START_REF] Sacerdote | The decidability of the reachability problem for vector addition systems (preliminary version)[END_REF][START_REF] Mayr | An algorithm for the general petri net reachability problem[END_REF]. Ten years later [START_REF] Lambert | A structure to decide reachability in petri nets[END_REF], Lambert provided a further simplified version based on [START_REF] Kosaraju | Decidability of reachability in vector addition systems (preliminary version)[END_REF]. This last proof still remains difficult and the upperbound complexity of the corresponding algorithm is just known to be non-primitive recursive. Nowadays, the exact complexity of the reachability problem for Petri nets is still an openquestion. Even an Ackermannian upper bound is open (this bound holds for Petri nets with finite reachability sets [START_REF] Figueira | Ackermannian and primitive-recursive bounds with dickson's lemma[END_REF]).

Basically, a Petri net is a pair (T, c init ) where T ⊆ N d × N d is a finite set of transitions, and c init ∈ N d is the initial configuration. A vector c ∈ N d is called a configuration. Given a transition t = (a, a ′ ), we introduce the binary relations t -→ over the configurations defined by

x t - → x ′ if there exists v ∈ N d such that x = a + v and x ′ = a ′ + v. A run from a configuration x to a configuration x ′ labelled by a word σ = t 1 . . . t k of transitions t j ∈ T is a sequence (c 0 , t 1 , c 1 , . . . , t k , c k ) where c 0 , . . . , c k are configurations such that c 0 = x, c k = x ′ , and such that c j-1 tj -→ c j for every 1 ≤ j ≤ k.
The reachability set is the set of configuration c such that that there exists a run from the initial configuration c init to c.

Example 1.1. The Petri net depicted in Figure 1 was introduced in [START_REF] Hopcroft | On the reachability problem for 5-dimensional vector addition systems[END_REF] as an example of Petri net having a reachability set which cannot be defined by a formula in the logic FO (N, +), called the Presburger arithmetic. In fact, the reachability set is equal to: Recently, in [START_REF] Leroux | The general vector addition system reachability problem by Presburger inductive invariants[END_REF], the reachability sets of Petri nets were proved to be almost semilinear, a class of sets that extends the class of Presburger sets (the sets definable in FO (N, +)) inspired by the semilinear sets [START_REF] Ginsburg | Semigroups, Presburger formulas and languages[END_REF]. Note that in general reachability sets are not definable in the Presburger arithmetic [START_REF] Hopcroft | On the reachability problem for 5-dimensional vector addition systems[END_REF] (see Example 1.1). An application of the almost semilinear sets was provided; a final configuration is not reachable from an initial one if and only if there exists a forward inductive invariant definable in the Presburger arithmetic that contains the initial configuration but not the final one. Since we can decide if a Presburger formula denotes a forward inductive invariant, we deduce that there exist checkable certificates of non-reachability in the Presburger arithmetic. In particular, there exists a simple algorithm for deciding the general Petri net reachability problem based on two semi-algorithms. A first one that tries to prove the reachability by enumerating finite sequences of actions and a second one that tries to prove the non-reachability by enumerating Presburger formulas. Such an algorithm always terminates in theory but in practice an enumeration does not provide an efficient way for deciding the reachability problem. In particular the problem of deciding efficiently the reachability problem is still an open question.

(p 1 , p 2 , p 3 , p 4 , p 5 ) ∈ N 5 | ( p 1 = 1 ∧ p 4 = 0 ∧ 1 ≤ p 2 + p 3 ≤ 2 p5 ) ∨ ( p 1 = 0 ∧ p 4 = 1 ∧ 1 ≤ p 2 + 2p 3 ≤ 2 p5+1 )
When the reachability set is definable in the Presburger arithmetic, the existence of checkable certificates of non-reachability in the Presburger arithmetic is immediate since the reachability set is a forward inductive invariant (in fact the most precise one). The problem of deciding if the reachability set of a Petri is definable in the Presburger arithmetic was studied twenty years ago independently by Dirk Hauschildt during his PhD [START_REF] Hauschildt | Semilinearity of the reachability set is decidable for Petri nets[END_REF] and Jean-Luc Lambert. Unfortunately, these two works were never published. Moreover, from these works, it is difficult to deduce a simple algorithm for computing a Presburger formula denoting the reachability set when such a formula exists.

For the class of flat Petri nets [START_REF] Fribourg | Petri nets, flat languages and linear arithmetic[END_REF][START_REF] Leroux | Flat counter automata almost everywhere![END_REF], such a computation can be performed with accelerations techniques. Let us recall that a Petri net is said to be flat if there exist some words σ 1 , . . . , σ k ∈ T * such that every reachable configuration is the target of a run labeled by a word in σ * 1 . . . σ * k from the initial configuration (A language included in σ * 1 . . . σ * k is said to be bounded [START_REF] Ginsburg | Bounded regular sets[END_REF]). Acceleration techniques provide a framework for deciding reachability properties that works well in practice but without termination guaranty in theory. Intuitively, acceleration techniques consist in computing with some symbolic representations transitive closures of sequences of actions. For Petri nets, the Presburger arithmetic is known to be expressive enough for this computation. As a direct consequence, when the reachability set of a Petri net is computable with acceleration techniques, this set is necessarily definable in the Presburger arithmetic. In [START_REF] Leroux | Flat counter automata almost everywhere![END_REF], we proved that a Petri net is flat if, and only if, its reachability set is computable by acceleration.

Recently, we proved that many classes of Petri nets with known Presburger reachability sets are flat [START_REF] Leroux | Flat counter automata almost everywhere![END_REF] and we conjectured that Petri nets with reachability sets definable in the Presburger arithmetic are flat. In [START_REF] Leroux | Presburger vector addition systems[END_REF] the conjecture get closed positively. As a direct consequence, classical acceleration techniques always terminate on the computation of Presburger formulas denoting reachability sets of Petri nets when such a formula exists.

2 Figure 1 :

 21 Figure 1: The Hopcroft and Pansiot net.

* Work funded by ANR grant REACHARD-ANR-11-BS02-001.