Univ. Bordeaux, CNRS, Bordeaux INP, LaBRI, UMR 5800, F-33400 Talence,
<EMAIL_ADDRESS>author is supported by the grant
ANR-17-CE40-0028 of the French National Research Agency ANR (project
BRAVAS)Jérôme Leroux[100]Theory of computation Logic and verification John Q.
Open and Joan R. Access 2 42nd Conference on Very Important Topics (CVIT 2016)
CVIT 2016 CVIT 2016 December 24–27, 2016 Little Whinging, United Kingdom 42 23

# Compiling Petri Net Mutual Reachability in Presburger

Jérôme Leroux

###### Abstract

Petri nets are a classical model of concurrency widely used and studied in
formal verification with many applications in modeling and analyzing hardware
and software, data bases, and reactive systems. The reachability problem is
central since many other problems reduce to reachability questions. The
reachability problem is known to be decidable but its complexity is extremely
high (non primitive recursive). In 2011, a variant of the reachability
problem, called the mutual reachability problem, that consists in deciding if
two configurations are mutually reachable was proved to be exponential-space
complete. Recently, this problem found several unexpected applications in
particular in the theory of population protocols. While the mutual
reachability problem is known to be definable in the Preburger arithmetic, the
best known upper bound of such a formula was recently proved to be non-
elementary (tower). In this paper we provide a way to compile the mutual
reachability relation of a Petri net with $d$ counters into a quantifier-free
Presburger formula given as a doubly exponential disjunction of $O(d)$ linear
constraints of exponential size. We also provide some first results about
Presburger formulas encoding bottom configurations.

###### keywords:

Petri nets, Vector addition systems, Formal verification, Reachability problem

###### category:

###  1 Introduction

Petri nets are a classical model of concurrency widely used and studied in
formal verification with many applications in modeling and analyzing hardware
and software, data bases, and reactive systems. The reachability problem is
central since many other problems reduce to reachability questions.
Unfortunately, the reachability problem is difficult for several reasons. In
fact, from a complexity point of view, the problem was recently proved to be
Ackermannian-complete ([17] for the upper-bound and [5, 15] for equivalent
lower-bounds). Moreover, even in practice, the reachability problem is
difficult. Nowadays, no efficient tool exists for deciding it since the known
algorithms are difficult to be implemented and require many enumerations in
extremely large state spaces (see [6] for the state-of-the-art algorithm
deciding the general reachability problem).

Fortunately, easier natural variants of the reachability problem can be
applied in various contexts. For instance, the coverability problem, a variant
of the reachability problem, can be applied in the analysis of concurrent
programs [1]. The coverability problem is known to be exponential-space
complete [20, 4], and efficient tools exist [3, 9].

Another variant is the mutual reachability problem. This problem consists in
deciding if two configurations are mutually reachable one from the other. This
problem was proved to be exponential-space complete in [13] and finds
unexpected applications in population protocols [7], trace logics [16],
universality problems related to structural liveness problems [12], and in
solving the home state problem [2]. The exponential-space complexity upper-
bound of the mutual reachability problem proved in [13] is obtained by
observing that if two configurations are mutually reachable, then the two
configurations belong to a cycle of the (infinite) reachability graph with a
length at most doubly-exponential with respect to the size in binary of the
two configurations.

Recently, the computation of a Presburger formula encoding the mutual
reachability problem found an application in the reachability problem of Petri
nets extended with a stack in [8]. In that paper, authors provided a formula
of tower size and left open the computation of a formula of elementary size.

Contribution. In this paper, we focus on the minimal size of a quantifier-free
Presburger formula encoding the mutual reachability relation. We provide a way
to compile the mutual reachability relation of a Petri net with $d$ counters
into a quantifier-free Presburger formula given as a doubly exponential
disjunction of $O(d)$ linear constraints of exponential size.

Outline. In Part I we provide algorithms for encoding in the quantifier-free
fragment of the Presburger arithmetic the membership of vectors in lattices
(see Section 2), and the reachability relations of words of Petri net actions
(see Section 3). In Part II we provide an overview of the way quantifier-free
Presburger formula encoding the mutual reachability are obtained. Results of
that part are self-contains except two technical results that are proved
respectively in Part III and Part IV. In Part V we conclude the paper with an
open problem about the configurations of a Petri net in the bottom strongly-
connected components of the reachability graph.

##  Part I Compiling in Presburger

In this part, we provide algorithms for encoding in the quantifier-free
fragment of the Presburger arithmetic lattices (see Section 2) and
reachability relations of words of Petri net actions (see Section 3).

The set of rationals, integers, non-negative rationals, and natural numbers
are denoted as $\mathbb{Q}$, $\mathbb{Z}$, $\mathbb{Q}_{\geq 0}$, and
$\mathbb{N}$ respectively. We denote by $\mathbb{X}^{d}$ the set of
$d$-dimensional vectors of elements in $\mathbb{X}$. Vectors are denoted in
bold face, and given $\mathbf{x}\in\mathbb{Q}^{d}$, we denote by
$\mathbf{x}(1),\ldots,\mathbf{x}(d)$ its components in such a way
$\mathbf{x}=(\mathbf{x}(1),\ldots,\mathbf{x}(d))$. We denote by
${\mathopen{\|}\mathbf{x}\mathclose{\|}}$ the _one-norm_
$\sum_{i=1}^{d}|\mathbf{x}(i)|$, and by
${\mathopen{\|}\mathbf{x}\mathclose{\|}_{\infty}}$ the _infinite-norm_
$\max_{1\leq i\leq d}|\mathbf{x}(i)|$. Given two vectors
$\mathbf{x},\mathbf{y}\in\mathbb{Q}^{d}$, we denote by
$\mathbf{x}\cdot\mathbf{y}$ the number
$\sum_{i=1}^{d}\mathbf{x}(i)\mathbf{y}(i)$.

###  2 Lattices

A _lattice_ is a _subgroup_ of $(\mathbb{Z}^{d},+)$, i.e. a set
$\mathbf{L}\subseteq\mathbb{Z}^{d}$ that contains the zero vector
$\mathbf{0}$, such that $\mathbf{x}+\mathbf{y}\in\mathbf{L}$ for every
$\mathbf{x},\mathbf{y}\in\mathbf{L}$, and such that $-\mathbf{x}\in\mathbf{L}$
for every $\mathbf{x}\in\mathbf{L}$. The lattice _spanned_ by a finite
sequence $\mathbf{v}_{1},\ldots,\mathbf{v}_{k}$ of vectors in $\mathbb{Z}^{d}$
is the lattice $\mathbb{Z}\mathbf{v}_{1}+\cdots+\mathbb{Z}\mathbf{v}_{k}$. Let
us recall that any lattice is spanned by such a finite sequence. It follows
that for any lattice $\mathbf{L}\subseteq\mathbb{Z}^{d}$, there is a
Presburger formula encoding the membership of a vector $\mathbf{v}$ in
$\mathbf{L}$ of the form $\exists z_{1},\ldots,z_{k}\leavevmode\nobreak\
\mathbf{v}=z_{1}\mathbf{v}_{1}+\cdots+z_{k}\mathbf{v}_{k}$. In order to obtain
a quantifier-free Presburger formula encoding $\mathbf{L}$, we can perform a
quantifier elimination from such a formula but it is difficult to obtain
interesting complexity bounds with such an approach. We follow another
approach based on the notion of _representations_.

A _representation_ $\gamma$ of a lattice $\mathbf{L}\subseteq\mathbb{Z}^{d}$
is a tuples
$\gamma\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}((n_{1},\mathbf{a}_{1}),\ldots,(n_{d},\mathbf{a}_{d}))$
of $d$ pairs $(n_{i},\mathbf{a}_{i})\in\mathbb{N}\times\mathbb{Z}^{d}$ such
that the following equality holds:

$\mathbf{L}=\left\\{\mathbf{x}\in\mathbb{Z}^{d}\mid\bigwedge_{i=1}^{d}\mathbf{a}_{i}\cdot\mathbf{x}\in
n_{i}\mathbb{Z}\right\\}$

We denote by $\llbracket{\gamma}\rrbracket$ the lattice $\mathbf{L}$ and by
${\mathopen{\|}\gamma\mathclose{\|}}_{\infty}$ the value
$\max\\{n_{1},{\mathopen{\|}\mathbf{a}_{1}\mathclose{\|}}_{\infty},\ldots,n_{d},{\mathopen{\|}\mathbf{a}_{d}\mathclose{\|}}_{\infty}\\}$.

In this section we prove the following Theorem 2.1 that shows that lattices
spanned by finite sequences of vectors admits a representation computable in
polynomial time (assuming numbers encoded in binary). Such a representation
will help encoding lattice membership with a formula in the quantifier-free
fragment of the Presburger arithmetic. All other results and definitions are
not used in the sequel.

######  Theorem 2.1.

Let $\mathbf{L}$ be the lattice spanned by a sequence of vectors in
$\\{-m,\ldots,m\\}^{d}$ encoded in binary for some $m\in\mathbb{N}$. We can
compute in polynomial time a representation $\gamma$ of $\mathbf{L}$ such that
${\mathopen{\|}\gamma\mathclose{\|}}_{\infty}\leq(d!)^{2}m^{d}$.

The proof is based on classical matrix operations over the rationals. We do
not recall classical notations and definitions we are using but briefly recall
some others.

Let $M$ be a $r\times r$ square matrix. Let us recall that the _determinant_
of $M$, denoted as $\det(M)$ is defined as $\sum_{\sigma\in
S_{r}}\operatorname{sgn}(\sigma)\prod_{i=1}^{r}M_{i\sigma(i)}$ where $S_{r}$
is the set of permutations of $\\{1,\ldots,r\\}$, and
$\operatorname{sgn}(\sigma)\in\\{-1,1\\}$ is the sign of $\sigma$. In
particular if $M$ is an integer matrix with coefficients bounded by some
$m\in\mathbb{N}$, then $\det(M)$ is an integer bounded in absolute value by
$r!m^{r}$. A $r\times r$ square matrix is said to be _non-singular_ if
$\det(M)$ is nonzero. Notice that in this case there exists a unique $r\times
r$ matrix $M^{-1}$ such that $M^{-1}M=MM^{-1}=I_{r}$ where $I_{r}$ is the
identity $r\times r$ square matrix, i.e. the matrix with zero coefficients
except on the main diagonal where coefficients are one. This matrix can be
computed by introducing the comatrice. Let us recall that the comatrix of any
$r\times r$ square matrix $M$ is the $r\times r$ square rational matrix
$\operatorname{com}(M)$ satisfying $(\operatorname{com}(M))_{ij}$ is
$\det(M^{ij})$ where $M^{ij}$ is the matrix obtained from $M$ by replacing the
$j$th column by a column of zeros, except on the $i$th line in which we put a
one. Let us recall that $M^{\top}\operatorname{com}(M)=\det(M)I_{r}$ where
$M^{\top}$ is the transpose of $M$. It follows that if $M$ is non-singular
then $M^{-1}=\frac{1}{\det(M)}\operatorname{com}(M)^{\top}$. Notice that if
the coefficients of $M$ are integers bounded in absolute value by some
$m\in\mathbb{N}$, then the coefficients of $\operatorname{com}(M)$ are
integers bounded in absolute value by $(r-1)!m^{r-1}$.

Let $M$ be a $r\times k$ matrix. The rank of $M$ is the maximal
$n\in\\{0,\ldots,\min\\{r,k\\}\\}$ such that $M$ admits a $n\times n$ non-
singular sub-matrix. Such a matrix $M$ is said to be _full row rank_ if its
rank is equal to $r$. We say that such a matrix $M$ has an _Hermite normal
form_ if there exists a uni-modular matrix $U$ (i.e. a matrix of integers with
a $+1$ or $-1$ determinant) such that $MU=[H0]$ where $H$ is a non-singular,
lower triangular, non-negative matrix, in which each row has a unique maximum
entry, which is located on the main diagonal of $H$. Let us recall that every
full row rank matrix $M$ has a unique Hermite normal form $[H0]$ and moreover
the uni-modular matrix $U$ such that $MU=[H0]$ is unique [21, Corollary 4.3b].
Additionally, if $M$ is an integral matrix then $H$ is a matrix of natural
numbers. Let us recall from [21, Section 10] that from a complexity point of
view, the matrices $U$ and $H$ are computable in polynomial time and moreover
$\det(H)$ divides the determinant of any $r\times r$ non-singular square sub-
matrix of $M$. In particular, if the coefficients of $M$ are integers bounded
in absolute value by some $m\in\mathbb{N}$, then $\det(H)$, which is the
product of the diagonal elements of $H$ is bounded by $r!m^{r}$. Let us recall
that $(\operatorname{com}(H))_{ax}=\det(H^{ij})$ where $H^{ij}$ is the matrix
obtained from $M$ by replacing the $j$th column by a column of zeros, except
on the $i$th line in which we put a one. Now, let $\sigma$ be a permutation of
$\\{1,\ldots,r\\}$ and observe that $(H^{ij})_{k\sigma(k)}\leq H_{kk}$ for
every $k\in\\{1,\ldots,r\\}$. It follows that
$\prod_{k=1}^{r}(H^{ij})_{k\sigma(k)}\leq\prod_{k=1}^{r}H_{kk}=\delta(H)$.
Therefore the coefficients of $\operatorname{com}(H)$ are integers bounded in
absolute value by $r!\det(H)\leq(r!)^{2}m^{r}$.

Now, let us prove Theorem 2.1. We consider a lattice $\mathbf{L}$ spanned by a
sequence $\mathbf{v}_{1},\ldots,\mathbf{v}_{k}$ of vectors in
$\\{-m,\ldots,m\\}^{d}$. We introduce the $d\times k$ matrix $L$ obtained from
this sequence by considering $\mathbf{v}_{j}$ as the $j$th column of $L$, i.e.
$L_{i,j}=\mathbf{v}_{j}(i)$ for every $1\leq i\leq d$ and $1\leq j\leq k$. We
denote by $r$ the rank of $L$. Recall that $r\leq\min\\{d,k\\}$. By reordering
columns of $L$ (which corresponds to a permutation of
$\mathbf{v}_{1},\ldots,\mathbf{v}_{k}$) and by reordering the lines of $L$,
(which corresponds to a permutation of the components of $\mathbf{L}$) we can
assume without loss of generality that $M$ can be decomposed as follows where
$A$ is a $r\times r$ non-singular matrix, $B$ is a $(d-r)\times r$ matrix,
$A^{\prime}$ is a $r\times(k-r)$ matrix, and $B^{\prime}$ is a
$(d-r)\times(k-r)$ matrix.

$L=\left[\begin{array}[]{cc}A&A^{\prime}\\\ B&B^{\prime}\end{array}\right]$

Let us introduce the $r\times k$ matrix
$M\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}[AA^{\prime}]$. Notice
that $M$ is full row rank. It follows that there exists a uni-modular matrix
$U$ such that $MU$ is in Hermite normal form $[H0]$.

We are ready for proving the following lemma.

######  Lemma 2.2.

The lattice $\mathbf{L}$ is the set of vectors $\mathbf{x}\in\mathbb{Z}^{d}$
such that:

  * $(i)$

$\det(H)$ divides the coefficients of
$[\mathbf{x}(1)\ldots\mathbf{x}(r)]\operatorname{com}(H)$, and

  * $(ii)$

$\det(A)[\mathbf{x}(r+1)\ldots\mathbf{x}(d)]=[\mathbf{x}(1)\ldots\mathbf{x}(r)]\operatorname{com}(A)B^{\top}$.

######  Proof 2.3.

Since the rank of $L$ is equal to the rank of $A$, it follows that every line
of $[BB^{\prime}]$ is a linear combination of the lines of $[AA^{\prime}]$. It
follows that there exists a $(d-r)\times r$ rational matrix $C$ such that
$[BB^{\prime}]=C[AA^{\prime}]$. Notice that this matrix $C$ satisfies
$C=BA^{-1}$ since $A$ is non-singular.

Assume first that $\mathbf{x}\in\mathbf{L}$.

Since $\mathbf{x}$ is a linear combination of the column vectors of $L$, and
since the $d-r$ last lines of $M$ are linear combinations of the lines of $L$,
we deduce that $\mathbf{x}$ is also a linear combination of the column vectors
of $M$. Hence, there exists a sequence $q_{1},\ldots,q_{k}\in\mathbb{Q}$ such
that $\mathbf{x}=\sum_{j=1}^{k}q_{j}\mathbf{v}_{j}$. From a matrix point of
view, we have $\left[\begin{array}[]{c}\mathbf{x}(1)\\\ \vdots\\\
\mathbf{x}(d)\end{array}\right]=M\left[\begin{array}[]{c}q_{1}\\\ \vdots\\\
q_{r}\end{array}\right]$. Since $M=\left[\begin{array}[]{c}A\\\
CA\end{array}\right]$, we deduce that $\mathbf{x}$ satisfies $(ii)$ by
observing that $\det(A)A^{-1}=\operatorname{com}(T)^{\top}$.

Next, observe that since $\mathbf{x}\in\mathbf{L}$ then
$\mathbf{x}=\sum_{j=1}^{k}z_{j}\mathbf{v}_{j}$ with
$z_{1},\ldots,z_{k}\in\mathbb{Z}$. It follows that we have:

$\displaystyle\left[\begin{array}[]{c}\mathbf{x}(1)\\\ \vdots\\\
\mathbf{x}(r)\end{array}\right]=M\left[\begin{array}[]{c}z_{1}\\\ \vdots\\\
z_{k}\end{array}\right]=[H0]U^{-1}\left[\begin{array}[]{c}z_{1}\\\ \vdots\\\
z_{k}\end{array}\right]=H\left[\begin{array}[]{c}z_{1}^{\prime}\\\ \vdots\\\
z_{r}^{\prime}\end{array}\right]$

Where $z_{1}^{\prime},\ldots,z_{k}^{\prime}$ is the following sequence:

$\left[\begin{array}[]{c}z_{1}^{\prime}\\\ \vdots\\\
z_{k}^{\prime}\end{array}\right]=U^{-1}\left[\begin{array}[]{c}z_{1}\\\
\vdots\\\ z_{k}\end{array}\right]$

We have proved that $\mathbf{x}$ satisfies $(i)$.

Finally, assume that $\mathbf{x}$ is any vector in $\mathbb{Z}^{d}$ satisfying
$(i)$ and $(ii)$. From $(i)$, we deduce that there exists
$z_{1}^{\prime},\ldots,z^{\prime}_{r}\in\mathbb{Z}$ such that:

$H^{-1}\left[\begin{array}[]{c}\mathbf{x}(1)\\\ \vdots\\\
\mathbf{x}(r)\end{array}\right]=\left[\begin{array}[]{c}z_{1}^{\prime}\\\
\vdots\\\ z_{r}^{\prime}\end{array}\right]$

We introduce the sequence $z_{1},\ldots,z_{k}$ defined as follows where
$z^{\prime}_{r+1},\ldots,z^{\prime}_{k}$ are defined as zero:

$\left[\begin{array}[]{c}z_{1}\\\ \vdots\\\
z_{k}\end{array}\right]\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}U\left[\begin{array}[]{c}z_{1}^{\prime}\\\
\vdots\\\ z_{k}^{\prime}\end{array}\right]$

Notice that we have:

$\left[\begin{array}[]{c}\mathbf{x}(1)\\\ \vdots\\\
\mathbf{x}(r)\end{array}\right]=[H0]U^{-1}\left[\begin{array}[]{c}z_{1}\\\
\vdots\\\ z_{k}\end{array}\right]\\\
=[AA^{\prime}]\left[\begin{array}[]{c}z_{1}\\\ \vdots\\\
z_{k}\end{array}\right]$

Combining with $(ii)$ and $[BB^{\prime}]=C[AA^{\prime}]$, we get:

$\left[\begin{array}[]{c}\mathbf{x}(1)\\\ \vdots\\\
\mathbf{x}(d)\end{array}\right]=L\left[\begin{array}[]{c}z_{1}\\\ \vdots\\\
z_{k}\end{array}\right]$

Therefore $\mathbf{x}\in\mathbf{L}$.

Now, let $n=\det(H)$. Observe that the coefficients of $\operatorname{com}(H)$
are bounded in absolute value by $(r!)^{2}m^{r}$. Since the coefficients of
$\operatorname{com}(A)$ are bounded in absolute value by $(r-1)!m^{r-1}$ and
the coefficients of $B$ are bounded in absolute value by $m$, we deduce that
the coefficients of $\operatorname{com}(A)B^{\top}$ are bounded in absolute
value by $r!m^{r}$. We have proved Theorem 2.1.

###  3 Words of Petri Net Actions

A _configuration_ is a vector in $\mathbb{N}^{d}$ and a _Petri net action_ is
a pair $a=(\mathbf{a}_{-},\mathbf{a}_{+})$ of configurations. We introduce
${\mathopen{\|}a\mathclose{\|}_{\infty}}\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\max\\{{\mathopen{\|}\mathbf{a}_{-}\mathclose{\|}_{\infty}},{\mathopen{\|}\mathbf{a}_{+}\mathclose{\|}_{\infty}}\\}$.
The _displacement_ of $a$ is defined as
$\Delta(a)\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\mathbf{a}_{+}-\mathbf{a}_{-}$.
We associate a Petri net action $a$ with the binary relation $\xrightarrow{a}$
over the configurations defined by $\mathbf{x}\xrightarrow{a}\mathbf{y}$ if
for some configuration $\mathbf{c}$ we have
$(\mathbf{x},\mathbf{y})=a+(\mathbf{c},\mathbf{c})$. Given a word
$\sigma=a_{1}\ldots a_{k}$ of Petri net actions $a_{1},\ldots,a_{k}$, we
introduce the _displacement_ of $\sigma$ defined as
$\Delta(\sigma)\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\sum_{j=1}^{k}\Delta(a_{j})$.
We also denote by $\xrightarrow{\sigma}$ the binary relation over the
configurations defined by $\mathbf{x}\xrightarrow{\sigma}\mathbf{y}$ if there
exists a sequence $\mathbf{c}_{0},\ldots,\mathbf{c}_{k}$ of configurations
such that $\mathbf{x}=\mathbf{c}_{0}$, $\mathbf{y}=\mathbf{c}_{k}$, and such
that $\mathbf{c}_{j-1}\xrightarrow{a_{j}}\mathbf{c}_{j}$ for every
$j\in\\{1,\ldots,k\\}$.

In this section, we provide a way to compile binary relations
$\xrightarrow{\sigma}$ for words $\sigma$ of Petri net actions into a
quantifier-free Preburger formula. In order to avoid introducing existentially
quantified intermediate variables (one for each action of $\sigma$), we recall
the definition of _Hurdle_ introduced in [11, Definition 2.5,p33]. First of
all, notice that $\mathbf{x}\xrightarrow{\sigma}\mathbf{y}$ for some
configurations $\mathbf{x},\mathbf{y}$ implies
$\mathbf{y}=\mathbf{x}+\Delta(\sigma)$. It follows that the relation
$\xrightarrow{\sigma}$ can be encoded in the Presburger arithmetic as soon as
we can characterize with a Presburger formula configurations $\mathbf{x}$ for
which there exists a configuration $\mathbf{y}$ such that
$\mathbf{x}\xrightarrow{\sigma}\mathbf{y}$. The _Hurdle_ of $\sigma$ provides
exactly this characterization. Intuitively, the Hurdle of $\sigma$ is the
unique minimal configuration $\mathbf{x}$ such that
$\mathbf{x}\xrightarrow{\sigma}\mathbf{y}$ for some $\mathbf{y}$. More
formally, let us introduce the Hurdle function $H$ that maps words of Petri
nets actions to configurations defined by induction as follows
$H(\varepsilon)$ is the zero configuration, and the following equality for any
Petri net action $a=(\mathbf{a}_{-},\mathbf{a}_{+})$ and for any word $\sigma$
of Petri net actions where $\max$ is the component-wise extension of the
classical max operator:

$H(a\sigma)=\max\\{\mathbf{a}_{-},H(\sigma)-\Delta(a)\\}$

The following lemma shows that the binary relation $\xrightarrow{\sigma}$ can
be encoded with a simple quantifier-free Presburger formula. In fact, for any
configurations $\mathbf{x},\mathbf{y}\in\mathbb{N}^{d}$, we have
$\mathbf{x}\xrightarrow{\sigma}\mathbf{y}$ if, and only if, the following
quantifier-free Presburger formula holds:

$\mathbf{x}\geq H(\sigma)\wedge\mathbf{y}=\mathbf{x}+\Delta(\sigma)$

######  Lemma 3.1 ([11]).

For every configuration $\mathbf{x}$ and every word $\sigma$ of Petri net
actions, we have $\mathbf{x}\geq H(\sigma)$ if, and only if, there exists a
configuration $\mathbf{y}$ such that
$\mathbf{x}\xrightarrow{\sigma}\mathbf{y}$.

The following lemma provides bounds on the values occurring in such a formula.

######  Lemma 3.2.

Let $\sigma$ be a word of Petri net actions in
$\\{0,\ldots,m\\}^{d}\times\\{0,\ldots,m\\}^{d}$ for some natural number
$m\in\mathbb{N}$. Then
${\mathopen{\|}H(\sigma)\mathclose{\|}}_{\infty},{\mathopen{\|}\Delta(\sigma)\mathclose{\|}}_{\infty}\leq|\sigma|m$.

######  Proof 3.3.

By induction on $|\sigma|$.

##  Part II Paper Overview

A _Petri net_ $A$ (_PN_ for short) is a finite set of Petri net actions. The
_reachability relation_ of $A$ is the binary relation $\xrightarrow{A^{*}}$
over the configurations defined by $\mathbf{x}\xrightarrow{A^{*}}\mathbf{y}$
if there exists a word $\sigma\in A^{*}$ such that
$\mathbf{x}\xrightarrow{\sigma}\mathbf{y}$. The Petri net reachability problem
consists in deciding given a PN $A$ and two configurations $\mathbf{x}$ and
$\mathbf{y}$ if $\mathbf{x}\xrightarrow{A^{*}}\mathbf{y}$. Whereas this
problem is decidable, its complexity is extremely hard (Ackermannian-
complete). This complexity no longer hold for a natural variant of the
reachability problem, called the mutual reachability problem, and defined as
follows.

The mutual reachability relation of a PN $A$ is the binary relation
$\ext@arrow 9999{\arrowfill@\leftarrow\relbar\rightarrow}{}{A^{*}}$ defined
over the configurations by $\mathbf{x}\ext@arrow
9999{\arrowfill@\leftarrow\relbar\rightarrow}{}{A^{*}}\mathbf{y}$ if
$\mathbf{x}\xrightarrow{A^{*}}\mathbf{y}$ and
$\mathbf{y}\xrightarrow{A^{*}}\mathbf{x}$. Since this relation is an
_equivalence relation_ (reflexive, symmetric, and transitive), it follows that
the set of configurations can be partitioned into equivalence classes. Such an
equivalence class is called a _strongly-connected component of configurations_
(_SCCC_ for short) of $A$. A SCCC $\mathbf{C}$ is said to be _forward-closed_
(resp. _backward-closed_) if for every triple
$(\mathbf{x},a,\mathbf{y})\in\mathbb{N}^{d}\times A\times\mathbb{N}^{d}$ such
that $\mathbf{x}\xrightarrow{a}\mathbf{y}$, we have
$\mathbf{x}\in\mathbf{C}\Rightarrow\mathbf{y}\in\mathbf{C}$ (resp.
$\mathbf{y}\in\mathbf{C}\Rightarrow\mathbf{x}\in\mathbf{C}$). A configuration
$\mathbf{c}_{\bot}$ is said to be _bottom_ (resp. _top_) for a PN $A$ if its
SCCC is _forward-closed_ (resp. _backward-closed_).

The PN mutual reachability problem consists in deciding given a PN $A$ and two
configurations $\mathbf{x}$ and $\mathbf{y}$ if $\mathbf{x}\ext@arrow
9999{\arrowfill@\leftarrow\relbar\rightarrow}{}{A^{*}}\mathbf{y}$,
equivalently if $\mathbf{x}$ and $\mathbf{y}$ are in the same SCCC. In [13],
we proved that the PN mutual reachability problem is decidable in exponential-
space by proving that there exists at most doubly-exponential long word
$u,v\in A^{*}$ such that $\mathbf{x}\xrightarrow{u}\mathbf{y}$ and
$\mathbf{y}\xrightarrow{v}\mathbf{x}$ when $\mathbf{x}$ and $\mathbf{y}$ are
mutually reachable.

In this paper we focus on the computation of concise quantifier-free
Presburger formulas encoding the mutual reachability relations and the set of
bottom configurations. Those formulas are obtained by proving that there exist
small witnesses of mutual reachability. Those witnesses are defined thanks to
the notion of _unfoldings_ introduced in Section 4. Intuitively an unfolding
of a Petri net is a graph hard-coding the values of some Petri net counters in
its states. In this section we also define the subclass of structurally-
reversible unfoldings. In Section 5 we show that this subclass provides
witnesses of mutual reachability. From those witnesses we provide in Section 6
a way to compile the mutual reachability relation of a Petri net in the
quantifier-free Presburger arithmetic.

###  4 Unfoldings

We introduce in this section the notion of unfoldings defined as
_structurally-reversible_ graphs hard-coding the values of some Petri net
counters in their states.

As usual, a (directed) _graph_ $G$ is a triple $(Q,A,T)$ where $Q$ is a non
empty finite set of states, $A$ is a finite set, and $T$ is a set of
_transitions_ in $Q\times A\times Q$. A _path_ $\pi$ from a state $p$ to a
state $q$ labeled by a word $\sigma\in A^{*}$ is a word of transitions in
$T^{*}$ of the form $(q_{0},a_{1},q_{1})\ldots(q_{k-1},a_{k},q_{k})$ for some
states $q_{0},\ldots,q_{k}$ satisfying $q_{0}=p$ and $q_{k}=q$, and for some
actions $a_{1},\ldots,a_{k}$ satisfying $\sigma=a_{1}\ldots a_{k}$. A path is
said to be _elementary_ if $q_{i}=q_{j}$ implies $i=j$. A path such that
$q_{0}=q_{k}$ is called a _cycle_ on $q_{0}$. A cycle is said to be _simple_
if $q_{i}=q_{j}$ with $i<j$ implies $i=0$ and $j=k$. A graph is said to be
_strongly-connected_ if for every state $p,q\in Q$ there exists a path from
$p$ to $q$.

A vector (in fact a mapping) in $\mathbb{N}^{I}$ where $I$ is a subset of
$\\{1,\ldots,d\\}$ is called an _$I$ -configuration_. Given an
$I$-configuration $\mathbf{c}$, we introduce
${\mathopen{\|}\mathbf{c}\mathclose{\|}_{\infty}}\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\max_{i\in
I}|\mathbf{c}(i)|$. We associate with a configuration
$\mathbf{c}\in\mathbb{N}^{d}$ the $I$-configuration $\mathbf{c}|_{I}$ in
$\mathbb{N}^{I}$ defined by $\mathbf{c}|_{I}(i)=\mathbf{c}(i)$ for every $i\in
I$. We also associate with a set $\mathbf{C}\subseteq\mathbb{N}^{d}$ of
configurations, the set
$\mathbf{C}|_{I}\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\\{\mathbf{c}|_{I}\mid\mathbf{c}\in\mathbf{C}\\}$.
Given an action $a=(\mathbf{a}_{-},\mathbf{a}_{+})$ of a Petri net, we extend
the binary relation $\xrightarrow{a}$ over the $I$-configurations by
$\mathbf{x}\xrightarrow{a}\mathbf{y}$ if $\mathbf{x},\mathbf{y}$ are
$I$-configurations such that there exists an $I$-configuration
$\mathbf{c}\in\mathbb{N}^{I}$ satisfying
$\mathbf{x}=\mathbf{a}_{-}|_{I}+\mathbf{c}$ and
$\mathbf{y}=\mathbf{a}_{+}|_{I}+\mathbf{c}$.

An _$I$ -unfolding_ of a PN $A$ where $I$ is a subset of $\\{1,\ldots,d\\}$ is
a strongly-connected _graph_ $G=(Q,A,T)$ where $Q$ is a finite set of
$I$-configurations, and $T$ is a set of triples $(p,a,q)\in Q\times A\times Q$
satisfying $p\xrightarrow{a}q$. The _displacement_ of a path $\pi$ labeled by
a word $\sigma$ is the vector
$\Delta(\pi)\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\Delta(\sigma)$.
Given a path $\pi$ from $p$ to $q$ labelled by a word $\sigma$, we denote by
$\xrightarrow{\pi}$ the binary relation on the configurations defined by
$\mathbf{x}\xrightarrow{\pi}\mathbf{y}$ if $\mathbf{x}|_{I}=p$,
$\mathbf{x}\xrightarrow{\sigma}\mathbf{y}$, and $\mathbf{y}|_{I}=q$.

An unfolding is said to be _structurally-reversible_ if for every transition
$t=(p,a,q)$ there exists a path $\pi$ from $q$ to $p$ such that
$\Delta(t\pi)=\mathbf{0}$.

######  Lemma 4.1.

Let $G=(Q,A,T)$ be a graph with states $Q\subseteq\mathbb{N}^{I}$ encoded in
binary. We can decide in polynomial time if $G$ is an $I$-unfolding and we can
decide in polynomial time if $G$ is structurally-reversible.

######  Proof 4.2.

Notice that $G$ is an $I$-unfolding if, and only if, $G$ is strongly-connected
and $p\xrightarrow{a}q$ for every $(p,a,q)\in T$. This property can be decided
in polynomial time. So, we can assume that $G$ is an $I$-unfolding. In that
case, notice that $G$ is structurally-reversible, if, and only if, the
following linear system over the free variable $f:T\rightarrow\mathbb{Q}_{>0}$
is satisfiable:

$\bigwedge_{q\in Q}\sum_{t\in T\cap\\{q\\}\times A\times Q}f(t)=\sum_{t\in
T\cap Q\times A\times\\{q\\}}f(t)\leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \wedge\leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ \sum_{t\in
T}f(t)\Delta(t)=\mathbf{0}$

This reduction is a direct application of the Euler’s lemma.

We associate a graph
$G_{\mathbf{C},I}\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}(Q,A,T)$
with an SCCC $\mathbf{C}$ and a set $I\subseteq\\{1,\ldots,d\\}$ such that
$\mathbf{C}|_{I}$ is finite by
$Q\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\mathbf{C}|_{I}$ and
$T\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\\{(\mathbf{x}|_{I},a,\mathbf{y}|_{I})\mid(\mathbf{x},a,\mathbf{y})\in\mathbf{C}\times
A\times\mathbf{C}\wedge\mathbf{x}\xrightarrow{a}\mathbf{y}\\}$.

######  Lemma 4.3.

The graph $G_{\mathbf{C},I}$ is a structurally-reversible $I$-unfolding.

######  Proof 4.4.

Let us denote by $G$ the graph $G_{\mathbf{C},I}$.

Since $\mathbf{x}\xrightarrow{a}\mathbf{y}$ implies
$\mathbf{x}|_{I}\xrightarrow{a}\mathbf{y}|_{I}$, we deduce that for every
transition $(p,a,q)\in T$, we have $p\xrightarrow{a}q$.

Let us show that $G$ is strongly-connected. Let $p,q\in Q$. There exists
$\mathbf{x},\mathbf{y}\in\mathbf{C}$ such that $p=\mathbf{x}|_{I}$ and
$q=\mathbf{y}|_{I}$. Since $\mathbf{C}$ is a SCCC, there exists a word
$\sigma$ of actions in $A$ such that
$\mathbf{x}\xrightarrow{\sigma}\mathbf{y}$ and such that all the intermediate
configurations are in $\mathbf{C}$. It follows that there exists a path in $G$
from $p$ to $q$ labeled by $\sigma$. In particular $G$ is strongly-connected.

Now, let us prove that $G$ is structurally-reversible. Let $(p,a,q)$ be a
transition in $T$. There exist $\mathbf{x},\mathbf{y}\in\mathbf{C}$ such that
$\mathbf{x}\xrightarrow{a}\mathbf{y}$ and such that $p=\mathbf{x}|_{I}$ and
$q=\mathbf{y}|_{I}$. Moreover since $\mathbf{C}$ is a SCCC, there exists a
word $\sigma$ of actions in $A$ such that
$\mathbf{y}\xrightarrow{\sigma}\mathbf{x}$ and such that all intermediate
configurations are in $\mathbf{C}$. We deduce that there exists a path in $G$
from $q$ to $p$ labeled by $\sigma$. Notice that
$\Delta(a)+\Delta(\sigma)=\mathbf{y}-\mathbf{x}+\mathbf{x}-\mathbf{y}=\mathbf{0}$.
It follows that $G$ is structurally-reversible.

####  4.1 Lattice $\mathbf{L}_{G}$

We associate with an $I$-unfolding $G$ the lattice $\mathbf{L}_{G}$ spanned by
the displacements of the simple cycles of $G$. The following lemma shows that
a representation $\gamma_{G}$ of $\mathbf{L}_{G}$ can be computed.

######  Lemma 4.5.

Let $G=(Q,A,T)$ be an $I$-unfolding with numbers encoded in binary. We can
compute in exponential time111In fact, it can be easily computed in polynomial
time thanks to a spanning tree of $G$, but this is out of the scope of that
paper. a representation $\gamma_{G}$ of $\mathbf{L}_{G}$ such that
${\mathopen{\|}\gamma_{G}\mathclose{\|}}_{\infty}\leq(d!)^{2}|Q|^{d}{\mathopen{\|}A\mathclose{\|}}_{\infty}^{d}$.

######  Proof 4.6.

Since a simple cycle has a length bounded by $|Q|$, it follows that
displacements of simple cycles are vectors in $\\{-m,\ldots,m\\}^{d}$ with
$m\leq|Q|.{\mathopen{\|}A\mathclose{\|}}_{\infty}$. We conclude the proof by
invoking Theorem 2.1.

The following lemma shows that for every pair $(p,q)$ of states the set
$\Delta(\pi)+\mathbf{L}_{G}$ does not depend on a path $\pi$ from $p$ to $q$.
We denote by $\mathbf{L}_{p,G,q}$ this set. Notice that $\mathbf{L}_{p,G,q}$
is a set of the form $\mathbf{v}+\mathbf{L}_{G}$ where $\mathbf{v}$ is a
vector in $\mathbb{Z}^{d}$ such that
${\mathopen{\|}\mathbf{v}\mathclose{\|}_{\infty}}\leq|Q|{\mathopen{\|}A\mathclose{\|}}_{\infty}^{d}$
since we can consider for $\mathbf{v}$ the displacement of an elementary path
from $p$ to $q$.

######  Lemma 4.7.

For every pair $(p,q)$ of states of a strongly-connected unfolding $G$, and
for any paths $\alpha,\beta$ from $p$ to $q$, we have
$\Delta(\alpha)+\mathbf{L}_{G}=\Delta(\beta)+\mathbf{L}_{G}$.

######  Proof 4.8.

Since $G$ is strongly-connected, there exists a path $\pi$ from $q$ to $p$.
Notice that $\alpha\pi$ and $\beta\pi$ are cycles in $G$, and in particular
$\Delta(\alpha\pi)+\mathbf{L}_{G}=\mathbf{L}_{G}=\Delta(\beta\pi)+\mathbf{L}_{G}$.
From $\Delta(\alpha)+\Delta(\beta\pi)=\Delta(\beta)+\Delta(\alpha\pi)$ we
deduce the lemma.

####  4.2 Upward-closed set $\mathbf{U}_{q,G}$

Given a set $\mathbf{C}$ of configurations, a configuration
$\mathbf{c}\in\mathbf{C}$ is said to be _minimal_ if for every
$\mathbf{x}\in\mathbf{C}$ we have
$\mathbf{x}\leq\mathbf{c}\Rightarrow\mathbf{x}=\mathbf{c}$. We denote by
$\min(\mathbf{C})$ the set of minimal elements of $\mathbf{C}$. The _upward-
closure_ of a set $\mathbf{B}\subseteq\mathbb{N}^{d}$ is the set
$\uparrow\mathbf{B}\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\mathbf{B}+\mathbb{N}^{d}$.
Given a configuration $\mathbf{b}$, we simply denote by $\uparrow\mathbf{b}$
the set $\uparrow\\{\mathbf{b}\\}$. A set $\mathbf{U}$ of configurations is
said to be _upward-closed_ if $\uparrow\mathbf{U}=\mathbf{U}$. Let us recall
that the upward-closure of any set is upward-closed, and since
$(\mathbb{N}^{d},\leq)$ is a well quasi ordered set, for any upward-closed set
$\mathbf{U}$, the set
$\mathbf{M}\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\min(\mathbf{U})$
is finite and satisfies $\mathbf{U}=\uparrow\mathbf{M}$. The set $\mathbf{M}$
is called the _basis_ of $\mathbf{U}$. It follows that the membership of a
configuration $\mathbf{x}$ in $\mathbf{U}$ is equivalent to the following
quantifier-free Presburger formula:

$\bigvee_{\mathbf{m}\in\mathbf{M}}\mathbf{x}\geq\mathbf{m}$

A _pumping pair_ for $(q,G)$ where $q$ is a state of an $I$-unfolding $G$ is a
pair $(u,v)$ of words in $A^{*}$ that label cycles on $q$ with a length
bounded by $db^{d}$ where
$b\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}(3dm)^{(d+2)^{2d+1}}$ and
$m\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}{\mathopen{\|}A\mathclose{\|}_{\infty}}$.
We introduce the set $\mathbf{U}_{q,G}$ of configurations
$\mathbf{c}\in\mathbb{N}^{d}$ such that $\mathbf{c}|_{I}\geq q$ and there
exists a pumping pair $(u,v)$ for $(q,G)$ such that
$\mathbf{c}^{-}\xrightarrow{u}\mathbf{c}\xrightarrow{v}\mathbf{c}^{+}$ for
some configurations $\mathbf{c}^{-},\mathbf{c}^{+}$ satisfying
$\mathbf{c}^{-}(i),\mathbf{c}^{+}(i)\geq mr^{3}(3drm)^{d}$ for every $i\not\in
I$ where $r\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}|Q|$. Notice
that $\mathbf{U}_{q,G}$ is upward-closed. The following lemma provides a way
to compute its basis.

######  Lemma 4.9.

Let $q$ be a state of an $I$-unfolding $G$ and let
$\mathbf{M}_{q,G}=\min\\{\mathbf{U}_{q,G}\\}$. We have
${\mathopen{\|}\mathbf{M}_{q,G}\mathclose{\|}_{\infty}}\leq s$ where
$s\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\max\\{{\mathopen{\|}q\mathclose{\|}}_{\infty},db^{d}m+mr^{3}(3drm)^{d}\\}$.
Moreover, we can decide the membership in $\mathbf{U}_{q,G}$ of a vector
$\mathbf{v}\in\\{0,\ldots,s\\}^{d}$ in space $O(\log(|Q|)+d\log(s))$.

######  Proof 4.10.

Let $W$ be the set of words in $A^{*}$ with a length bounded by $db^{d}$ that
labels a cycle on $q$ in $G$. Let $(u,v)\in W\times W$ and observe that a
configuration $\mathbf{c}\in\mathbb{N}^{d}$ is such that
$\mathbf{c}^{-}\xrightarrow{u}\mathbf{c}\xrightarrow{v}\mathbf{c}^{+}$ for
some configurations $\mathbf{c}^{-},\mathbf{c}^{+}$ if, and only if,
$\mathbf{c}\geq H(v)$ and $\mathbf{c}\geq H(u)+\Delta(u)$. Moreover, since in
that case $\mathbf{c}^{-}=\mathbf{c}-\Delta(u)$ and
$\mathbf{c}^{+}=\mathbf{c}+\Delta(v)$, we deduce that
$\mathbf{c}^{-}(i),\mathbf{c}^{+}(i)\geq mr^{3}(3drm)^{d}$ if, and only if,
$\mathbf{c}(i)\geq\Delta(u)+mr^{3}(3drm)^{d}$ and
$\mathbf{c}(i)\geq-\Delta(v)+mr^{3}(3drm)^{d}$. Let us introduce the
configuration $\mathbf{c}_{u,v}$ defined by $\mathbf{c}_{u,v}(i)=q(i)$ if
$i\in I$, and by the following equality if $i\not\in I$:

$c_{u,v}(i)=\max\\{H(v)(i),H(u)(i)+\Delta(u)(i),\Delta(u)(i)+mr^{3}(3drm)^{d},-\Delta(v)(i)+mr^{3}(3drm)^{d}\\}$

and observe that we have the following equality:

$\mathbf{U}_{q,G}=\uparrow\\{\mathbf{c}_{u,v}\mid(u,v)\in W\times W\\}$

Denoting by $\mathbf{M}_{q,G}=\min\\{\mathbf{U}_{q,G}\\}$, we deduce that
${\mathopen{\|}\mathbf{M}_{q,G}\mathclose{\|}}_{\infty}\leq s$. Now, let us
consider a vector $\mathbf{v}\in\\{0,\ldots,s\\}^{d}$ and observe that
$\mathbf{v}$ is in $\mathbf{U}_{q,G}$ if, and only if, there exists $(u,v)\in
W\times W$ such that $\mathbf{v}\geq\mathbf{c}_{u,v}$. Rather than exploring
all the possible pairs $(u,v)\in W\times W$, notice that we can explore step
by step pairs of words $(u,v)$, and just compute step by step the values
$H(u)$, $H(v)$, $\Delta(u)$, $\Delta(v)$, $|u|$, $|v|$, and the state
$q_{-},q_{+}$ such that $u$ is the label of a path from $q_{-}$ to $q$ and $v$
is the label of a path from $q$ to $q_{+}$. We then stop if $q_{-}=q=q_{+}$
and $\mathbf{v}\geq\mathbf{c}_{u,v}$. It follows that we can decide the
membership of $\mathbf{v}$ in $\mathbf{U}_{q,G}$ in space
$O(\log(|Q)+d\log(s))$.

###  5 Witnesses of Mutual Reachability

In this paper, we prove the following characterization of the mutual
reachability relation. This characterization will be useful to compute a
Presburger formula encoding the mutual reachability relation, and a Presburger
formula encoding the set of bottom configurations.

######  Theorem 5.1.

Let $A$ be a PN, and let
$b\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}(3dm)^{(d+2)^{2d+1}}$
where
$m\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}{\mathopen{\|}A\mathclose{\|}_{\infty}}$.
A set $\mathbf{C}$ of configurations are mutually reachable for $A$ if, and
only if, there exists a structurally-reversible $I$-unfolding $G=(Q,A,T)$ with
$\mathbf{C}|_{I}\subseteq
Q\subseteq\\{q\in\mathbb{N}^{I}\mid{\mathopen{\|}q\mathclose{\|}_{\infty}}<b\\}$
such that:

  * •

$\mathbf{c}\in\mathbf{U}_{\mathbf{c}|_{I},G}$ for every
$\mathbf{c}\in\mathbf{C}$,

  * •

$\mathbf{y}-\mathbf{x}\in\mathbf{L}_{\mathbf{x}|_{I},G,\mathbf{y}|_{I}}$ for
every $\mathbf{x},\mathbf{y}\in\mathbf{C}$.

One way of the previous Theorem 5.1 is obtained thanks to the following lemma.

######  Lemma 5.2.

Let us consider a structurally-reversible $I$-unfolding $(Q,A,T)$ and let
$r\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}|Q|$ and
$m\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}{\mathopen{\|}A\mathclose{\|}_{\infty}}$,
let $\mathbf{x},\mathbf{y}$ be two configurations such that:

  * •

$p\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\mathbf{x}|_{I}$, and
$q\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\mathbf{y}|_{I}$ are in
$Q$,

  * •

$\mathbf{x}(i),\mathbf{y}(i)\geq mr^{3}(3drm)^{d}$ for every $i\not\in I$, and

  * •

$\mathbf{y}-\mathbf{x}\in\mathbf{L}_{p,G,q}$.

Then for any elementary path $\pi$ from $p$ to $q$, there exists a cycle
$\theta$ on $q$ such that $\mathbf{x}\xrightarrow{\pi\theta}\mathbf{y}$ and
such that
$|\theta|\leq{\mathopen{\|}\mathbf{y}-\mathbf{x}-\Delta(\pi)\mathclose{\|}}2r^{3}(3drm)^{2d}$.

######  Proof 5.3.

The proof is given in Part III.

In fact, let us consider a set $\mathbf{C}$ of configurations such that there
exists an $I$-unfolding $G=(Q,A,T)$ such that $\mathbf{C}|_{I}\subseteq
Q\subseteq\\{q\in\mathbb{N}^{I}\mid{\mathopen{\|}q\mathclose{\|}_{\infty}}<b\\}$
such that:

  * •

$\mathbf{c}\in\mathbf{U}_{\mathbf{c}|_{I},G}$ for every
$\mathbf{c}\in\mathbf{C}$,

  * •

$\mathbf{y}-\mathbf{x}\in\mathbf{L}_{\mathbf{x}|_{I},G,\mathbf{y}|_{I}}$ for
every $\mathbf{x},\mathbf{y}\in\mathbf{C}$.

We introduce $r\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}|Q|$. Let
$\mathbf{x},\mathbf{y}\in\mathbf{C}$. Let
$p\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\mathbf{x}|_{I}$,
$q=\mathbf{y}|_{I}$. Since $\mathbf{x}\in\mathbf{U}_{p,G}$, there exists a
cycle $\alpha$ on $p$ with a length bounded by $db^{d}$ such that
$\mathbf{x}\xrightarrow{\alpha}\mathbf{x}^{+}$ for some configurations
$\mathbf{x}^{+}$ such that $\mathbf{x}^{+}(i)\geq mr^{3}(3drm)^{d}$ for every
$i\not\in I$. Symmetrically, there exists a cycle $\beta$ on $q$ with a length
bounded by $db^{d}$ such that $\mathbf{y}^{-}\xrightarrow{\beta}\mathbf{y}$
for some configurations $\mathbf{y}^{-}$ such that $\mathbf{y}^{-}(i)\geq
mr^{3}(3drm)^{d}$ for every $i\not\in I$. Observe that
$\mathbf{y}^{-}-\mathbf{x}^{+}=\mathbf{y}-\mathbf{x}-\Delta(\beta)+\Delta(\alpha)$.
In particular $\mathbf{y}^{-}-\mathbf{x}^{+}-\Delta(\pi)$ is in the lattice
$\mathbf{L}_{G}$. Lemma 5.2 shows that there exists a cycle $\theta$ on $q$
such that $\mathbf{x}^{+}\xrightarrow{\pi\theta}\mathbf{y}^{-}$ and such that
$|\theta|\leq{\mathopen{\|}\mathbf{y}^{-}-\mathbf{x}^{+}-\Delta(\pi)\mathclose{\|}}2r^{3}(3drm)^{2d}$.
It follows that we have $\mathbf{x}\xrightarrow{\pi^{\prime}}\mathbf{y}$ with
$\pi^{\prime}\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\alpha\pi\theta\beta$.
By symmetry, we get $\mathbf{x}\ext@arrow
9999{\arrowfill@\leftarrow\relbar\rightarrow}{}{A^{*}}\mathbf{y}$.

######  Remark 5.4.

As a direct consequence of the previous proof, notice that we can provide a
bound on the length of a path from $\mathbf{x}$ to $\mathbf{y}$ that only
depends on ${\mathopen{\|}\mathbf{y}-\mathbf{x}\mathclose{\|}}$, $d$ and $m$,
a result proved [14]. In fact, notice that
$\mathbf{y}^{-}-\mathbf{x}^{+}-\Delta(\pi)=\mathbf{y}-\mathbf{x}-\Delta(\beta)+\Delta(\alpha)-\Delta(\pi)$.
It follows that
${\mathopen{\|}\mathbf{y}^{-}-\mathbf{x}^{+}-\Delta(\pi)\mathclose{\|}}\leq{\mathopen{\|}\mathbf{y}-\mathbf{x}\mathclose{\|}}+dm(|\pi|+|\beta|+|\alpha|)\leq{\mathopen{\|}\mathbf{y}-\mathbf{x}\mathclose{\|}}+dm(2d+1)b^{d})$
since $|\pi|\leq r\leq b^{d}$, $|\beta|,|\alpha|\leq db^{d}$. It follows that:

$|\pi^{\prime}|\leq(2d+1)b^{d}+{\mathopen{\|}\mathbf{y}-\mathbf{x}\mathclose{\|}}+dm(2d+1)b^{d})2r^{3}(3drm)^{2d}$

By observing that $r\leq b^{d}$ and $b=(3dm)^{(d+2)^{2d+1}}$, we deduce that
there exists a constant $c_{d,m}$ that only depends on $d$ and $m$ such that
$|\pi^{\prime}|\leq{\mathopen{\|}\mathbf{y}-\mathbf{x}\mathclose{\|}}c_{d,m}$.

The other way of the previous Theorem 5.1 is obtained thanks to the following
lemma.

######  Lemma 5.5.

Let $A$ be a PN, and let
$b\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}(3dm)^{(d+2)^{2d+1}}$
where
$m\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}{\mathopen{\|}A\mathclose{\|}_{\infty}}$.
For every SCCC $\mathbf{C}$ of $A$, there exists a set
$I\subseteq\\{1,\ldots,d\\}$ such that
$\mathbf{C}|_{I}\subseteq\\{q\in\mathbb{N}^{I}\mid{\mathopen{\|}q\mathclose{\|}_{\infty}}<b\\}$,
and denoting by $G$ the structurally-reversible $I$-unfolding
$G_{\mathbf{C},I}$:

  * •

We have $\mathbf{c}\in\mathbf{U}_{\mathbf{c}|_{I},G}$ for every
$\mathbf{c}\in\mathbf{C}$, and

  * •

we have
$\mathbf{y}-\mathbf{x}\in\mathbf{L}_{\mathbf{x}|_{I},G,\mathbf{y}|_{I}}$ for
every $\mathbf{x},\mathbf{y}\in\mathbf{C}$.

######  Proof 5.6.

The proof is given in Part IV.

Concerning the set of bottom configurations, we provide the following theorem.
An $I$-unfolding $G=(Q,A,T)$ is said to be _forward-closed_ if for every $p\in
Q$ and for every $a\in A$, if there exists an $I$-configuration $q$ such that
$p\xrightarrow{a}q$, then $q\in Q$ and $(p,a,q)\in T$.

######  Theorem 5.7.

Let $A$ be a PN, and let
$b\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}(3dm)^{(d+2)^{2d+1}}$
where
$m\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}{\mathopen{\|}A\mathclose{\|}_{\infty}}$.
A configuration $\mathbf{c}$ is bottom if, and only if, there exists a
forward-closed structurally-reversible $I$-unfolding $G=(Q,A,T)$ such that
${\mathopen{\|}q\mathclose{\|}_{\infty}}<b$ for every $q\in Q$, a state $r\in
Q$ such that $\mathbf{c}|_{I}=r$, $\mathbf{c}\in\mathbf{U}_{r,G}$, and such
that for every $(p,a,q)\in T$ and for every $\mathbf{v}\in\mathbf{L}_{r,G,p}$,
we have:

$\mathbf{c}+\mathbf{v}\in\mathbf{U}_{p,G}\cap\uparrow\mathbf{a}_{-}\leavevmode\nobreak\
\leavevmode\nobreak\ \Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
\mathbf{c}+\mathbf{v}+\Delta(a)\in\mathbf{U}_{q,G}$

######  Proof 5.8.

Assume first that $\mathbf{c}$ is a bottom configuration and let $\mathbf{C}$
be its SCCC. Lemma 5.5 shows that there exists a set
$I\subseteq\\{1,\ldots,d\\}$ such that
${\mathopen{\|}\mathbf{x}|_{I}\mathclose{\|}_{\infty}}<b$ for every
$\mathbf{x}\in\mathbf{C}$, and denoting by $G$ the structurally-reversible
$I$-unfolding $G_{\mathbf{C},I}$:

  * •

We have $\mathbf{x}\in\mathbf{U}_{\mathbf{x}|_{I},G}$ for every
$\mathbf{x}\in\mathbf{C}$.

  * •

We have
$\mathbf{y}-\mathbf{x}\in\mathbf{L}_{\mathbf{x}|_{I},G,\mathbf{y}|_{I}}$ for
every $\mathbf{x},\mathbf{y}\in\mathbf{C}$.

Let $r=\mathbf{c}|_{I}$.

Let us prove that $G$ is forward-closed. Let $p\in Q$, $a\in A$, and consider
an $I$-configuration $q$ such that $p\xrightarrow{a}q$ and let us prove that
$q\in Q$. There exists $\mathbf{x}\in\mathbf{C}$ such that
$p=\mathbf{x}|_{I}$. Since $\mathbf{x}\in\mathbf{U}_{p,G}$, there exists a
configuration $\mathbf{x}^{+}$ reachable from $\mathbf{x}$ such that
$\mathbf{x}^{+}|_{I}=r$ and $\mathbf{x}^{+}(i)\geq m$ for every $i\not\in I$.
Since $\mathbf{C}$ is bottom, it follows that $\mathbf{x}^{+}\in\mathbf{C}$.
So, by replacing $\mathbf{x}$ by $\mathbf{x}^{+}$ we can assume that
$\mathbf{x}=\mathbf{x}^{+}$. As $p\xrightarrow{a}q$ and $\mathbf{x}|_{I}=p$,
we get $\mathbf{x}(i)=p(i)\geq\mathbf{a}_{-}(i)$ for every $i\in I$. Moreover,
as $\mathbf{x}(i)\geq m\geq\mathbf{a}_{-}(i)$ for every $i\not\in I$, we have
proved that $\mathbf{x}\geq\mathbf{a}_{-}$. Hence,
$\mathbf{x}\xrightarrow{a}\mathbf{y}$ with
$\mathbf{y}\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\mathbf{x}+\Delta(a)$.
As $\mathbf{C}$ is a bottom SCCC, we deduce that $\mathbf{y}\in\mathbf{C}$.
Hence $(\mathbf{x}|_{I},a,\mathbf{y}|_{I})\in T$. Since this triple is
$(p,a,q)$, we have proved that $q\in Q$ and $(p,a,q)\in T$. Hence $G$ is
forward-closed.

Let us consider $(p,a,q)\in T$ and $\mathbf{v}\in\mathbf{L}_{r,G,p}$ such that
$\mathbf{c}+\mathbf{v}\in\mathbf{U}_{p,G}\cap\uparrow\mathbf{a}_{-}$. Let
$\mathbf{x}\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\mathbf{c}+\mathbf{v}$.
Theorem 5.1 shows that $\mathbf{x}\in\mathbf{C}$. Since
$\mathbf{x}\geq\mathbf{a}_{-}$ we deduce that
$\mathbf{x}\xrightarrow{a}\mathbf{y}$ with
$\mathbf{y}\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\mathbf{x}+\Delta(a)$.
Since $\mathbf{C}$ is a bottom SCCC, it follows that
$\mathbf{y}\in\mathbf{C}$. Hence $\mathbf{y}\in\mathbf{U}_{q,G}$ since
$\mathbf{y}|_{I}=q$. We have proved one direction of the theorem.

Now, assume that $\mathbf{c}$ is a configuration such that there exists a
forward-closed structurally-reversible $I$-unfolding $G=(Q,A,T)$, a state
$r\in Q$ such that $\mathbf{c}|_{I}=r$, $\mathbf{c}\in\mathbf{U}_{r,G}$, and
such that for every $(p,a,q)\in T$ and for every
$\mathbf{v}\in\mathbf{L}_{r,G,p}$ we have:

$\mathbf{c}+\mathbf{v}\in\mathbf{U}_{p,G}\cap\uparrow\mathbf{a}_{-}\leavevmode\nobreak\
\leavevmode\nobreak\ \Longrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
\mathbf{c}+\mathbf{v}+\Delta(a)\in\mathbf{U}_{q,G}$

And let us prove that $\mathbf{c}$ is bottom. It is sufficient to prove that
for every configuration $\mathbf{x}$ reachable from $\mathbf{c}$, the
configurations $\mathbf{x}$ and $\mathbf{c}$ are mutually reachable. There
exists a word $\sigma\in A^{*}$ such that
$\mathbf{c}\xrightarrow{\sigma}\mathbf{x}$. Assume that $\sigma=a_{1}\ldots
a_{k}$, and let us introduce the sequence
$\mathbf{c}_{0},\ldots,\mathbf{c}_{k}$ of configurations such that
$\mathbf{c}_{0}=\mathbf{x}$, $\mathbf{c}_{k}=\mathbf{x}$ and such that
$\mathbf{c}_{i-1}\xrightarrow{a_{i}}\mathbf{c}_{i}$ for every $1\leq i\leq k$.
Let us introduce $q_{i}=\mathbf{c}_{i}|_{I}$. Since $G$ is forward-closed, and
$q_{i-1}\xrightarrow{a_{i}}q_{i}$ for every $1\leq i\leq k$, we deduce that
$q_{i}\in Q$ for every $0\leq i\leq k$. Notice that
$\mathbf{c}_{0}\in\mathbf{U}_{q_{0},G}$. Assume by induction that
$\mathbf{c}_{i-1}\in\mathbf{U}_{q_{i-1},G}$ for some $i\in\\{1,\ldots,k\\}$
and let us prove that $\mathbf{c}_{i}\in\mathbf{U}_{q_{i},G}$. Observe that
$\mathbf{c}_{i-1}=\mathbf{c}+\Delta(a_{1}\ldots a_{i-1})$. As $a_{1}\ldots
a_{i-1}$ is the label of a path from $r$ to $q_{i-1}$, it follows that
$\mathbf{v}\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\Delta(a_{1}\ldots
a_{i-1})$ is in $\mathbf{L}_{r,G,p}$. Since additionally we have
$\mathbf{c}_{i-1}\geq(\mathbf{a}_{i})_{-}$ we deduce that
$\mathbf{c}+\mathbf{v}+\Delta(a_{i})\in\mathbf{U}_{q_{i},G}$. As
$\mathbf{c}+\mathbf{v}+\Delta(a_{i})=\mathbf{c}_{i}$, we have proved the
induction. In particular $\mathbf{x}=\mathbf{c}_{k}$ is in
$\mathbf{U}_{q_{k},G}$. From Theorem 5.1 we deduce that $\mathbf{x}$ and
$\mathbf{c}$ are mutually reachable. Hence $\mathbf{c}$ is a bottom
configuration.

###  6 Compiling in Presburger

By encoding with a quantifier-free Presburger formula the membership of a
vector in the upward-closed set $\mathbf{U}_{q,G}$ and the lattice
$\mathbf{L}_{G}$, we obtain as a direct corollary the following theorem.

######  Theorem 6.1.

Let $A$ be a PN, and let
$s\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}2mb^{3d}(3db^{d}m)^{d}$
where
$b\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}(3dm)^{(d+2)^{2d+1}}$ and
$m\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}{\mathopen{\|}A\mathclose{\|}_{\infty}}$.
There exists a set $S_{A}$ of tuples
$(\mathbf{a},\mathbf{b},\mathbf{v},\gamma)$ where
$\mathbf{a},\mathbf{b}\in\\{0,\ldots,s\\}^{d}$ and
$\mathbf{v}\in\\{-s,\ldots,s\\}^{d}$ and $\gamma$ is a representation of a
lattice such that ${\mathopen{\|}\gamma\mathclose{\|}_{\infty}}\leq s$ with a
membership problem in space $O(s)$ such that for every configuration
$\mathbf{x},\mathbf{y}\in\mathbb{N}^{d}$, we have:

$\mathbf{x}\ext@arrow
9999{\arrowfill@\leftarrow\relbar\rightarrow}{}{A^{*}}\mathbf{y}\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\
\Longleftrightarrow\leavevmode\nobreak\ \leavevmode\nobreak\
\leavevmode\nobreak\ \bigvee_{(\mathbf{a},\mathbf{b},\mathbf{v},\gamma)\in
S_{A}}\mathbf{x}\geq\mathbf{a}\wedge\mathbf{y}-\mathbf{x}-\mathbf{v}\in\llbracket{\gamma}\rrbracket\wedge\mathbf{y}\geq\mathbf{b}$

######  Proof 6.2.

Let us introduce the set $S_{A}$ of tuples
$(\mathbf{a},\mathbf{b},\mathbf{v},\gamma)$ such that there exists a
structurally-reversible $I$-unfolding $G$ satisfying
$Q\subseteq\\{q\in\mathbb{N}^{I}\mid{\mathopen{\|}q\mathclose{\|}_{\infty}}<b\\}$,
let $r=|Q|\leq b^{d}$, such that $\gamma$ is a representation of
$\mathbf{L}_{G}$ satisfying
${\mathopen{\|}\gamma\mathclose{\|}_{\infty}}\leq(d!)^{2}b^{d}m^{d}\leq s$
computed by some given algorithm (see Lemma 4.5), two states $p,q\in Q$, a
simple path $\pi$ from $p$ to $q$ satisfying $\mathbf{v}=\Delta(\pi)$, and
$\mathbf{a},\mathbf{b}\in\\{0,\ldots,s\\}^{d}$ satisfying
$\mathbf{a}\in\mathbf{U}_{p,G}$ and $\mathbf{b}\in\mathbf{U}_{q,G}$. Notice
that ${\mathopen{\|}\mathbf{v}\mathclose{\|}_{\infty}}\leq b^{d}m\leq s$. From
Theorem 5.1, we deduce that $S_{A}$ satisfies the theorem.

Now, just observe we can decide if a tuple
$(\mathbf{a},\mathbf{b},\mathbf{v},\gamma)$ where
$\mathbf{a},\mathbf{b},\mathbf{v}\in\\{0,\ldots,s\\}^{d}$ and $\gamma$ is a
representation of a lattice such that
${\mathopen{\|}\gamma\mathclose{\|}_{\infty}}\leq s$ is in $S_{A}$ by
enumerating all the possible structurally-reversible $I$-unfolding $G$
satisfying
$Q\subseteq\\{q\in\mathbb{N}^{I}\mid{\mathopen{\|}q\mathclose{\|}_{\infty}}<b\\}$
(we just remember one at each step of the enumeration). Then, we just compute
with the algorithm used for defining $\mathbf{S}_{A}$ a representation of
$\mathbf{L}_{G}$ and check if $\gamma$ is this representation. Then we can
check if $\mathbf{a}\in\mathbf{U}_{p,G}$ and $\mathbf{b}\in\mathbf{U}_{q,G}$
in space $O(\log(|Q|)+d\log(s))$. We are done.

From a Presburger formula $\phi_{A}$ encoding the mutual reachability
relation, a Presburger formula $\phi_{A}^{\bot}(\mathbf{c})$ encoding the set
of bottom configurations can be obtained as follows:

$\phi_{A}^{\top}(\mathbf{c})\leavevmode\nobreak\
\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\leavevmode\nobreak\
\forall\mathbf{x}\bigwedge_{a\in
A}\phi_{A}(\mathbf{c},\mathbf{x})\wedge\mathbf{x}\geq\mathbf{a}_{-}\Rightarrow\phi_{A}(\mathbf{c},\mathbf{x}+\Delta(a))$

Even if such a formula is rather simple, it does not take advantage of the
fact that $\mathbf{c}$, $\mathbf{x}$ and $\mathbf{x}+\Delta(a)$ are in the
same SCCC, a property used in the following theorem.

A $k$-_threshold_ formula $\phi$ is a boolean combination of formulas of the
form $\mathbf{x}(i)\geq z$ where $i\in\\{1,\ldots,d\\}$ and $z\in\mathbb{Z}$
is an integer satisfying $|z|\leq k$. The size of such a formula is the one
expected with numbers encoded in binary.

######  Theorem 6.3.

Let $A$ be a PN and let
$s\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}2mb^{3d}(3db^{d}m)^{d}$
where
$b\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}(3dm)^{(d+2)^{2d+1}}$ and
$m\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}{\mathopen{\|}A\mathclose{\|}_{\infty}}$.
We can compute in time $O(s^{d})$ a set $T_{A}$ of tuples $(r,\gamma,\phi)$
where $r$ is an $I$-configuration with
${\mathopen{\|}q\mathclose{\|}_{\infty}}<b$, $\gamma$ is a representation of a
lattice such that ${\mathopen{\|}\gamma\mathclose{\|}_{\infty}}\leq s$, and
$\phi$ is a $k$-threshold formula with a size bounded by $O(s)$ and $k\leq s$,
and such that a configuration $\mathbf{c}$ is a bottom configurations if, and
only if:

$\bigvee_{(q,\gamma,\phi)\in T_{A}}\mathbf{c}|_{I}=r\leavevmode\nobreak\
\wedge\leavevmode\nobreak\
\forall\mathbf{v}\in\llbracket{\gamma}\rrbracket\leavevmode\nobreak\
\phi(\mathbf{c}+\mathbf{v})$

######  Proof 6.4.

The set $T_{A}$ is obtained by enumerating the forward-closed structurally-
reversible $I$-unfoldings $G=(Q,A,T)$ such that
${\mathopen{\|}q\mathclose{\|}_{\infty}}<b$ for every $q\in Q$. We introduce
$\mathbf{M}_{q,G}\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\min(\mathbf{U}_{q,G})$
for every $q\in Q$. For such a $G$ and for each state $r\in Q$, we introduce a
sequence $(v_{p})_{p\in Q}$ of vectors such that $\mathbf{v}_{p}$ is the label
of an elementary path from $r$ to $p$. We denote by $\phi_{r,G}$ the following
threshold formula:

$\phi_{r,G}(\mathbf{x})\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\bigwedge_{(p,a,q)\in
T}((\bigvee_{\mathbf{m}\in\mathbf{M}_{p,G}}\mathbf{x}\geq\max(\mathbf{m},\mathbf{a}_{-})-\mathbf{v}_{p})\Rightarrow(\bigvee_{\mathbf{m}\in\mathbf{M}_{q,G}}\mathbf{x}\geq\mathbf{m}-\Delta(a)-\mathbf{v}_{p}))$

From Theorem 6.3 we deduce that $T_{A}$ satisfies the theorem.

##  Part III Proof of Lemma 5.2

In this part, we prove Lemma 5.2. All other results proved in this section are
not used in the sequel. The proof follows an extended form of the _zigzag-
freeness_ approach introduced in [18]. Intuitively, we prove that the cycle
$\theta$ can be obtained by concatenating a sequence
$\theta_{1},\ldots,\theta_{k}$ of short cycles on $q$ such that for every
$n\in\\{0,\ldots,k\\}$ the displacement of
$\Delta(\theta_{1}\ldots\theta_{n})$ is almost the vector
$\frac{n-d}{k}(\mathbf{y}-\mathbf{x}-\Delta(\pi))$.

###  7 Reordering finite sums of integer vectors

In this section, we show that if a vector $\mathbf{z}\in\mathbb{Z}^{d}$ is the
sum of a sequence $\mathbf{z}_{1},\ldots,\mathbf{z}_{k}\in\mathbb{Z}^{d}$,
then we can extract a sub-sequence satisfying the same property and such that
additionally $k$ is small (with respect to some parameters). Moreover, we also
prove that we can reorder such a sequence in such a way
$\sum_{j=1}^{n}\mathbf{z}_{j}\geq\min\\{\mathbf{z}(i),0\\}$ for every
$i\in\\{1,\ldots,d\\}$ and for every $n\in\\{0,\ldots,k\\}$.

Those two results are obtained thanks to following central result.

######  Lemma 7.1 ([10]).

Let $\mathbf{v}_{1},\ldots,\mathbf{v}_{k}$ be a non-empty sequence of vectors
in $\mathbb{R}^{d}$ such that
${\mathopen{\|}\mathbf{v}_{j}\mathclose{\|}_{\infty}}\leq 1$ for every $1\leq
j\leq k$ and let $\mathbf{v}=\sum_{j=1}^{k}\mathbf{v}_{j}$. There exists a
permutation $\sigma$ of $\\{1,\ldots,k\\}$ such that for every
$n\in\\{d,\ldots,k\\}$, we have:

${\mathopen{\|}\sum_{j=1}^{n}\mathbf{v}_{\sigma(j)}-\frac{n-d}{k}\mathbf{v}\mathclose{\|}_{\infty}}\leq
d$

In fact, from the previous lemma we deduce the following two corollaries.

######  Corollary 7.2.

Assume that $\mathbf{z}=\mathbf{z}_{1}+\ldots+\mathbf{z}_{k}$ for some vectors
$\mathbf{z}_{1},\ldots,\mathbf{z}_{k}\in\mathbb{Z}^{d}$. Then there exists
$J\subseteq\\{1,\ldots,k\\}$ such that $\mathbf{z}=\sum_{j\in
J}\mathbf{z}_{j}$ with $|J|\leq
2{\mathopen{\|}\mathbf{z}\mathclose{\|}}(3dm)^{d}$ and
$m\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\max_{1\leq j\leq
k}{\mathopen{\|}\mathbf{z}_{j}\mathclose{\|}_{\infty}}$.

######  Proof 7.3.

Assume that $\mathbf{z}=\mathbf{z}_{1}+\ldots+\mathbf{z}_{k}$ for some vectors
$\mathbf{z}_{1},\ldots,\mathbf{z}_{k}\in\mathbb{Z}^{d}$ and assume that there
does not exists a set $J$ strictly smaller than $\\{1,\ldots,k\\}$ such that
$\mathbf{z}=\sum_{j\in J}\mathbf{z}_{j}$. This last property is equivalent to
$\sum_{j\in J}\mathbf{z}_{j}\not=\mathbf{0}$ for every non-empty subset
$J\subseteq\\{1,\ldots,k\\}$. We introduce
$m\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\max_{1\leq j\leq
k}{\mathopen{\|}\mathbf{z}_{j}\mathclose{\|}_{\infty}}$. Let us prove that
$k\leq 2{\mathopen{\|}\mathbf{z}\mathclose{\|}}(3dm)^{d}$. Without loss of
generality, we can assume that $\mathbf{z}\geq 0$ since we can swap the sign
of $\mathbf{z}(i),\mathbf{z}_{1}(i),\ldots,\mathbf{z}_{k}(i)$ for any $i$ to
reduce our problem to this special case. If $k=0$ the lemma is proved, so let
us assume that $k\geq 1$. In particular
${\mathopen{\|}\mathbf{z}\mathclose{\|}}\geq 1$ and $m\geq 1$.

Let us first prove that there exists a sequence
$\mathbf{e}_{1},\ldots\mathbf{e}_{k}$ of configurations such that
$\mathbf{e}_{j}\leq\max\\{\mathbf{0},\mathbf{z}_{j}\\}$ for every
$j\in\\{1,\ldots,k\\}$, and such that
$\mathbf{z}=\sum_{j=1}^{k}\mathbf{e}_{j}$. To do so, we introduce the non-
decreasing sequence $\mathbf{c}_{0},\ldots,\mathbf{c}_{k}$ of configurations
defined as
$\mathbf{c}_{0}\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\mathbf{0}$
and by induction for every $j\in\\{1,\ldots,k\\}$ by
$\mathbf{c}_{j}\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\max\\{\mathbf{c}_{j-1},\mathbf{c}_{j-1}+\mathbf{z}_{j}\\}$.
By induction, we observe that
$\mathbf{c}_{j}\geq\sum_{\ell=1}^{j}\mathbf{z}_{j}$ for every
$j\in\\{0,\ldots,k\\}$. In particular $\mathbf{c}_{k}\geq\mathbf{z}$. We also
introduce the sequence $\mathbf{e}_{1},\ldots,\mathbf{e}_{k}$ of
configurations defined by
$\mathbf{e}_{j}\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\min\\{\mathbf{z},\mathbf{c}_{j}\\}-\min\\{\mathbf{z},\mathbf{c}_{j-1}\\}$.
Notice
$\sum_{j=1}^{k}\mathbf{e}_{j}=\min\\{\mathbf{z},\mathbf{c}_{k}\\}-\min\\{\mathbf{z},\mathbf{c}_{0}\\}$.
Since $\mathbf{c}_{k}\geq\mathbf{z}$ and $\mathbf{c}_{0}=\mathbf{0}$, we
derive $\sum_{j=1}^{k}\mathbf{e}_{j}=\mathbf{z}$. Now, let us prove that
$\mathbf{e}_{j}\leq\max\\{\mathbf{0},\mathbf{z}_{j}\\}$. So, let
$i\in\\{1,\ldots,d\\}$. Assume first that $\mathbf{z}_{j}(i)\leq 0$. In that
case from
$\mathbf{c}_{j}\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\max\\{\mathbf{c}_{j-1},\mathbf{c}_{j-1}+\mathbf{z}_{j}\\}$,
we deduce that $\mathbf{c}_{j}(i)=\mathbf{c}_{j-1}(i)$. It follows that
$\mathbf{e}_{j}(i)=0$ and we are done. Now assume that $\mathbf{z}_{j}(i)>0$.
In that case from
$\mathbf{c}_{j}=\max\\{\mathbf{c}_{j-1},\mathbf{c}_{j-1}+\mathbf{z}_{j}\\}$ we
deduce that $\mathbf{c}_{j}(i)=\mathbf{c}_{j-1}(i)+\mathbf{z}_{j}(i)$. From
$\mathbf{e}_{j}\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\max\\{\mathbf{z},\mathbf{c}_{j}\\}-\max\\{\mathbf{z},\mathbf{c}_{j-1}\\}$
we deduce that
$\mathbf{e}_{j}(i)=\max\\{\mathbf{z}(i),\mathbf{c}_{j-1}(i)+\mathbf{z}_{j}(i)\\}-\max\\{\mathbf{z}(i),\mathbf{c}_{j-1}(i)\\}\leq\mathbf{z}_{j}(i)$
and we are done.

Next, let us introduce the sequence $\mathbf{v}_{1},\ldots,\mathbf{v}_{k}$
defined by
$\mathbf{v}_{j}\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\mathbf{z}_{j}-\mathbf{e}_{j}$.
Notice that ${\mathopen{\|}\mathbf{v}_{j}\mathclose{\|}_{\infty}}\leq m$ and
$\sum_{j=1}^{k}\mathbf{v}_{j}=\mathbf{0}$. We introduce
$\mathbf{x}_{n}\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\sum_{j=1}^{n}\mathbf{v}_{j}$.
By applying a permutation, Lemma 7.1 applied on the sequence
$(\frac{1}{m}\mathbf{v}_{j})_{1\leq j\leq n}$ shows that we can assume without
loss of generality that $\mathbf{x}_{n}\in\mathbf{X}$ for every $d\leq n\leq
k$ where $\mathbf{X}$ is the set of vectors $\mathbf{x}\in\mathbb{Z}^{d}$ such
that ${\mathopen{\|}\mathbf{x}\mathclose{\|}_{\infty}}\leq md$. Notice that if
$n\in\\{0,\ldots,d\\}$, we also have $\mathbf{x}_{n}\in\mathbf{X}$ since
$\mathbf{x}_{n}$ is a sum of at most $d$ vectors with a norm bounded by $m$.

The cardinal of $\mathbf{X}$ is bounded by $(1+2dm)^{d}\leq(3dm)^{d}$. Now,
assume by contradiction that there exists $\ell\in\\{0,\ldots,k-(3dm)^{d}\\}$
satisfying $\mathbf{e}_{j}=\mathbf{0}$ for every
$j\in\\{\ell+1,\ldots,\ell+(3dm)^{d}\\}$. Notice that there exists $p<q$ in
$\\{\ell,\ldots,\ell+(3dm)^{d}\\}$ such that $\mathbf{x}_{p}=\mathbf{x}_{q}$
since the cardinal of $\mathbf{X}$ is bounded by $(3dm)^{d}$. It follows that
$\sum_{j=p+1}^{q}\mathbf{v}_{j}=\mathbf{0}$. From $\mathbf{e}_{j}=\mathbf{0}$
for every $j\in\\{\ell+1,\ldots,\ell+(3dm)^{d}\\}$ it follows that
$\mathbf{v}_{j}=\mathbf{z}_{j}$ for every $j\in\\{p+1,\ldots,q\\}$. In
particular $\sum_{j=p+1}^{q}\mathbf{z}_{j}=\mathbf{0}$. Hence $k$ is not
minimal since we can remove the vectors
$\mathbf{z}_{p+1},\ldots,\mathbf{z}_{q}$ from the sequence
$\mathbf{z}_{1},\ldots,\mathbf{z}_{k}$, and we get a contradiction. It follows
that for every $\ell\in\\{0,\ldots,k-(3dm)^{d}\\}$ there exists
$j\in\\{\ell+1,\ldots,\ell+(3dm)^{d}\\}$ such that
$\mathbf{e}_{j}\not=\mathbf{0}$. From
${\mathopen{\|}\mathbf{z}\mathclose{\|}}=\sum_{j=1}^{k}{\mathopen{\|}\mathbf{e}_{j}\mathclose{\|}}$,
it follows that
${\mathopen{\|}\mathbf{z}\mathclose{\|}}\geq\frac{k}{(3dm)^{d}}-1$. Hence
$k\leq({\mathopen{\|}\mathbf{z}\mathclose{\|}}+1)(3dm)^{d}$. Since
$1+{\mathopen{\|}\mathbf{z}\mathclose{\|}}\leq
2{\mathopen{\|}\mathbf{z}\mathclose{\|}}$, we deduce that $k\leq
2{\mathopen{\|}\mathbf{z}\mathclose{\|}}(3dm)^{d}$.

######  Corollary 7.4.

Assume that $\mathbf{z}=\mathbf{z}_{1}+\cdots+\mathbf{z}_{k}$ where
$\mathbf{z}_{1},\ldots,\mathbf{z}_{k}\in\mathbb{Z}^{d}$. There exists a
permutation $\sigma$ of $\\{1,\ldots,k\\}$ such that for every
$n\in\\{0,\ldots,k\\}$ and for every $i\in\\{1,\ldots,d\\}$, we have:

$\sum_{j=1}^{n}\mathbf{z}_{\sigma(j)}(i)\geq\min\\{\mathbf{z}(i),0\\}-md$

where
$m\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\max_{j}{\mathopen{\|}\mathbf{z}_{j}\mathclose{\|}_{\infty}}$.

######  Proof 7.5.

If $k=0$ the lemma is proved. So, we can assume that $k\geq 1$, and in
particular $m\geq 1$. By applying a permutation, Lemma 7.1 on the sequence
$(\frac{1}{m}\mathbf{z}_{j})_{1\leq j\leq k}$ shows that we can assume without
loss of generality that for every $n\in\\{0,\ldots,k\\}$, there exists a
vector $\mathbf{e}_{n}\in\mathbb{R}^{d}$ such that
${\mathopen{\|}\mathbf{e}_{n}\mathclose{\|}_{\infty}}\leq md$ and such that
$\mathbf{x}_{n}=\frac{n-d}{k}\mathbf{z}+\mathbf{e}_{n}$ where
$\mathbf{x}_{n}\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\sum_{j=1}^{n}\mathbf{z}_{j}$.
Let $i\in\\{1,\ldots,d\\}$ and let us prove that
$\mathbf{x}_{n}(i)\geq\min\\{\mathbf{z}(i),0\\}-md$. Observe that if
$n\in\\{0,\ldots,d\\}$ then the property is immediate since
$\mathbf{x}_{n}(i)\geq-md$. So, let us assume that $n>d$. If
$\mathbf{z}(i)\geq 0$ then $\frac{n-d}{k}\mathbf{z}(i)\geq 0$ and we get
$\mathbf{x}_{n}(i)\geq\mathbf{e}_{n}(i)\geq-md$. If $\mathbf{z}(i)\leq 0$ then
$\frac{n-d}{k}\mathbf{z}(i)\geq\mathbf{z}(i)$. In particular
$\mathbf{x}_{n}(i)\geq\min\\{\mathbf{z}(i),0\\}-md$ also in that case.

###  8 From simple cycles to small full-state cycles

A cycle of an unfolding $G$ is said to be _full-state_ if every state of $G$
occurs in the cycle. In this section we prove that if $G$ is structurally-
reversible, then the displacement of any simple cycle is the displacement of a
“small” full-state cycle. In this section $G$ is a structurally-reversible
unfolding.

We first observe that the negation of the displacement of any cycle is the
displacement of another cycle as shown by the following lemma.

######  Lemma 8.1.

For every cycle $\theta$, there exists a cycle $\theta^{\prime}$ such that
$\Delta(\theta^{\prime})=-\Delta(\theta)$.

######  Proof 8.2.

Assume that $\theta=t_{1}\ldots t_{k}$ for some transitions
$t_{1},\ldots,t_{k}$. Since $G$ is structurally-reversible, for every
$j\in\\{1,\ldots,k\\}$, there exists a path $\pi_{j}$ such that $t_{j}\pi_{j}$
is a cycle with a zero displacement. Now, observe that
$\theta^{\prime}\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\pi_{k}\ldots\pi_{1}$
is a cycle such that $\Delta(\theta^{\prime})=-\Delta(\theta)$.

Let us show the following lemma based on small solutions for linear integer
programming [19].

######  Lemma 8.3.

Every transition occurs in a finite sequence $\theta_{1},\ldots,\theta_{n}$ of
simple cycles such that
$\Delta(\theta_{1})+\cdots+\Delta(\theta_{n})=\mathbf{0}$ and such that
$n\leq(3drm)^{d}$

######  Proof 8.4.

Let $t$ be a transition. Since $G$ is strongly connected, the transition $t$
occurs in a simple cycle $\theta_{0}$. Lemma 8.1 shows that
$-\Delta(\theta_{0})$ is a finite sum of displacements of simple cycles. In
particular $-\Delta(\theta_{0})$ is in the cone generated by the displacements
of simple cycles, i.e. the finite sums of displacements of simple cycles
multiplied by non-negative rational numbers. From Carathéodory theorem, there
exists $d$ simple cycles $\theta_{1},\ldots,\theta_{d}$ and $d$ non-negative
rational numbers $r_{1},\ldots,r_{d}$ such that
$-\Delta(\theta_{0})=\sum_{j=1}^{d}r_{j}\Delta(\theta_{j})$. By introducing a
positive integer $h_{0}$ such that
$h_{j}\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}h_{0}r_{j}$ is a
natural number for every $j$, we derive that the following linear system over
the sequences $(h_{j})_{0\leq\ j\leq d}$ of natural numbers

$\sum_{j=0}^{d}h_{j}\mathbf{v}_{j}=\mathbf{0}$

admits a solution satisfying $h_{0}>0$ where
$\mathbf{v}_{j}\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\Delta(\theta_{j})$.

From [19], it follows that solutions of that system can be decomposed as
finite sums of “minimal” solutions $(h_{j})_{1\leq j\leq k}$ of the same
system satisfying additionally the following constraint:

$\sum_{j=0}^{d}h_{j}\leq(1+(d+1)rm)^{d}$

From $1+(d+1)rm\leq(3drm)$, we derive $(1+(d+1)rm)^{d}\leq(3drm)^{d}$. Since
there exist solutions of that system with $h_{0}>0$, there exists at least a
minimal one satisfying the same constraint. We have proved the lemma.

We deduce the following lemma.

######  Lemma 8.5.

There exists a full-state cycle with a zero displacement with a length bounded
by $r^{2}(r-1)(3drm)^{d}$.

######  Proof 8.6.

Let us consider the set $H$ of pairs $(p,q)\in Q\times Q$ such that there
exists a transition from $p$ to $q$ with $p\not=q$. For every $h\in H$ of the
form $(p,q)$, we select a transition $t_{h}\in T$ from $p$ to $q$. Lemma 8.3
shows that for every $h\in H$, there exists a sequence of at most $(3drm)^{d}$
simple cycles with a zero total displacement that contains $t_{h}$. It follows
that there exists a sequence of at most $|H|(3drm)^{d}$ simple cycles with a
zero total displacement that contains all the transitions $t_{h}$ with $h\in
H$. Since the set of transitions that occurs in that sequence is strongly
connected, Euler’s Lemma shows that there exists a cycle $\theta$ with the
same Parikh image as the sum of the Parikh images of the cycles occurring in
the sequence. It follows that $|\theta|\leq r|H|(3rdm)^{d}$. Notice that
$\Delta(\theta)=\mathbf{0}$ and $\theta$ is a full-state cycle. From $|H|\leq
r(r-1)$ we are done.

We deduce the following corollary.

######  Corollary 8.7.

The displacement of a simple cycle is the displacement of a full-state cycle
with a length bounded by $r^{2}(r-1)(3drm)^{d}+r$.

######  Proof 8.8.

Lemma 8.5 shows that there exists full-state cycle $\theta$ with a zero
displacement with a length bounded by $r^{2}(r-1)(3drm)^{d}$. Now, just
observe that any simple cycle $\theta_{s}$ can be inserted in $\theta$ in such
a way we get a full-state cycle with the same displacement as $\theta_{s}$.

###  9 Proof of Lemma 5.2

Now, let us prove Lemma 5.2. To do so, let us consider a structurally-
reversible $I$-unfolding $G=(Q,A,T)$, and let
$r\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}|Q|$ and
$m\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}{\mathopen{\|}A\mathclose{\|}_{\infty}}$.
Notice that if $m=0$ the proof is immediate. So, we can assume that $m\geq 1$.

Let $\mathbf{x},\mathbf{y}$ be two configurations such that the following
conditions hold:

  * •

$\mathbf{x}|_{I},\mathbf{y}|_{I}\in Q$,

  * •

$\mathbf{x}(i),\mathbf{y}(i)\geq mr^{3}(3drm)^{d}$ for every $i\not\in I$, and

  * •

$\mathbf{y}-\mathbf{x}\in\mathbf{L}_{\mathbf{x}|_{I},G,\mathbf{y}|_{I}}$.

Let $\pi$ be an elementary path from $\mathbf{x}|_{I}$ to $\mathbf{y}|_{I}$.

We introduce
$\mathbf{z}\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\mathbf{y}-\mathbf{x}-\Delta(\pi)$.
Since
$\mathbf{y}-\mathbf{x}\in\mathbf{L}_{\mathbf{x}|_{I},G,\mathbf{y}|_{I}}$, we
deduce that $\mathbf{z}\in\mathbf{L}_{G}$. It follows that $\mathbf{z}$ is a
finite sum of displacements of cycles and negation of displacements of cycles.
Lemma 8.1 shows that the negation of the displacement of a cycle is the
displacement of another cycle. It follows that $\mathbf{z}$ is a finite sum of
displacements of cycles. As the displacement of a cycle is a finite sum of
displacements of simple cycles, we deduce that $\mathbf{z}$ is a finite sum of
displacements of simple cycles.

Corollary 7.2 and Corollary 7.4 shows that there exists a sequence
$\mathbf{z}_{1},\ldots,\mathbf{z}_{k}$ of displacements of simple cycles such
that $\mathbf{z}=\sum_{j=1}^{k}\mathbf{z}_{j}$,
$k\leq(1+{\mathopen{\|}\mathbf{z}\mathclose{\|}})(3drm)^{d}$, and such that
for every $n\in\\{0,\ldots,k\\}$, we have:

$\sum_{j=1}^{n}\mathbf{z}_{j}(i)\geq\min\\{0,\mathbf{z}(i)\\}-drm$

Corollary 8.7 shows that for every $1\leq j\leq k$, there exists a full-state
cycle $\theta_{j}$ such that $\Delta(\theta_{j})=\mathbf{z}_{j}$ and
$|\theta_{j}|\leq r^{2}(r-1)(3drm)^{d}+r$. With a rotation of $\theta_{j}$, we
can assume without loss of generality that $\theta_{j}$ is a cycle on $q$. We
introduce the cycle $\theta$ defined as follows:

$\theta\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\theta_{1}\ldots\theta_{n}$

We are going to prove that $\mathbf{x}\xrightarrow{\pi\theta}\mathbf{y}$. To
do so, let $\delta t$ be a prefix of $\pi\theta$ where $\delta$ is a path from
$p$ to a state $r$ and $t=(r,a,s)$ is a transition in $T$ and
$a=(\mathbf{a}_{-},\mathbf{a}_{+})$ is a Petri net action. Let
$i\in\\{1,\ldots,d\\}$ and let us prove that
$\mathbf{x}(i)+\Delta(\delta)(i)\geq\mathbf{a}_{-}(i)$. Observe that if $i\in
I$, since $G$ is an $I$-unfolding, and $\mathbf{x}(i)=p(i)$, we have
$\mathbf{x}(i)+\Delta(\delta)(i)=r(i)$. Moreover, as $r\xrightarrow{a}s$ we
deduce that $\mathbf{x}(i)+\Delta(\delta)(i)\geq\mathbf{a}_{-}(i)$. Now,
assume that $i\not\in I$. Since $\mathbf{a}_{-}(i)\leq m$, it is sufficient to
show that $\mathbf{x}(i)+\Delta(\pi)(i)\geq m$ in that case.

Since $\pi$ is elementary, we deduce that $|\pi|<r$. Notice that if $\delta$
is a prefix of $\pi$ then $|\delta|\leq|\pi|$. In particular
$\Delta(\delta)(i)\geq-m(r-1)$. It follows that
$\mathbf{x}(i)+\Delta(\delta)(i)\geq m$ and we are done. So, we can assume
that $\delta$ is not a prefix of $\pi$. It follows that there exists
$n\in\\{1,\ldots,k\\}$ and a prefix $\pi^{\prime}$ of $\theta_{n}$ such that
$\delta=\pi\theta_{1}\ldots\theta_{n-1}\pi^{\prime}$. Hence
$\Delta(\delta)=\Delta(\pi\pi^{\prime})+\sum_{j=1}^{n-1}\mathbf{z}_{j}(i)$.
Moreover, notice that $|\Delta(\pi\pi^{\prime})(i)|\leq m|\pi\pi^{\prime}|\leq
m(r-1)+mr^{2}(r-1)(3drm)^{d}+mr\leq mr^{3}(3drm)^{d}-drm-m$. We decompose the
proof that $\mathbf{x}(i)+\Delta(\delta)(i)\geq m$ in two cases following that
$\mathbf{z}(i)\leq 0$ or $\mathbf{z}(i)\geq 0$.

  * •

Assume first that $\mathbf{z}(i)\geq 0$. In that case
$\sum_{j=1}^{n-1}\mathbf{z}_{j}(i)\geq-drm$. It follows that
$\mathbf{x}(i)+\Delta(\delta)(i)\geq mr^{3}(3drm)^{d}-drm-
mr^{3}(3drm)^{d}+drm+m\geq m$.

  * •

Next, assume that $\mathbf{z}(i)\leq 0$. In that case
$\sum_{j=1}^{n-1}\mathbf{z}_{j}(i)\geq\mathbf{z}(i)-drm$. It follows that
$\mathbf{x}(i)+\Delta(\delta)(i)\geq\mathbf{x}(i)+\mathbf{z}(i)+\Delta(\pi\pi^{\prime})(i)-drm=\mathbf{y}(i)-\Delta(\pi\pi^{\prime})(i)-drm\geq(3drm)^{d}-drm-
mr^{3}(3drm)^{d}+drm+m\geq m$.

We have proved that $\mathbf{x}\xrightarrow{\pi\theta}\mathbf{y}$. Now,
observe that $|\theta|\leq k(r^{2}(r-1)(3drm)^{d}+r)$. From $k\leq
2{\mathopen{\|}\mathbf{z}\mathclose{\|}}(3drm)^{d}$, we get
$|\theta|\leq{\mathopen{\|}\mathbf{y}-\mathbf{x}\mathclose{\|}}2r^{3}(3drm)^{2d}$.
Lemma 5.2 is proved.

##  Part IV Proof of Lemma 5.5

In this part, we prove Lemma 5.5. All other results proved in this part are
not used in the sequel.

###  10 Extractors

The notion of extractors was first introduced in [13]. Intuitively, extractors
provide a natural way to classify components of a vector of natural numbers
into two categories: large ones and small ones. The notion is parameterized by
a set $I\subseteq\\{1,\ldots,d\\}$ that provides a way to focus only on
components in $I$. More formally, a _$d$ -dimensional extractor_ $\lambda$ is
a non-decreasing sequence $(\lambda_{0}\leq\cdots\leq\lambda_{d+1})$ of
positive natural numbers denoting some _thresholds_. Given a $d$-dimensional
extractor $\lambda$ and a set $I\subseteq\\{1,\ldots,d\\}$, a _$(\lambda,I)$
-small set_ of a set $\mathbf{C}\subseteq\mathbb{N}^{d}$ is a subset
$J\subseteq I$ such that $\mathbf{c}(j)<\lambda_{|J|}$ for every $j\in J$ and
$\mathbf{c}\in\mathbf{C}$. The following lemma shows that there exists a
unique maximal $(\lambda,I)$-small set w.r.t. inclusion. We denote by
$\operatorname{extract}_{\lambda,\mathbf{C}}(I)$ this set.

######  Lemma 10.1.

The class of $(\lambda,I)$-small sets of a set
$\mathbf{C}\subseteq\mathbb{N}^{d}$ is non empty and stable under union.

######  Proof 10.2.

We adapt the proof of [13, Section 8]. Since the class contains the empty set,
it is nonempty. Now, let us prove the stability by union by considering two
$(\lambda,I)$-small sets $J_{1}$ and $J_{2}$ of $\mathbf{C}$ and let us prove
that $J\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}J_{1}\cup J_{2}$ is
a $(\lambda,I)$-small set of $\mathbf{C}$. Since $J_{1},J_{2}\subseteq I$, we
derive $J\subseteq I$. Let $\mathbf{c}\in\mathbf{C}$ and $j\in J$. If $j\in
J_{1}$ then $\mathbf{c}(j)<\lambda_{|J_{1}|}\leq\lambda_{|J|}$ since
$|J_{1}|\leq|J|$. Symmetrically, if $j\in J_{2}$ we deduce that
$\mathbf{c}(j)<\lambda_{|J_{2}|}\leq\lambda_{|J|}$. We have proved that $J$ is
a $(\lambda,I)$-small set of $\mathbf{C}$.

######  Example 10.3.

Let us consider the $2$-dimensional extractor
$\lambda=(\lambda_{0}\leq\lambda_{1}\leq\lambda_{2}\leq\lambda_{3})$ and
assume that $I=\\{1,2\\}$ and let $\mathbf{C}=\\{(m,n)\\}$ with
$m,n\in\mathbb{N}$. We have:

$\operatorname{extract}_{\lambda,\mathbf{C}}(I)=\begin{cases}\\{1,2\\}&\text{
if }m,n<\lambda_{2}\\\ \emptyset&\text{ if }(m\geq\lambda_{2}\wedge
n\geq\lambda_{1})\vee(m\geq\lambda_{1}\wedge n\geq\lambda_{2})\\\
\\{1\\}&\text{ if }m<\lambda_{1}\wedge n\geq\lambda_{2}\\\ \\{2\\}&\text{ if
}m\geq\lambda_{2}\wedge n<\lambda_{1}\end{cases}$

######  Remark 10.4.

As shown by the previous example, the values $\lambda_{0}$ and $\lambda_{d+1}$
of any $d$-dimensional extractor $\lambda$ are not used directly by our
definitions. Those extreme values are introduced to simplify some notations in
the sequel.

The following lemma shows that components that are not in
$\operatorname{extract}_{\lambda,\mathbf{C}}(I)$ are large for at least one
vector in $\mathbf{C}$.

######  Lemma 10.5.

Let
$J\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\operatorname{extract}_{\lambda,\mathbf{C}}(I)$.
For every $i\in I\backslash J$ there exists $\mathbf{c}\in\mathbf{C}$ such
that:

$\mathbf{c}(i)\geq\lambda_{|J|+1}$

######  Proof 10.6.

Assume that for some $i\in I\backslash J$, we have
$\mathbf{c}(i)<\lambda_{|J|+1}$ for every $\mathbf{c}\in\mathbf{C}$. Let
$J^{\prime}\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}J\cup\\{i\\}$
and observe that $J^{\prime}$ is a $(\lambda,I)$-small set of $\mathbf{C}$. In
fact, for every $\mathbf{c}\in\mathbf{C}$ and for every $j\in J^{\prime}$, we
have $\mathbf{c}(j)<\lambda_{|J|}\leq\lambda_{|J^{\prime}|}$ if $j\in J$, and
$\mathbf{c}(j)<\lambda_{|J|+1}=\lambda_{|J^{\prime}|}$ if $j=i$. We get a
contradiction by maximality of
$\operatorname{extract}_{\lambda,\mathbf{C}}(I)$. We deduce the lemma.

Given a set $I\subseteq\\{1,\ldots,d\\}$ we define
$\operatorname{extract}_{\lambda,e}(I)$ for a finite word $e$ of
configurations by
$\operatorname{extract}_{\lambda,\varepsilon}(I)\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}I$,
and by
$\operatorname{extract}_{\lambda,e\mathbf{c}}(I)\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\operatorname{extract}_{\lambda,\\{\mathbf{c}\\}}(\operatorname{extract}_{\lambda,e}(I))$
for every $\mathbf{c}\in\mathbb{N}^{d}$ and for every finite word $e$ of
configurations. Given an infinite word $e$ of configurations, we observe that
$(\operatorname{extract}_{\lambda,e_{n}}(I))_{n\in\mathbb{N}}$ where $e_{n}$
is the finite prefix of $e$ of length $n$ is a non-increasing sequence of sets
in $\\{1,\ldots,d\\}$. It follows that this sequence is asymptotically
constant and equals to a set included in $\\{1,\ldots,d\\}$. We denote
$\operatorname{extract}_{\lambda,e}(I)$ that set. The following lemma shows
that extracting along a word of configurations in $\mathbf{C}$ asymptotically
coincides with an extraction of $\mathbf{C}$.

######  Lemma 10.7.

Let us consider a set $I\subseteq\\{1,\ldots,d\\}$, an extractor $\lambda$, a
set $\mathbf{C}$ of configurations, and an infinite word $e$ over
$\mathbf{C}$. We have
$\operatorname{extract}_{\lambda,\mathbf{C}}(I)\subseteq\operatorname{extract}_{\lambda,e}(I)$.
Moreover,
$\operatorname{extract}_{\lambda,\mathbf{C}}(I)=\operatorname{extract}_{\lambda,e}(I)$
if every configuration of $\mathbf{C}$ occurs infinitely often in $e$.

######  Proof 10.8.

We introduce
$J\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\operatorname{extract}_{\lambda,\mathbf{C}}(I)$,
$J_{\infty}\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\operatorname{extract}_{\lambda,e}(I)$,
the prefix $e_{n}$ of length $n$ of $e$, and
$J_{n}\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\operatorname{extract}_{\lambda,e_{n}}(I)$.

Let us prove that $J\subseteq J_{n}$ for every $n$. Since $J_{0}=I$ the
property is proved for $n=0$. Assume that $J\subseteq J_{n-1}$ for some $n\geq
1$ and let us prove that $J\subseteq J_{n}$. There exists
$\mathbf{c}\in\mathbf{C}$ such that $e_{n}=e_{n-1}\mathbf{c}$. Since
$\mathbf{c}\in\mathbf{C}$, it follows that $\mathbf{c}(j)<\lambda_{|J|}$ for
every $j\in J$. As $J\subseteq J_{n-1}$, we deduce that $J$ is a
$(\lambda,J_{n-1})$-small set of $\\{\mathbf{c}\\}$. Since $J_{n}$ is the
maximal set satisfying that property, we get $J\subseteq J_{n}$ and we have
proved the induction. It follows that $J\subseteq J_{n}$ for every
$n\in\mathbb{N}$. Moreover, since $J_{\infty}=\bigcap_{n\in\mathbb{N}}J_{n}$,
we deduce the inclusion $J\subseteq J_{\infty}$.

Now, assume that every $\mathbf{c}\in\mathbf{C}$ occurs in $e$ infinitely
often. Since $(J_{n})_{n\in\mathbb{N}}$ is a non increasing sequence of
$\\{1,\ldots,d\\}$, there exists $N$ such that $J_{n}=J_{\infty}$ for every
$n\geq N$. Let $\mathbf{c}\in\mathbf{C}$. There exists $n>N$ such that
$e_{n}=e_{n-1}\mathbf{c}$. From
$J_{n}=\operatorname{extract}_{\lambda,\\{\mathbf{c}\\}}(J_{n-1})$ and
$J_{n}=J_{n-1}=J_{\infty}$, we derive
$J_{\infty}=\operatorname{extract}_{\lambda,\\{\mathbf{c}\\}}(J_{\infty})$. In
particular $\mathbf{c}(j)<\lambda_{|J_{\infty}|}$ for every $j\in J_{\infty}$.
We have proved that $\mathbf{c}(j)<\lambda_{|J_{\infty}|}$ for every $j\in
J_{\infty}$ and for every $\mathbf{c}\in\mathbf{C}$. As $J_{\infty}\subseteq
I$, we deduce that $J_{\infty}$ is a $(\lambda,I)$-small set of $\mathbf{C}$.
Since $J$ is the maximal set satisfying that property, we deduce that
$J_{\infty}\subseteq J$. It follows that $J=J_{\infty}$.

###  11 Rackoff Extraction

A _$\sigma$ -execution_, where $\sigma=a_{1}\ldots a_{k}$ is a word of Petri
net actions, is a non-empty word of configurations
$e=\mathbf{c}_{0}\mathbf{c}_{1}\ldots\mathbf{c}_{k}$ such that
$\mathbf{c}_{0}\xrightarrow{a_{1}}\mathbf{c}_{1}\cdots\xrightarrow{a_{k}}\mathbf{c}_{k}$.
We denote by $\operatorname{src}(e)$ and $\operatorname{tgt}(e)$ the
configurations $\mathbf{c}_{0}$ and $\mathbf{c}_{k}$ respectively. An
_execution_ of a PN $A$ is a $\sigma$-execution for some $\sigma\in A^{*}$.

An execution $e$ is said to be _$I$ -cyclic_ for some
$I\subseteq\\{1,\ldots,d\\}$ if
$\operatorname{src}(e)|_{I}=\operatorname{tgt}(e)|_{I}$. We say that a word
$\sigma=\mathbf{a}_{1}\ldots\mathbf{a}_{k}$ of actions in a PN $A$ is obtained
from an execution $e$ of $A$ by removing $I$-cycles where
$I\subseteq\\{1,\ldots,d\\}$, if there exists a decomposition of $e$ into a
concatenation $e_{0}\ldots e_{k}$ of $I$-cyclic executions
$e_{0},\ldots,e_{k}$ such that
$\operatorname{tgt}(e_{j-1})\xrightarrow{a_{j}}\operatorname{src}(e_{j})$ for
every $1\leq j\leq k$.

An extractor $\lambda=(\lambda_{0}\leq\cdots\leq\lambda_{d+1})$ is said to be
_$m$ -adapted_ if for every $n\in\\{0,\ldots,d\\}$:

$\lambda_{n+1}\geq\lambda_{n}+m\lambda_{n}^{n}$

######  Lemma 11.1 (slight extension of [20]).

Let $\lambda$ be an $m$-adapted extractor and $e$ be an execution of a PN
$A\subseteq\\{0,\ldots,m\\}^{d}\times\mathbb{N}^{d}$. Let
$I\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\operatorname{extract}_{\lambda,e}(\\{1,\ldots,d\\})$.
There exists a word $\sigma$ that can be obtained from $e$ by removing
$I$-cycles such that $|\sigma|\leq d\lambda_{d}^{d}$ and such that
$\operatorname{src}(e)\xrightarrow{\sigma}\mathbf{c}$ for some configuration
$\mathbf{c}$ satisfying $\mathbf{c}(i)=\operatorname{tgt}(e)(i)$ for every
$i\in I$, and such that for every $i\not\in I$ we have:

$\mathbf{c}(i)\geq\lambda_{|I|+1}-m\sum_{j=1}^{|I|}\lambda_{j}^{j}$

######  Proof 11.2.

The proof follows a similar approach to the original one from Rackoff [20]. We
prove the lemma by induction over $d$. Naturally, if $d=0$ the lemma is
immediate. Assume the lemma proved for every dimension strictly smaller than
$d\geq 1$ and let us consider an $m$-adapted extractor
$\lambda=(\lambda_{0}\leq\cdots\leq\lambda_{d+1})$ and an $A^{*}$-execution
$e=\mathbf{c}_{0}\ldots\mathbf{c}_{k}$ for a PN
$A\subseteq\\{0,\ldots,m\\}^{d}\times\mathbb{N}^{d}$. We introduce
$J_{n}\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\operatorname{extract}_{\lambda,\mathbf{c}_{0}\ldots\mathbf{c}_{n-1}}(\\{1,\ldots,d\\})$
for every $n\in\\{0,\ldots,k+1\\}$. Since $J_{0}=\\{1,\ldots,d\\}$, there
exists a maximal $h\in\\{0,\ldots,k+1\\}$ such that $J_{h}=\\{1,\ldots,d\\}$.
For every $0\leq n<h$, since $J_{n}=\\{1,\ldots,d\\}$, we deduce that
$\mathbf{c}_{n}\in\\{0,\ldots,\lambda_{d}-1\\}^{d}$. It follows that the
cardinal of $\\{\mathbf{c}_{n}\mid 0\leq n<h\\}$ is bounded by
$\lambda_{d}^{d}$. Without loss of generality, by removing cycles from the
$A^{*}$-execution $e$, we can assume that
$\mathbf{c}_{0},\ldots,\mathbf{c}_{h-1}$ are distinct. It follows that
$h\leq\lambda_{d}^{d}$. Notice that if $h=k+1$ we are done. So, we can assume
that $h\leq k$.

Let us introduce
$J\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}J_{h+1}$. By maximality
of $h$, it follows that $J$ is strictly included in $\\{1,\ldots,d\\}$. We
introduce $d^{\prime}=|J|$. Thanks to a permutation of the components, we can
assume without loss of generality that $J=\\{1,\ldots,d^{\prime}\\}$. Lemma
10.5 shows that $\mathbf{c}_{h}(i)\geq\lambda_{d^{\prime}+1}$ for every
$i\in\\{d^{\prime}+1,\ldots,d\\}$. We let
$f:\mathbb{N}^{d}\mapsto\mathbb{N}^{d^{\prime}}$ be the function defined by
$f(\mathbf{z})=(\mathbf{z}(1),\ldots,\mathbf{z}(d^{\prime}))$ for every
$\mathbf{z}\in\mathbb{N}^{d}$. We also introduce the $d^{\prime}$-dimensional
extractor $\lambda^{\prime}=(\lambda_{0}\leq\cdots\leq\lambda_{d^{\prime}+1})$
and the PN
$A^{\prime}=\\{(f(\mathbf{a}_{-}),f(\mathbf{a}_{+}))\mid(\mathbf{a}_{-},\mathbf{a}_{+})\in
A\\}$. Let us introduce the $(A^{\prime})^{*}$-execution
$e^{\prime}=\mathbf{c}^{\prime}_{h+1}\ldots\mathbf{c}^{\prime}_{k}$ where
$\mathbf{c}^{\prime}_{n}\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}f(\mathbf{c}_{n})$,
and let us introduce the sequence $J^{\prime}_{h},\ldots,J^{\prime}_{k+1}$
defined by
$J^{\prime}_{n}\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\operatorname{extract}_{\lambda^{\prime},\mathbf{c}^{\prime}_{h}\ldots\mathbf{c}^{\prime}_{n-1}}(\\{1,\ldots,d^{\prime}\\})$
for every $n\in\\{h+1,\ldots,k+1\\}$.

Let us first prove that $J^{\prime}_{n}=J_{n}$ for every
$n\in\\{h+1,\ldots,k+1\\}$. First of all notice that
$J^{\prime}_{h+1}\subseteq J_{h+1}$. Moreover, for every $i\in J_{h+1}$ we
have $\mathbf{c}^{\prime}_{h}(i)<\lambda^{\prime}_{|J_{h+1}|}$. Hence
$J_{h+1}$ is a $(\lambda^{\prime},J^{\prime}_{h+1})$-small set of
$\\{\mathbf{c}^{\prime}_{h}\\}$. By maximality of $J^{\prime}_{h+1}$ we get
$J_{h+1}\subseteq J^{\prime}_{h+1}$. Hence $J^{\prime}_{h+1}=J_{h+1}$. Assume
by induction the property true for some $n\in\\{h+1,\ldots,k\\}$. Since
$J^{\prime}_{n+1}$ is a $(\lambda^{\prime},J^{\prime}_{n})$-small set of
$\\{\mathbf{c}_{n}^{\prime}\\}$, we deduce that $J^{\prime}_{n+1}\subseteq
J^{\prime}_{n}$ and
$\mathbf{c}^{\prime}_{n}(j)<\lambda^{\prime}_{|J^{\prime}_{n}|}$ for every
$j\in J^{\prime}_{n}$. As $J^{\prime}_{n}=J_{n}$, and
$\mathbf{c}^{\prime}_{n}(j)=\mathbf{c}_{n}(j)$ for every
$j\in\\{1,\ldots,d^{\prime}\\}$, we deduce that $J^{\prime}_{n}$ is a
$(\lambda,J_{n})$-small set of $\mathbf{c}_{n}$. By maximality of $J_{n+1}$,
we get $J^{\prime}_{n+1}\subseteq J_{n+1}$. Symmetrically, since $J_{n+1}$ is
a $(\lambda,J_{n})$-small set of $\mathbf{c}_{n}$, we deduce that
$J_{n+1}\subseteq J_{n}$ and $\mathbf{c}_{n}(j)<\lambda_{|J_{n}|}$ for every
$j\in J_{n}$. A $J^{\prime}_{n}=J_{n}$, we deduce that $J_{n}$ is a
$(\lambda^{\prime},J_{n}^{\prime})$-small set of $\mathbf{c}_{n}^{\prime}$. By
maximality of $J_{n+1}^{\prime}$, we get $J_{n+1}\subseteq J^{\prime}_{n+1}$.
We have proved that $J^{\prime}_{n}=J_{n}$ for every
$n\in\\{h+1,\ldots,k+1\\}$.

It follows that $J^{\prime}_{k+1}=J_{k+1}=I$. By induction, there exists a
word $\sigma^{\prime}$ that can be obtained from $e^{\prime}$ by removing
$I$-cycles such that

$|\sigma^{\prime}|\leq\sum_{j=1}^{d^{\prime}}\lambda_{j}^{j}$

and such that
$\mathbf{c}_{h}^{\prime}\xrightarrow{\sigma^{\prime}}\mathbf{c}^{\prime}$ for
some configuration $\mathbf{c}^{\prime}\in\mathbb{N}^{d^{\prime}}$ satisfying
$\mathbf{c}^{\prime}(i)=\mathbf{c}^{\prime}_{k}(i)$ for every $i\in I$ and
such that for every $i\in\\{1,\ldots,d^{\prime}\\}\backslash I$ we have:

$\mathbf{c}^{\prime}(i)\geq\lambda_{|I|+1}-m\sum_{j=0}^{|I|}\lambda_{j}^{j}$

Since $\sigma^{\prime}$ can be obtained from $e^{\prime}$ by removing
$I$-cycles, it follow that there exists a word $w$ that can be obtained from
$\mathbf{c}_{h}\ldots\mathbf{c}_{k}$ by removing $I$-cycles, and such that
$\sigma^{\prime}$ is the word obtained from $w$ by applying the function $f$
on each action. Notice that for every prefix $u$ of $w$ and for every
$i\in\\{d^{\prime}+1,\ldots,d\\}$ we have:

$\displaystyle\mathbf{c}_{h}(i)+\Delta(u)(i)$
$\displaystyle\geq\lambda_{d^{\prime}+1}-m|w|$
$\displaystyle\geq\lambda_{d^{\prime}+1}-m\sum_{j=1}^{d^{\prime}}\lambda_{j}^{j}$
$\displaystyle\geq\lambda_{|I|+1}-m\sum_{j=0}^{|I|}\lambda_{j}^{j}$

The last inequality is obtained by induction by observing that $\lambda$ is
$m$-adapted. We deduce that $\mathbf{c}_{h}(i)+\Delta(u)(i)\geq\lambda_{0}$
with the same kind of induction. In particular the configuration
$\mathbf{c}\in\mathbb{N}^{d}$ defined by
$\mathbf{c}(i)\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\mathbf{c}^{\prime}(i)$
if $i\in\\{1,\ldots,d^{\prime}\\}$ and
$\mathbf{c}(i)\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\mathbf{c}_{h+1}(i)+\Delta(w)(i)$
if $i\in\\{d^{\prime}+1,\ldots,d\\}$ satisfies
$\mathbf{c}_{h}\xrightarrow{w}\mathbf{c}$. Notice that
$\mathbf{c}(i)=\mathbf{c}_{k}(i)$ for every $i\in I$, and for every $i\not\in
I$, we have:

$\mathbf{c}(i)\geq\lambda_{|I|+1}-m\sum_{j=0}^{|I|}\lambda_{j}^{j}$

Let us introduce
$\sigma\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\mathbf{a}_{1}\ldots\mathbf{a}_{h}w$
where
$\mathbf{a}_{n}\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\mathbf{c}_{n}-\mathbf{c}_{n-1}$
for every $n\in\\{1,\ldots,h\\}$. Observe that
$\mathbf{c}_{0}\xrightarrow{\sigma}\mathbf{c}$ and moreover we have:

$|\sigma|\leq
h+\sum_{j=1}^{d^{\prime}}\lambda_{j}^{j}\leq\sum_{j=1}^{d}\lambda_{j}^{j}\leq
d\lambda_{d}^{d}$

We have proved the induction.

###  12 From SCCC to small unfoldings

We associate with an extractor $\lambda$ and a SCCC $\mathbf{C}$ of a PN $A$,
the set
$I\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\operatorname{extract}_{\lambda,\mathbf{C}}(\\{1,\ldots,d\\})$.
Notice that
$Q\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\mathbf{C}|_{I}$ is
finite since this set is included in
$\\{q\in\mathbb{N}^{I}\mid{\mathopen{\|}q\mathclose{\|}_{\infty}}<\lambda_{|I|}\\}$.
It follows that $G_{\mathbf{C},I}$ is a structurally-reversible $I$-unfolding.
We show in this section that for every $\mathbf{c}\in\mathbf{C}$ there exists
a kind of partial pumping pairs for $(\mathbf{c},G_{\mathbf{C},I})$.

Let us recall that an _infinite execution_ $e$ of $A$ is an infinite word of
configurations such that every finite non-empty prefix is an execution of $A$.
Let us prove the following technical lemma.

######  Lemma 12.1.

If $\mathbf{C}$ is not reduced to a singleton, there exists an infinite
execution $e\in\mathbf{C}^{\omega}$ of $A$ such that every configuration of
$\mathbf{C}$ occurs infinitely often in $e$.

######  Proof 12.2.

Since $\mathbf{C}$ is countable, there exists an infinite sequence
$(\mathbf{c}_{n})_{n\in\mathbb{N}}$ such that
$\mathbf{C}=\\{\mathbf{c}_{n}\mid n\in\mathbb{N}\\}$. Moreover, by replacing
that sequence by the sequence $s_{0},s_{1},\ldots$ where
$s_{n}\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\mathbf{c}_{0},\ldots,\mathbf{c}_{n}$,
we can assume without loss of generality that every configuration of
$\mathbf{C}$ occurs infinitely often in the sequence
$(\mathbf{c}_{n})_{n\in\mathbb{N}}$. Since $\mathbf{C}$ is a SCCC, for every
positive natural number $n$, there exists an $A^{*}$-execution from
$\mathbf{c}_{n-1}$ to $\mathbf{c}_{n}$ of the form $e_{n}\mathbf{c}_{n}$. Let
us introduce the word
$e\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}e_{1}e_{2}\ldots$. Notice
that since $\mathbf{C}$ is not reduced to a singleton, the word $e$ is
infinite. Moreover, notice that $e$ is an infinite execution satisfying the
lemma.

Now, assume that $\lambda$ is $m$-adapted for some positive natural number $m$
(this notion is introduced in the previous section).

######  Lemma 12.3.

If $A\subseteq\\{0,\ldots,m\\}^{d}\times\mathbb{N}^{d}$, for every
$\mathbf{c}\in\mathbf{C}$, there exists a cycle $\alpha$ in $G$ on
$\mathbf{c}|_{I}$ such that $|\alpha|\leq d\lambda_{d}^{d}$ and a
configuration $\mathbf{c}^{+}$ such that
$\mathbf{c}\xrightarrow{\alpha}\mathbf{c}^{+}$ and such that
$\mathbf{c}^{+}(i)\geq\lambda_{|I|+1}-m\sum_{j=1}^{|I|}\lambda_{j}^{j}$ for
every $i\not\in I$.

######  Proof 12.4.

Observe that if $\mathbf{C}$ is reduced to a singleton, the lemma is trivial
with $\alpha\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\varepsilon$.
So, we can assume that $\mathbf{C}$ is not a singleton. Lemma 12.1 shows that
there exists an infinite execution $e=\mathbf{c}_{0}\mathbf{c}_{1}\ldots$ of
configurations in $\mathbf{C}$ such that every configuration of $\mathbf{C}$
occurs infinitely often. Without loss of generality, by replacing $e$ by a
suffix of $e$ we can assume that $\mathbf{c}=\mathbf{c}_{0}$. Lemma 10.7 shows
that $\operatorname{extract}_{\lambda,e}(\\{1,\ldots,d\\})=I$. It follows that
there exists $N\in\mathbb{N}$ such that for every $n\geq N$ the prefix $e_{n}$
of $e$ of length $n$ satisfies
$\operatorname{extract}_{\lambda,e_{n}}(\\{1,\ldots,d\\})=I$. Since
$\mathbf{c}$ occurs infinitely often in $e$, there exists $n\geq N$ such that
$\mathbf{c}$ is the last configuration of $e_{n}$. Lemma 11.1 shows that there
exists a word $u$ that can be obtained from $e_{n}$ by removing $I$-cycles
such that $|u|\leq d\lambda_{d}^{d}$ and such that
$\mathbf{c}\xrightarrow{u}\mathbf{c}^{+}$ for some configuration
$\mathbf{c}^{+}$ satisfying
$\mathbf{c}^{+}(i)\geq\lambda_{|I|+1}-m\sum_{j=1}^{|I|}\lambda_{j}^{j}$ for
every $i\not\in I$. Since $u$ can be obtained from $e_{n}$ by removing
$I$-cycles, it follows that $u$ is the label of a cycle $\alpha$ on
$\mathbf{c}|_{I}$ in $G$.

Symmetrically, we deduce a similar backward property.

######  Lemma 12.5.

If $A\subseteq\mathbb{N}^{d}\times\\{0,\ldots,m\\}^{d}$, for every
$\mathbf{c}\in\mathbf{C}$, there exists a cycle $\beta$ in $G$ on
$\mathbf{c}|_{I}$ such that $|\beta|\leq d\lambda_{d}^{d}$ and a configuration
$\mathbf{c}^{-}$ such that $\mathbf{c}^{-}\xrightarrow{\beta}\mathbf{c}$, and
such that for every $i\not\in I$:
$\mathbf{c}^{-}(i)\geq\lambda_{|I|+1}-m\sum_{j=1}^{|I|}\lambda_{j}^{j}$.

######  Proof 12.6.

Let us introduce the PN
$A^{\prime}\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\\{(\mathbf{a}_{+},\mathbf{a}_{-})\mid(\mathbf{a}_{-},\mathbf{a}_{+})\in
A\\}$. Observe that $\mathbf{C}$ is a SCCC of $A^{\prime}$. Let $G^{\prime}$
be the $I$-unfolding associated to the extractor $\lambda$ and the SCCC
$\mathbf{C}$ of $A^{\prime}$. Lemma 13.3 shows that there exists a cycle in
$G^{\prime}$ on $\mathbf{c}|_{I}$ labeled by a word $u$ such that $|u|\leq
d\lambda_{d}^{d}$ and a configuration $\mathbf{c}^{-}$ such that
$\mathbf{c}\xrightarrow{u}\mathbf{c}^{-}$, and such that
$\mathbf{c}^{-}(i)\geq\lambda_{|I|+1}-m\sum_{j=1}^{|I|}\lambda_{j}^{j}$ for
every $i\not\in I$. Assume that $u=a_{1}^{\prime}\ldots a_{n}^{\prime}$ with
$a_{j}^{\prime}=(\mathbf{x}_{j},\mathbf{y}_{j})$ and let
$v\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}a_{n}\ldots a_{1}$ with
$a_{j}\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}(\mathbf{y}_{j},\mathbf{x}_{j})$.
Observe that since $u$ is the label of a cycle on $\mathbf{c}|_{I}$ in
$G^{\prime}$, then $v$ is the label of a cycle on $\mathbf{c}|_{I}$ in $G$.
Moreover, from $\mathbf{c}\xrightarrow{v}\mathbf{c}^{-}$ we derive
$\mathbf{c}^{-}\xrightarrow{v}\mathbf{c}$. We have proved the lemma.

###  13 Proof of Lemma 5.5

In this section, we prove Lemma 5.5. We consider a PN $A$ and a SCCC
$\mathbf{C}$ of $A$. We introduce
$m\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}{\mathopen{\|}A\mathclose{\|}_{\infty}}$.
If $m=0$, the proof is immediate. So, we can assume that $m\geq 1$.

We introduce the extractor $\lambda$ satisfying $\lambda_{0}=1$, and for every
$n\in\\{0,\ldots,d\\}$:

$\lambda_{n+1}\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}m\sum_{j=1}^{n}\lambda_{j}^{j}+m\lambda_{n}^{3n}(3d\lambda_{n}^{n}m)^{d}$

Observe that $\lambda$ is $m$-adapted.

We introduce
$b\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\lambda_{d}$, the set
$I\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}\operatorname{extract}_{\lambda,\mathbf{C}}(\\{1,\ldots,d\\})$,
and the structurally-reversible $I$-unfolding $G=(Q,A,T)$ associated to
$\mathbf{C}$ (defined in the previous section), $\lambda$ and $A$. Notice that
$Q\subseteq\\{q\in\mathbb{N}^{I}\mid{\mathopen{\|}q\mathclose{\|}_{\infty}}<\lambda_{|I|}\\}$.
Denoting by $r\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}|Q|$, we
deduce that $r\leq\lambda_{|I|}^{|I|}$.

Observe that for every $\mathbf{x},\mathbf{y}\in\mathbf{C}$, we have
$\mathbf{y}-\mathbf{x}\in L_{\mathbf{x}|_{I},G,\mathbf{y}|_{I}}$. Moreover
$Q\subseteq\\{q\in\mathbb{N}^{I}\mid{\mathopen{\|}q\mathclose{\|}_{\infty}}<b\\}$
since $\lambda_{|I|}\leq b$. The following lemma provides a bound on $b$.

######  Lemma 13.1.

We have $b\leq(3dm)^{(d+2)^{2d+1}}$.

######  Proof 13.2.

Notice that
$\lambda_{n+1}=m\sum_{j=1}^{n}\lambda_{j}^{j}+m\lambda_{n}^{3n}(3d\lambda_{n}^{n}m)^{d}\leq
mn\lambda_{n}^{n}+m\lambda_{n}^{3n}(3d\lambda_{n}^{n}m)^{d}\leq
md\lambda_{n}^{3d}+m\lambda_{n}^{3d}(3d\lambda_{n}m)^{d^{2}}\leq(3d\lambda_{n}m)^{d^{2}+3d}$.
By induction on $n$, we deduce that $\lambda_{n}\leq(3dm)^{n(d^{2}+3d)^{n}}$.
In particular, we have $b\leq(3dm)^{s}$ where
$s\stackrel{{\scriptstyle\textrm{{\tiny{def}}}}}{{=}}d(d^{2}+3d)^{d}\leq(d+2)^{2d+1}$.

######  Lemma 13.3.

We have $\mathbf{c}\in\mathbf{U}_{\mathbf{c}|_{I},G}$ for every
$\mathbf{c}\in\mathbf{C}$.

######  Proof 13.4.

Lemma 12.3 and Lemma 12.5 show that there exist $u,v\in A^{*}$ that label
cycles $\alpha,\beta$ in $G$ on $\mathbf{c}|_{I}$ such that $|u|,|v|\leq
db^{d}$, and two configurations $\mathbf{c}^{-},\mathbf{c}^{+}$ such that
$\mathbf{c}^{-}\xrightarrow{u}\mathbf{c}\xrightarrow{v}\mathbf{c}^{+}$, and
such that
$\mathbf{c}^{-}(i),\mathbf{c}^{+}(i)\geq\lambda_{|I|+1}-m\sum_{j=1}^{|I|}\lambda_{j}^{j}$
for every $i\not\in I$. Notice that
$\lambda_{|I|+1}-m\sum_{j=1}^{|I|}\lambda_{j}^{j}=m(\lambda_{|I|}^{|I|})^{3}(3d\lambda_{|I|}^{|I|}m)^{d}\geq
mr^{3}(3drm)^{d}$. It follows that $(u,v)$ is a pumping pair for
$(\mathbf{c}|_{I},G)$.

##  Part V Conclusion

This paper provides a way for computing a quantifier free Presburger formula
$\phi_{A}(\mathbf{x},\mathbf{y})$ encoding the mutual reachability relation of
a Petri net $A$ between two configurations $\mathbf{x},\mathbf{y}$. We also
provided in Theorem 6.3 a Presburger formula encoding the set of bottom
configurations. This formula introduces quantified sub-formulas of the form
$\forall\mathbf{v}\in\llbracket{\gamma}\rrbracket\phi(\mathbf{c}+\mathbf{v})$
or equivalently
$\exists\mathbf{v}\in\llbracket{\gamma}\rrbracket\neg\phi(\mathbf{c}+\mathbf{v})$
where $\gamma$ is a representation of a lattice, and $\phi$ is a threshold
formula. In order to obtain a quantifier-free formula, by putting $\neg\phi$
in disjunctive normal form, it is sufficient to provide a way to encode in the
quantifier-free fragment of the Presburger arithmetic the following set:

$(I_{1}\times\cdots\times
I_{d})+\mathbb{Z}\mathbf{p}_{1}+\cdots+\mathbb{Z}\mathbf{p}_{k}$

where $I_{1},\ldots,I_{d}$ are intervals of $\mathbb{Z}$ and
$\mathbf{p}_{1},\ldots,\mathbf{p}_{k}$ are vectors in $\mathbb{Z}^{d}$. We
left this problem open.

The author thanks Petr Jančar for discussions motivating this work.

### References

  * [1] Gérard Basler, Michele Mazzucchi, Thomas Wahl, and Daniel Kroening.  Symbolic counter abstraction for concurrent software.  In CAV, volume 5643 of Lecture Notes in Computer Science, pages 64–78. Springer, 2009.
  * [2] Eike Best and Javier Esparza.  Existence of home states in petri nets is decidable.  Inf. Process. Lett., 116(6):423–427, 2016.
  * [3] Michael Blondin, Alain Finkel, Christoph Haase, and Serge Haddad.  Approaching the coverability problem continuously.  In Marsha Chechik and Jean-François Raskin, editors, Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, volume 9636 of Lecture Notes in Computer Science, pages 480–496. Springer, 2016.
  * [4] E. Cardoza, Richard J. Lipton, and Albert R. Meyer.  Exponential space complete problems for Petri nets and commutative semigroups: Preliminary report.  In STOC’76, pages 50–54. ACM, 1976.  doi:10.1145/800113.803630.
  * [5] Wojciech Czerwinski and Lukasz Orlikowski.  Reachability in vector addition systems is ackermann-complete.  In 62nd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2021, Denver, CO, USA, February 7-10, 2022, pages 1229–1240. IEEE, 2021.  doi:10.1109/FOCS52979.2021.00120.
  * [6] Alex Dixon and Ranko Lazic.  Kreach: A tool for reachability in petri nets.  In Armin Biere and David Parker, editors, Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part I, volume 12078 of Lecture Notes in Computer Science, pages 405–412. Springer, 2020.  doi:10.1007/978-3-030-45190-5\\_22.
  * [7] Javier Esparza, Pierre Ganty, Jérôme Leroux, and Rupak Majumdar.  Verification of population protocols.  Acta Inf., 54(2):191–215, 2017.
  * [8] Moses Ganardi, Rupak Majumdar, Andreas Pavlogiannis, Lia Schütze, and Georg Zetzsche.  Reachability in bidirected pushdown VASS.  In Mikolaj Bojanczyk, Emanuela Merelli, and David P. Woodruff, editors, 49th International Colloquium on Automata, Languages, and Programming, ICALP 2022, July 4-8, 2022, Paris, France, volume 229 of LIPIcs, pages 124:1–124:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022.  doi:10.4230/LIPIcs.ICALP.2022.124.
  * [9] Thomas Geffroy, Jérôme Leroux, and Grégoire Sutre.  Occam’s razor applied to the petri net coverability problem.  Theor. Comput. Sci., 750:38–52, 2018.
  * [10] V. S. Grinberg and S. V. Sevast’yanov.  Value of the steinitz constant.  Functional Analysis and Its Applications, 14(2):125–126, Apr 1980\.  doi:10.1007/BF01086559.
  * [11] Michel Hack.  Decidability questions for Petri Nets.  PhD thesis, Massachusetts Institute of Technology, Cambridge, MA, USA, 1976.  URL: https://hdl.handle.net/1721.1/27441.
  * [12] Petr Jancar, Jérôme Leroux, and Grégoire Sutre.  Co-finiteness and co-emptiness of reachability sets in vector addition systems with states.  In Petri Nets, volume 10877 of Lecture Notes in Computer Science, pages 184–203. Springer, 2018.
  * [13] Jérôme Leroux.  Vector addition system reversible reachability problem.  Logical Methods in Computer Science, 9(1), 2013.
  * [14] Jérôme Leroux.  Distance between mutually reachable petri net configurations.  In Arkadev Chattopadhyay and Paul Gastin, editors, 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2019, December 11-13, 2019, Bombay, India, volume 150 of LIPIcs, pages 47:1–47:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019.  doi:10.4230/LIPIcs.FSTTCS.2019.47.
  * [15] Jérôme Leroux.  The reachability problem for petri nets is not primitive recursive.  In 62nd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2021, Denver, CO, USA, February 7-10, 2022, pages 1241–1252. IEEE, 2021.  doi:10.1109/FOCS52979.2021.00121.
  * [16] Jérôme Leroux, M. Praveen, and Grégoire Sutre.  A relational trace logic for vector addition systems with application to context-freeness.  In CONCUR, volume 8052 of Lecture Notes in Computer Science, pages 137–151. Springer, 2013.
  * [17] Jérôme Leroux and Sylvain Schmitz.  Reachability in vector addition systems is primitive-recursive in fixed dimension.  In LICS. IEEE Computer Society, 2019.  to appear.
  * [18] Jérôme Leroux and Grégoire Sutre.  On flatness for 2-dimensional vector addition systems with states.  In CONCUR, volume 3170 of Lecture Notes in Computer Science, pages 402–416. Springer, 2004.
  * [19] Loic Pottier.  Minimal solutions of linear diophantine systems: Bounds and algorithms.  In R. V. Book, editor, Proceedings 4th Conference on Rewriting Techniques and Applications, Como (Italy), volume 488 of Lecture Notes in Computer Science, pages 162–173. Springer, 1991.
  * [20] C. Rackoff.  The covering and boundedness problems for vector addition systems.  Theoretical Computer Science, 6(2):223–231, 1978.
  * [21] Alexander Schrijver.  Theory of Linear and Integer Programming.  John Wiley & Sons, Inc., USA, 1986.