University of<EMAIL_ADDRESS>by the
ERC grant INFSYS, agreement no. 950398. University of
<EMAIL_ADDRESS>Wojciech Czerwiński, Adam Jędrych
[500]Theory of computation Parallel computing models 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

# Long Runs Imply Big Separators in Vector Addition Systems

Wojciech Czerwiński  Adam Jędrych

###### Abstract

Despite recent progress which settled the complexity of the reachability
problem for Vector Addition Systems with States (VASSes) as being Ackermann-
complete we still lack much understanding for that problem. A striking example
is the reachability problem for three-dimensional VASSes (3-VASSes): it is
only known to be PSpace-hard and not known to be elementary. One possible
approach which turned out to be successful for many VASS subclasses is to
prove that to check reachability it suffices to inspect only runs of some
bounded length. This approach however has its limitations, it is usually hard
to design an algorithm substantially faster than the possible size of finite
reachability sets in that VASS subclass. It motivates a search for other
techniques, which may be suitable for designing fast algorithms. In 2010
Leroux has proven that non-reachability between two configurations implies
separability of the source from the target by some semilinear set, which is an
inductive invariant. There can be a reasonable hope that it suffices to look
for separators of bounded size, which would deliver an efficient algorithm for
VASS reachability. In the paper we show that also this approach meets an
obstacle: in VASSes fulfilling some rather natural conditions existence of
only long runs between some configurations implies existence of only big
separators between some other configurations (and in a slightly modified
VASS). Additionally we prove that a few known examples of involved VASSes
fulfil the mentioned conditions. Therefore improving the complexity of the
reachability problem (for any subclass) using the separators approach may not
be simpler than using the short run approach.

###### keywords:

Vector Addition Systems, reachability problem, separators, semilinear sets

##  1 Introduction

The complexity of the reachability problem for Vector Addition Systems (VASes)
was a challenging and natural problem for a few decades of research. The first
result about its complexity was ExpSpace-hardness by Lipton in 1976 [17].
Decidability was shown by Mayr in 1981 [18]. Later the construction of Mayr
was further simplified and presented in a bit different light by Kosaraju [11]
and Lambert [12]. This construction is currently known under the name KLM
decomposition after the three main inventors. The first complexity upper bound
was obtained by Leroux and Schmitz as recent as in 2016 [15], where the
reachability problem was shown to be solvable in cubic-Ackermann time. A few
years later the same authors have shown that the problem can be solved in
Ackermann time and actually in primitive recursive time, when the dimension is
fixed [16]. At the same time a lower bound of Tower-hardness was established
for the reachability problem [4, 6]. Last year two independent papers have
shown Ackermann-hardness of the reachability problem [14, 7] thus settling the
complexity of the problem to be Ackermann-complete.

However, despite this recent huge progress we still lack much understanding
about the reachability problem in VASSes. The most striking example is the
problem for dimension three. The best known lower bound for the reachability
problem for 3-VASSes is PSpace-hardness inherited from the hardness result for
2-VASSes [1], while the best known upper bound is much bigger then Tower.
Concretely speaking the problem can be solved in time $\mathcal{F}_{7}$ [16],
where $\mathcal{F}_{\alpha}$ is the hierarchy of fast-growing complexity
classes, see [20] (recall that $\textup{Tower}=\mathcal{F}_{3}$). Similarly
for other low dimensional VASSes the situation is unclear. Currently the
smallest dimension $d$ for which an ExpSpace-hardness is known for $d$-VASSes
is $d=6$ and for which a Tower-hardness is known is $d=8$ [8]. Therefore for
any $d\in[3,5]$ the problem can be in PSpace and is not known to be elementary
and for $d\in[6,7]$ the problem can be elementary. For some of those
dimensions one can hope to get better hardness results in the future, but we
conjecture that for $3$-VASSes and $4$-VASSes the reachability problem
actually is elementary and the challenge is to find this algorithm. This
complexity gap is just one witness of our lack of understanding of the
structure of VASSes. One can hope that in the future we will be able to design
efficient algorithms for the reachability problem even for VASSes in high
dimensions under the condition that they belong to some subclass, for example
they avoid some hard patterns. This can be quite important from a practical
point of view. Understanding for which classes efficient (say PSpace)
algorithms are possible may be thus another future goal. Therefore we think
that the quest for better understanding the reachability problem is still
valid, even though the complexity of the reachability problem for general
VASSes is settled.

A common and very often successful approach to the reachability problem is
proving a short run property, namely showing that in order to decide
reachability it suffices to inspect only runs of some bounded length. This
technique was exploited a lot in the area of VASSes. Rackoff proved his
ExpSpace upper bound on the complexity of the coverability problem [19] using
this approach: he has shown that if there exists a covering run, then there
exists also a covering run of at most doubly-exponential length. Recently
there was a lot of research about low dimensional VASSes and the technique of
bounded run length was also used there. In [1] authors established complexity
of the reachability problem for 2-VASSes to PSpace-completeness by proving
that in order to decide reachability it suffices to inspect runs of at most
exponential length. Similarly in the next paper in this line of research [9]
it was shown that in 2-VASSes with unary transition representation it suffices
to consider runs of polynomial length, which proves NL-completeness of the
reachability problem.

This approach however meets a subtle obstacle when one tries to prove some
upper bound on the complexity of the reachability problem in say $d$-VASSes.
In order to show a bounded length property it is natural to try to unpump long
runs in some way. Unpumping however can be very tricky when the run is close
to some of the axes, as only a small modification of the run may cause some
counters to become negative. A common approach to that problem is to modify a
run when all its counters are high and therefore local run modifications
cannot cause any problem. Such an approach is used for example in 2-VASSes [1]
and in the KLM decomposition [11, 12, 18]. However, not all the runs may have
a configuration with all counter values high. Therefore it is very convenient
to have a cycle, which increases all the counters simultaneously. Observe that
existence of such a cycle implies that the set of reachable configurations is
infinite. Thus using this approach is challenging in the case when the
reachability set is finite. For finite set in turn it is hard to design
algorithm substantially faster than the size of the reachability set. It is
well known that in $d$-VASSes finite reachability sets can be as large as
$F_{d-1}(n)$, where $n$ is the VASS size and $F_{\alpha}$ is the hierarchy of
very fast growing functions, see [20]. Therefore designing an algorithm
breaking $F_{d-1}(n)$ time for the reachability problem in $d$-VASSes (if such
exist) may need some other approach. Breaking the barrier of the size of
finite reachability set is possible in general, but probably in many cases
very challenging. To the best of our knowledge the only nontrivial algorithm
breaking it is the one in [9] doing a sophisticated analysis of possible
behaviours of runs in 2-VASSes. This motivates a search for other techniques,
which may be more suitable for designing fast algorithms.

Leroux in his work [13] provided an algorithm for the reachability problem,
which follows a completely different direction. He has shown that if there is
no run from a configuration $s\in\mathbb{N}^{d}$ to a configuration
$t\in\mathbb{N}^{d}$ in a VAS $V$ then there exists a semilinear set $S$,
called a _separator_ , which (1) contains $s$, (2) does not contain $t$ and
(3) is an _inductive invariant_ , namely if $v\in S$ then also $v+t\in S$ for
any transition $t$ of $V$ such that $v+t\in\mathbb{N}^{d}$. Notice that
existence of a separator clearly implies non-reachability between $s$ and $t$,
so by Leroux’s work non-reachability and existence of separator are
equivalent. Then the following simple algorithm decides whether $t$ is
reachable from $s$: run two semi-procedures, one looks for possible runs
between $s$ and $t$, longer and longer, another one looks for possible
separators between $s$ and $t$, bigger and bigger. Clearly either there exists
a run or there exists a separator, so at some point the algorithm will find it
and terminate. From this perspective one can view runs and separators as dual
objects. If bounding the length of a run is nontrivial, maybe bounding the
size of a separator can be another promising approach. Notice that proving for
example an $F_{d}(n)$ upper bound on the size of separators would provide an
algorithm solving the reachability problem which works in time at most
exponential $F_{d}(n)$, which is still $F_{d}(\mathcal{O}(n))$ for $d\geq 3$.

##### Our contribution

Our main contribution are two theorems stating that in VASSes fulfilling
certain rather natural conditions if there are only long runs between some of
its two configurations then in a small modification of these VASSes there are
only big separators for some other two configurations. We designed Theorem 3.1
to have relatively simple statement, but also to be sufficiently strong for
our applications. Theorem 5.2 needs more sophisticated notions and more
advanced tools to be proven, but it has potentially a broader spectrum of
applications.

Additionally we have shown that two nontrivial constructions of involved
VASSes, namely the 4-VASS from [5] and VASS used in the Tower-hardness
construction from [4] fulfil the conditions proposed by us in Theorem 3.1.
This indicates that for each VASS subclass $\mathcal{F}$ (for example
$3$-VASSes) either (1) in order to prove better upper complexity bound for the
reachability problem in $\mathcal{F}$ one should focus more on proving the
short run property than on proving the small separator property or (2) proving
small separator property is somehow possible for $\mathcal{F}$. However, in
the latter case the mentioned VASS has to be constructed by the use of rather
different techniques than currently known, as it needs to violate conditions
of Theorems 3.1 and 5.2.

We have not considered VASSes occurring in the most recent papers proving the
Ackermann-hardness [14, 7], but it seems to us that these techniques are
promising at least with respect to VASSes occurring in [7].

##### Organisation of the paper

In Section 2 we introduce preliminary notions and recall standard facts. Then
in Section 3 we state and prove our first main result, Theorem 3.1. In Section
4 we provide two applications of Theorem 3.1, in Section 4.1 to the $4$-VASS
described in [5] and in Section 4.2 to VASSes occurring in the paper [4]
proving the Tower-hardness of the reachability problem. Finally, in Section 5
we prove our second main result, Theorem 5.2.

##  2 Preliminaries

##### Basic notions

We denote by $\mathbb{N}$ the set of nonnegative integers and by
$\mathbb{N}_{+}$ the set of positive integers. For $a,b\in\mathbb{N}$ by
$[a,b]$ we denote the set $\\{a,a+1,\ldots,b-1,b\\}$. For a set $S$ we write
$|S|$ to denote its size, i.e. the number of its elements. For two sets $A,B$
we define $A+B=\\{a+b\mid a\in A,b\in A\\}$ and $AB=\\{a\cdot b\mid a\in
A,b\in B\\}$. In that context we often simplify the notation and write $x$
instead of the singleton set $\\{x\\}$, for example $x+\mathbb{N}y$ denotes
the set $\\{x\\}+\mathbb{N}\\{y\\}$. The _description size_ of an irreducible
fraction $\frac{p}{q}$ is $\max(|p|,|q|)$, for $r\in\mathbb{Q}$ its
description size is the description size of its irreducible form.

For a $d$-dimensional vector $x=(x_{1},\ldots,x_{d})\in\mathbb{R}^{d}$ and
index $i\in[1,d]$ we write $x[i]$ for $x_{i}$. For $S\subseteq[1,d]$ we write
$\textup{proj}_{S}(x)$ to denote the $|S|$-dimensional vector obtained from
$x$ by removing all the coordinates outside $S$. The _norm_ of a vector
$x\in\mathbb{N}^{d}$ is $\textup{norm}(x)=\max_{i\in[1,d]}|x[i]|$. For
$i\in[1,d]$ the elementary vector $e_{i}$ is the unique vector such that
$e_{i}[j]=0$ for $j\neq i$ and $e_{i}[i]=1$. By $0^{d}\in\mathbb{N}^{d}$ we
denote the $d$-dimensional vector with all the coordinates being zero.

##### Vector Addition Systems

A $d$-dimensional Vector Addition System with States (shortly $d$-VASS or just
a VASS) consists of finite set of _states_ $Q$ and finite set of _transitions_
$T\subseteq Q\times\mathbb{Z}^{d}\times Q$. _Configuration_ of a $d$-VASS
$V=(Q,T)$ is a pair $(q,v)\in Q\times\mathbb{N}^{d}$, we often write $q(v)$
instead of $(q,v)$. For a configuration $c=q(v)$ we write
$\textup{state}(c)=q$. For a set of vectors $S\subseteq\mathbb{N}^{d}$ and
state $q\in Q$ we write $q(S)=\\{q(v)\mid v\in S\\}$. Transition $t=(p,u,q)$
can be fired in configuration $(r,v)\in Q\times\mathbb{N}^{d}$ if $p=r$ and
$u+v\in\mathbb{N}^{d}$. Then we write $p(v)\stackrel{{\scriptstyle
t}}{{\longrightarrow}}q(u+v)$. The triple $(p(u),t,q(u+v))$ is called an
_anchored transition_. A _run_ is a sequence of anchored transitions
$\rho=(c_{1},u_{1},c_{2}),\ldots,(c_{n},u_{n},c_{n+1})$. Such a run $\rho$ is
then a run _from_ configuration $c_{1}$ _to_ configuration $c_{n+1}$ and
_traverses_ through configurations $c_{i}$ for $i\in[2,n]$. We also say that
$\rho$ is from $\textup{state}(c_{1})$ to $\textup{state}(c_{n+1})$. If there
is a run from configuration $c$ to configuration $c^{\prime}$ we also say that
$c^{\prime}$ is _reachable_ from $c$ or $c$ _reaches_ $c^{\prime}$ and write
$c\longrightarrow c^{\prime}$. Otherwise we write $c\centernot\longrightarrow
c^{\prime}$. The configuration $c$ is the _source_ of $\rho$ while
configuration $c^{\prime}$ is the _target_ of $\rho$, we write
$\textup{src}(\rho)=c$ and $\textup{trg}(\rho)=c^{\prime}$. For a
configuration $c\in Q\times\mathbb{N}^{d}$ we denote
$\textsc{post}_{V}(c)=\\{c^{\prime}\mid c\longrightarrow c^{\prime}\\}$ the
set of all the configurations reachable from $c$ and ${\rm
Phys.\leavevmode\nobreak\ Rev.\leavevmode\nobreak\ E}_{V}(c)=\\{c^{\prime}\mid
c^{\prime}\longrightarrow c\\}$ the set of all the configurations which reach
$c$. The _reachability problem for VASSes_ given a VASS $V$ and two its
configurations $s$ and $t$ asks whether $s$ reaches $t$ in $V$. For a VASS $V$
by its _size_ we denote the total number of bits needed to represent its
states and transitions. A VASS is said to be _binary_ if numbers in its
transitions are encoded in binary. Effect of a transition $(c,u,c^{\prime})\in
Q\times\mathbb{Z}^{d}\times Q$ is the vector $u\in\mathbb{N}^{d}$. We extend
this notion naturally to anchored transitions and runs, effect of the run
$\rho=(c_{1},u_{1},c_{2}),\ldots,(c_{n},u_{n},c_{n+1})$ is equal to
$u_{1}+\ldots+u_{n}$. Vector Addition Systems (VASes) are VASSes with just one
state or in other words VASSes without states. It is well known and simple to
show that the reachability problems for VASes and for VASSes are polynomially
interreducible. In this work we focus wlog. on the reachability problem for
VASSes.

##### Semilinear sets

For any vectors $b,v_{1},\ldots,v_{k}\in\mathbb{N}^{d}$ the set
$L=b+\mathbb{N}v_{1}+\ldots+\mathbb{N}v_{k}$ is called a _linear_ set. Then
vector $b$ is the _base_ of $L$ and vectors $v_{1},\ldots,v_{k}$ are _periods_
of $L$. Set of vectors is _semilinear_ if it is a finite union of linear sets.
Set of VASS configurations $S\subseteq Q\times\mathbb{N}^{d}$ is _semilinear_
if it is a finite union of sets of the form $q_{i}(S_{i})\subseteq
Q\times\mathbb{N}^{d}$, where $S_{i}$ are semilinear as sets of vectors. The
_size_ of a representation of a linear set is the sum of norms of its base and
periods. The _size_ of a representation of a semilinear set $\bigcup_{i}L_{i}$
is the sum of sizes of representations of the sets $L_{i}$. The size of a
semilinear set is the size of its smallest representation.

For a $d$-VASS $V=(Q,T)$ and two of its configurations $s,t\in
Q\times\mathbb{N}^{d}$ a set $S\subseteq Q\times\mathbb{N}^{d}$ of
configurations is a _separator for $(V,s,t)$_ if it fulfils the following
conditions: 1) $s\in S$, 2) $t\not\in S$, 3) $S$ is invariant under
transitions of $V$, namely for any $c\in S$ such that
$c\stackrel{{\scriptstyle t}}{{\longrightarrow}}c^{\prime}$ for some $t\in T$
we also have $c^{\prime}\in S$. In our work we usually do not exploit by
condition 3) by itself, but use the facts which are implied by all the
conditions 1), 2) and 3) together: $\textsc{post}(s)\subseteq S$ and ${\rm
Phys.\leavevmode\nobreak\ Rev.\leavevmode\nobreak\ E}(t)\cap S=\emptyset$.

##### Well quasi-order on runs

We say that an order $(X,\preceq)$ is a well-quasi order (wqo) if in every
infinite sequence $x_{1},x_{2},\ldots$ of elements of $X$ there is a
_domination_ , i.e. there exist $i<j$ such that $x_{i}\preceq x_{j}$.

Fix a $d$-VASS $V=(Q,T)$. We define here a very useful order on runs, which
turns out to be a wqo (a weaker version was originally introduced in [10]).
For two configurations $p(u),q(v)\in Q\times\mathbb{N}^{d}$ we write
$p(u)\preceq q(v)$ if $p=q$ and $u[i]\leq v[i]$ for each $i\in[1,d]$. For two
anchored transitions in
$(c_{1},t,c_{2}),(c^{\prime}_{1},t^{\prime},c^{\prime}_{2})$ we write
$(c_{1},t,c_{2})\preceq(c^{\prime}_{1},t^{\prime},c^{\prime}_{2})$ if
$t=t^{\prime}$, $c_{1}\preceq c^{\prime}_{1}$ and $c_{2}\preceq
c^{\prime}_{2}$ (notice that the last condition is actually implied by the
previous two). For two runs $\rho=m_{1}\ldots m_{k}$ and
$\rho^{\prime}=m^{\prime}_{1}\ldots m^{\prime}_{\ell}$, where all $m_{i}$ for
$i\in[1,k]$ and $m^{\prime}_{i}$ for $i\in[1,\ell]$ are anchored transitions
we write $\rho\unlhd\rho^{\prime}$ if and there exists a sequence of indices
$i_{1}<i_{2}<\ldots<i_{k-1}<i_{k}=\ell$ such that for each $j\in[1,k]$ we have
$m_{j}\preceq m^{\prime}_{i_{j}}$. Notice there that setting $i_{k}=\ell$
implies that $\textup{trg}(\rho)\preceq\textup{trg}(\rho^{\prime})$. All the
subsequent considerations can be analogously applied in the case when we
demand $\textup{trg}(\rho)=\textup{trg}(\rho^{\prime})$ and $i_{1}=1$, but
$i_{k}$ does not necessarily equal $\ell$, which enforces that
$\textup{src}(\rho)\preceq\textup{src}(\rho^{\prime})$. The following claim is
a folklore, for a proof see Proposition 19 in [3].

######  Claim 1.

Order $\unlhd$ is a wqo on runs with the same source.

The order $\unlhd$ has a nice property that runs bigger than a fixed one are
additive in a certain sense. The following claim is also a folklore, for a
proof see Lemma 23 in [2] (arXiv version of [3]).

######  Claim 2.

Let $\rho$, $\rho_{1}$ and $\rho_{2}$ be runs of VASS $V$ with
$\textup{src}(\rho)=\textup{src}(\rho_{1})=\textup{src}(\rho_{2})$ such that
$\rho\unlhd\rho_{1},\rho_{2}$,
$\textup{trg}(\rho_{1})=\textup{trg}(\rho)+\delta_{1}$ and
$\textup{trg}(\rho_{2})=\textup{trg}(\rho)+\delta_{2}$ for some
$\delta_{1},\delta_{2}\in\mathbb{N}^{d}$. Then there exist a run
$\rho^{\prime}$ such that $\textup{src}(\rho)=\textup{src}(\rho^{\prime})$,
$\rho\unlhd\rho^{\prime}$ and
$\textup{trg}(\rho^{\prime})=\textup{trg}(\rho)+\delta_{1}+\delta_{2}$.

The following corollary can be easily shown by induction on $n$.

######  Corollary 2.1.

Let $\rho\unlhd\rho^{\prime}$ be runs of VASS $V$ such that
$\textup{src}(\rho^{\prime})=\textup{src}(\rho)$ and
$\textup{trg}(\rho^{\prime})=\textup{trg}(\rho)+\delta$ for some
$\delta\in\mathbb{N}^{d}$. Then for any $n\in\mathbb{N}$ there exists a run
$\rho_{n}$ of $V$ such that $\textup{src}(\rho_{n})=\textup{src}(\rho)$ and
$\textup{trg}(\rho_{n})=\textup{trg}(\rho)+n\delta$.

The above notions will be useful in the proof of Theorem 5.2.

##  3 Main tool

In this section we state and prove our first main result, Theorem 3.1. It is
simpler both in the formulation and in the proof from the more involved
Theorem 5.2, but sufficient to show applications in Section 4.

The statement of Theorem 3.1 may seem at first glance a bit artificially
involved thus before stating it we explain the intuition behind this research
direction. Recently there is a big progress in showing lower complexity bounds
for the reachability problem in VASSes. On the intuitive level proving a new
lower bound often boils down to finding a new source of hardness in VASSes or
in other words designing a family of VASSes which is involved in some sense.
In particular these involved VASSes should have a run from some source
configuration to some target configuration, but each such run should be long.
For some reason VASS families proposed in a number of recent constructions
share many similarities. The first one is that the runs from the source to the
target usually have some very specific shape and there is exactly one shortest
run. Along this run usually some very restrictive invariants are kept and any
deviation from them results in the impossibility of reaching the target
configuration. To our best knowledge the same schema reappears in all the
known lower bound results, in particular in the recent ones [6, 5, 14, 7, 8].
In many of these constructions the following invariant is kept: product of
some two counters $x$ and $y$ equals the other counter $z$ where the counter
$x$ is bounded, while $y$ and $z$ are unbounded. In other words the ratio
$y/z$ is fixed and bounded at some point at the run. The reason behind this
phenomenon is the use of so called multiplication triples technique introduced
in [4]. Theorem 3.1 tries to describe this situation more precisely and state
that in some way for VASSes following this popular line of design we might
expect to have troubles with avoiding big separators. Because assumptions of
Theorem 3.1 are actually very strong and restrictive we formulate also Theorem
5.2 in Section 5 which tries to take a bit more flexible approach for making
the above described phenomena more precise. Notice that in Theorem 3.1 we
describe VASSes with no run from $s$ to $t$, but there is a close resemblance
to the above described setting as there is a run from $s+e_{2}$ to $t$.

######  Theorem 3.1.

Let $V$ be a $d$-VASS, $s,t\in Q\times\mathbb{N}^{d}$ be two its
configurations, $q\in Q$ be a state and a line $\alpha=a+\mathbb{N}\Delta$ for
vectors $a,\Delta\in\mathbb{N}^{d}$ be such that

  1. (1)

$\Delta=(\Delta[1],\Delta[2],0^{d-2})\in\mathbb{N}^{d}$,

  2. (2)

there is no run from $s$ to $t$,

  3. (3)

$q(\alpha)\subseteq\textsc{post}_{V}(s)$,

  4. (4)

$q(\alpha+\mathbb{N}_{+}e_{2})\subseteq{\rm Phys.\leavevmode\nobreak\
Rev.\leavevmode\nobreak\ E}_{V}(t)$.

Then each separator for $(V,s,t)$ contains a period $r\cdot\Delta$ for some
$r\in\mathbb{Q}$.

######  Proof 3.2.

Consider an arbitrary separator $S$ for $(V,s,t)$. Let $S_{q}=\\{v\mid q(v)\in
S,v\in\mathbb{N}^{d}\\}$ be its part devoted to the state $q$ and let
$S_{q}=\bigcup_{i\in I}L_{i}$, where $L_{i}$ are linear sets. As the line
$\alpha$ contains infinitely many points and $\alpha\subseteq S_{q}$ then some
of the linear sets $L_{i}$ have to contain infinitely many points of $\alpha$.
Denote this $L_{i}$ by $L$, let $L=b+\mathbb{N}p_{1}+\ldots+\mathbb{N}p_{k}$.
We know that for arbitrarily big $n$ we have
$a+n\Delta=b+n_{1}p_{1}+\ldots+n_{k}p_{k}$ for some $n_{i}\in\mathbb{N}$.
Wlog. we can assume that $n_{i}>0$, we just do not write the periods $p_{i}$
with coefficient $n_{i}=0$. Notice first that for each coordinate $j\in[3,d]$
we have $(a+n\Delta)[j]\leq\textup{norm}(a)$. Therefore for $p_{i}$ such that
$p_{i}[j]>0$ for some $j\in[3,d]$ we have $n_{i}\leq\textup{norm}(a)$. Let
$P_{0}$ be the set of periods $p_{i}$ such that $p_{i}[j]=0$ for all
$j\in[3,d]$ and $P_{\neq 0}$ be the set of the other periods $p_{i}$. We thus
have

$(a-b-\sum_{p_{i}\in P_{\neq 0}}n_{i}p_{i})+n\Delta=\sum_{p_{i}\in
P_{0}}n_{i}p_{i},$

where the sum $v=(a-b-\sum_{p_{i}\in P_{\neq 0}}n_{i}p_{i})$ has a norm
bounded by
$B=\textup{norm}(a)+\textup{norm}(b)+k\cdot\textup{norm}(a)\cdot\max_{p_{i}\in
P_{\neq 0}}\textup{norm}(p_{i})$, which is independent of $n$. If we restrict
the equation to the first two coordinates of the considered vectors we have

$(v[1],v[2])+n(\Delta[1],\Delta[2])=\sum_{p_{i}\in
P_{0}}n_{i}(p_{i}[1],p_{i}[2]).$ (1)

We aim at showing that one of $p_{i}$ is equal to $r\cdot\Delta$ for some
$r\in\mathbb{Q}$. Recall that for each $j\in[3,d]$ we have
$\Delta[j]=p_{i}[j]=0$, so it is enough to show that
$(p_{i}[1],p_{i}[2])=r\cdot(\Delta[1],\Delta[2])$.

We first show the following claim.

######  Claim 3.

For each period $p\in P_{0}$ we have $\Delta[1]\cdot p[2]\leq\Delta[2]\cdot
p[1]$.

######  Proof 3.3.

The intuitive meaning of $\Delta[1]\cdot p[2]\leq\Delta[2]\cdot p[1]$ is that
$\frac{\Delta[1]}{\Delta[2]}\leq\frac{p[1]}{p[2]}$, however we cannot write
the fraction $\frac{p[1]}{p[2]}$ as it might happen that $p[2]=0$. Assume
towards a contradiction that for some $p\in P_{0}$ we have $\Delta[1]\cdot
p[2]>\Delta[2]\cdot p[1]$. Let $\delta=\Delta[1]\cdot p[2]-\Delta[2]\cdot
p[1]>0$. Recall that $a+n\Delta\in L$ for some $n\in\mathbb{N}$, therefore
also $a+n\Delta+\Delta[1]\cdot p\in L$ as $p\in P_{0}$ is a period of $L$.
Then however

$\displaystyle\Delta[1]\cdot p$
$\displaystyle=\Delta[1]\cdot(p[1],p[2],0^{d-2})=(\Delta[1]\cdot
p[1],\Delta[1]\cdot p[2],0^{d-2})$ $\displaystyle=(\Delta[1]\cdot
p[1],\Delta[2]\cdot p[1]+\delta,0^{d-2})=p[1]\cdot\Delta+\delta\cdot
e_{2}\in\mathbb{N}\Delta+\mathbb{N}_{+}e_{2}.$

Therefore $a+n\Delta+\Delta[1]\cdot p\in
b+\mathbb{N}\Delta+\mathbb{N}_{+}e_{2}$ and it means that
$q(a+n\Delta+\Delta[1]\cdot p)\in{\rm Phys.\leavevmode\nobreak\
Rev.\leavevmode\nobreak\ E}_{V}(t)$. However we know that
$q(a+n\Delta+\Delta[1]\cdot p)\in q(S_{q})\subseteq S$ and therefore separator
$S$ nonempty intersects the set ${\rm Phys.\leavevmode\nobreak\
Rev.\leavevmode\nobreak\ E}_{V}(t)$. This is a contradiction with the
definition of separator.

In order to show that $p=r\cdot\Delta$ for some $p\in P_{0}$ it is sufficient
to show that $\Delta[1]\cdot p[2]=\Delta[2]\cdot p[1]$. Assume towards a
contradiction that for all $p\in P_{0}$ we have $\Delta[1]\cdot
p[2]\neq\Delta[2]\cdot p[1]$. By Claim 3 we know that actually for all $p\in
P_{0}$ we have that $\Delta[1]\cdot p[2]<\Delta[2]\cdot p[1]$. Thus $p[1]>0$
and we can equivalently write that for all $p\in P_{0}$ we have that
$\frac{\Delta[2]}{\Delta[1]}>\frac{p[2]}{p[1]}$. Let $F$ be the maximal value
of $\frac{p[2]}{p[1]}$ for $p\in P_{0}$, clearly
$\frac{\Delta[2]}{\Delta[1]}>F$, so

$\Delta[2]>F\cdot\Delta[1].$ (2)

By (1) we know that

$\frac{(v+n\Delta)[2]}{(v+n\Delta)[1]}\leq F,$

as $v+n\Delta$ is a positive linear combination of vectors $p\in P_{0}$ and
for each $p\in P_{0}$ we have $\frac{p[2]}{p[1]}\leq F$. Therefore it holds

$v[2]+n\Delta[2]\leq F(v[1]+n\Delta[1])$

and equivalently

$n(\Delta[2]-F\Delta[1])\leq Fv[1]-v[2].$

By (2) we have that $\Delta[2]-F\Delta[1]>0$ therefore

$n\leq\frac{Fv[1]-v[2]}{\Delta[2]-F\Delta[1]}.$

This is in contradiction with the assumption that $n$ can be arbitrarily big
and finishes the proof.

######  Remark 3.4.

In Theorem 3.1 instead of separator for $(V,s,t)$ one can consider a separator
for $(V^{\prime},s,t)$, where $V^{\prime}$ is obtained from $V$ by adding a
loop in state $q$ with the effect of decreasing the second counter. Indeed, it
is easy to observe that all the points 1-4 in the theorem statement remain
true after substitution of $V$ by $V^{\prime}$. Such a version of Theorem 3.1
is a bit more convenient for some of the applications.

##  4 Applications

In this section we show how Theorem 3.1 can be used to obtain lower bounds on
the separator size. In Section 4.1 we prove that using a construction from [5]
one can obtain a $4$-VASS with separators of at least doubly-exponential size.
In Section 4.2 we show that there exist VASSes with separators of arbitrary
high elementary size of a special shape. Existence of separators of arbitrary
high elementary size is an easy consequence of Tower-hardness of VASS
reachability problem, we provide in Theorem 4.3 a concrete instance of such a
separator. It is not a big contribution, but the aim of proving Theorem 4.3 is
rather to illustrate that our techniques can be quite easily applied to many
existing VASS examples.

###  4.1 Doubly-exponential separator in a $4$-VASS

The aim of this section is to show the following theorem.

######  Theorem 4.1.

There exists a family of binary $4$-VASSes $(V_{n})_{n\in\mathbb{N}}$ of size
$\mathcal{O}(n^{3})$ such that for some configurations $s_{n},t_{n}$ of
$V_{n}$ with $\textup{norm}(s_{n}),\textup{norm}(t_{n})\leq 1$ such that
$s_{n}$ does not reach $t_{n}$ the smallest separator for
$(V_{n},s_{n},t_{n})$ is of doubly-exponential size wrt. $n$.

The rest of this section is devoted to the proof of Theorem 4.1. Our
construction is based on the construction of a family of binary $4$-VASSes
$(U_{n})_{n\in\mathbb{N}}$ with shortest run of doubly-exponential length,
which is described in Section 5 in [5]. The picture below illustrates VASS
$U_{n}$, it is taken from [5] and modified a bit. The proof follows a very
natural line and is not a big challenge. It boils down to performing a small
modification to $4$-VASSes from [5] in order to ensure conditions of Theorem
3.1 and then checking that indeed these conditions are satisfied. We sketch
here the idea behind the construction of the mentioned family of $4$-VASSes
only into such an extend that we can explain the proof of Theorem 4.1, for
details we refer to [5].

$\cdot$$\cdot$$p_{k}$$q_{k}$$p_{k-1}$$q_{k-1}$$\cdots$$\ p_{1}\ $$\ q_{1}\ $$\
p_{0}\
$$(1,1,0,0)$$(1,1,0,0)$$(0,0,0,2^{k})$$(0,-1,1,0)$$(0,a_{k},-b_{k},0)$$(0,0,0,-1)$$(0,0,0,2^{k-1})$$(0,-1,1,0)$$(0,a_{k-1},-b_{k-1},0)$$(0,0,0,-1)$$(0,0,0,2^{1})$$(0,-1,1,0)$$(0,a_{1},-b_{1},0)$$(0,0,0,-1)$$(-a,-b,0,0)$

The construction relies on the following lemma (Lemma 12 in [5]).

######  Lemma 4.2.

For each $n\geq 1$ there are $n$ rational numbers

$1<f_{1}<\ldots<f_{n}=1+\frac{1}{4^{n}}$

of description size bounded by $4^{n^{2}+n}$, such that the description size
of $f$ defined as

$f=(f_{n})^{2^{n}}\cdot\ldots\cdot(f_{2})^{2^{2}}\cdot(f_{1})^{2^{1}}$ (3)

is bounded by $4^{2(n^{2}+n)}$.

The VASSes $U_{n}$ are constructed as follows. Valuation of the four counters
$(x_{1},x_{2},x_{3},x_{4})$ in the distinguished _initial_ state is initially
$0^{4}$, the run is _accepting_ if it finishes in the distinguished _final_
state also with valuation $0^{4}$. Each run of $U_{n}$ consists of $n+2$
phases: the _initial phase_ , $n$ phases corresponding to fractions
$f_{n},f_{n-1},\ldots,f_{2},f_{1}$, respectively and the _final phase_. In
each run after the initial phase the counter valuation is equal to $(N,N,0,0)$
for some nondeterministically guessed value $N\in\mathbb{N}$. In every
accepting run the phase corresponding to the fraction $f_{i}$ results only in
multiplying the second counter $x_{2}$ by a value $f_{i}^{2^{i}}$. Therefore
in such an accepting run counter valuation after phases corresponding to
fractions $f_{n},\ldots,f_{i}$ is the following

$(x_{1},x_{2},x_{3},x_{4})=(N,N\cdot f_{n}^{2^{n}}\cdot\ldots\cdot
f_{i}^{2^{i}},0,0).$

In particular after all the $n$ phases corresponding to fractions the second
counter is equal to

$N\cdot f_{n}^{2^{n}}\cdot\ldots\cdot f_{1}^{2^{1}}=N\cdot f,$

where the equality follows from Lemma 4.2. Let $p_{i}$ be the state of $U_{n}$
after the initial phase, $n-i$ phases corresponding to fractions
$f_{n},\ldots,f_{i+1}$ and just before the phase corresponding to fraction
$f_{i}$ (in the case when $i>0$). It is important that due to Claim 15 in [5]
any reachable configuration of the form $p_{i}(x_{1},x_{2},x_{3},x_{4})$
satisfies $x_{2}\leq f_{n}^{2^{n}}\cdot\ldots\cdot f_{i}^{2^{i}}\cdot x_{1}$.
In particular for any reachable configuration $p_{0}(x_{1},x_{2},x_{3},x_{4})$
we have that $x_{2}\leq f\cdot x_{1}$, as $f=f_{n}^{2^{n}}\cdot\ldots\cdot
f_{1}^{2^{1}}$. Let $f=\frac{a}{b}$. In the final phase the transition with
the effect $(-b,-a,0,0)$ is applied in a loop. One can easily see that in
order to reach counter values $0^{4}$ after the final phase we need to have in
the state $p_{0}$ values satisfying the equality $x_{2}=f\cdot x_{1}$.
Similarly any configuration $q_{n-1}(x_{1},x_{2},x_{3},x_{4})$ on an accepting
run needs to satisfy $x_{2}=f_{n}^{2^{n}}\cdot x_{1}$. Let
$f_{i}=\frac{a_{i}}{b_{i}}$ for all $i\in[1,n]$. Then in any accepting run
$x_{1}$ needs to be divisible by $b_{n}^{2^{n}}$, which is a doubly-
exponential number wrt. $n$. This forces any accepting run of $U_{n}$ to be
doubly-exponential.

We slightly modify $4$-VASSes $U_{n}$ in order to obtain $4$-VASSes $V_{n}$,
which fulfil conditions of Theorem 3.1. VASS $V_{n}$ is obtained from $U_{n}$
by adding at the end of $U_{n}$ two instructions: 1) decrease of $x_{2}$ by
$1$; and then 2) a loop, which decreases $x_{2}$ by an arbitrary nonnegative
number. We first show that $V_{n}$ indeed satisfies conditions of Theorem 3.1
and then we argue how this finishes the proof of Theorem 4.1. Let
$q_{\textup{in}}$ be the initial state of VASS $U_{n}$, $q_{\textup{out}}$ be
its final state and $q_{\textup{last}}$ be the state after the final phase,
but before applying the above mentioned decrements of $x_{2}$. We set
$s_{n}=q_{\textup{in}}(0^{4})$ and $t_{n}=q_{\textup{out}}(0^{4})$. Let
$N=\prod_{i=1}^{n}b_{i}^{2^{i}}$. We set $\Delta=(N,N\cdot
f_{n}^{2^{n}},0,0)\in\mathbb{N}^{4}$ and fix state $q=q_{n-1}$. We claim that
VASS $V_{n}$ together with two configurations $s_{n}$ and $t_{n}$, state $q$
and vector $\Delta$ satisfies conditions of Theorem 3.1.

Condition (1) is satisfied trivially as $\Delta=(N,N\cdot f_{n}^{2^{n}},0,0)$.
In order to see that (2) is satisfied recall that if $V_{n}$ reaches
$q_{0}(x_{1},x_{2},x_{3},x_{4})$ then we have that
$x_{2}\leq\frac{a}{b}x_{1}$. In the final phase we subtract in the loop vector
$(b,a,0,0)$, but it does not change this inequality. Finally subtracting at
least $1$ at $x_{2}$ implies that any reachable configuration
$q_{\textup{out}}(x_{1},x_{2},x_{3},x_{4})$ satisfies
$x_{2}+1\leq\frac{a}{b}\cdot x_{1}$. This is not true for $x_{1}=x_{2}=0$,
which shows that condition (2) is indeed satisfied. Observe now that for each
$k\in\mathbb{N}$ configuration $p_{n}(kN,kN,0,0)$ after the initial phase is
reachable from $s_{n}$. Thus also configuration $p_{n-1}(kN,kN\cdot
f_{n}^{2^{n}},0,0)$ is reachable from $s_{n}$ if we multiply the second
counter by $f_{n}^{2^{n}}$, which proves condition (3). Observe also that
starting in a configuration $p_{n-1}(kN,kN\cdot f_{n}^{2^{n}},0,0)$ one can
reach valuation $q_{\textup{last}}(0^{4})$ before the decrements of $x_{2}$.
Therefore after adding $e_{2}=(0,1,0,0)$ to both sides we get that
$p_{n-1}(kN,kN\cdot f_{n}^{2^{n}}+1,0,0)\longrightarrow
q_{\textup{last}}(0,1,0,0)\longrightarrow t_{n}$ for any $k\in\mathbb{N}$.
Because of an option of decreasing $x_{2}$ many times in $q_{\textup{last}}$
we get that $p_{n-1}(kN,kN\cdot f_{n}^{2^{n}}+\ell,0,0)\longrightarrow t_{n}$
for any $k,\ell\geq 1$, which equivalent to the condition (4).

Therefore by Theorem 3.1 we have that each separator for $(V_{n},s_{n},t_{n})$
contains a period $\Delta\cdot r\in\mathbb{N}^{4}$ for some $r\in\mathbb{Q}$.
Let $\Delta\cdot r=(x_{1},x_{2},0,0)\in\mathbb{N}^{4}$. We know that
$x_{2}=x_{1}\cdot\Big{(}\frac{a_{n}}{b_{n}}\Big{)}^{2^{n}}$, so in order for
$x_{2}\in\mathbb{N}$ we need to have $b_{n}^{2^{n}}\mid x_{1}$. This implies
that $x_{1}$ is doubly-exponential with respect to $n$. Therefore size of the
period $\Delta\cdot r$ and thus size of the separator is doubly-exponential
with respect to $n$.

###  4.2 Tower size separators

In this section we show the following result.

######  Theorem 4.3.

There exists a family of VASSes $(V_{n})_{n\in\mathbb{N}}$ of size polynomial
wrt. $n$ such that for some configurations $s_{n},t_{n}$ of $V_{n}$ with
$\textup{norm}(s_{n})=\textup{norm}(t_{n})=0$ the following is true:

  * •

$s_{n}\longrightarrow t_{n}$, but the shortest run is $n$-fold exponential,

  * •

$s_{n}\centernot\longrightarrow t_{n}+e$ for some elementary vector $e$ and
each separator for $(V_{n},s_{n},t_{n}+e)$ is of at least $n$-fold exponential
size.

The rest of this section is dedicated to prove Theorem 4.3. Construction of
VASSes $V_{n}$ is based on constructions in [4], but we do not follow exactly
[4] in order to avoid some technicalities and simplify the construction. As
the construction [4] is pretty involved we decided only to sketch the
intuition behind the constructed VASSes and use many of its properties without
a detailed explanation. The main goal of this section is to provide an
intuition why Theorem 3.1 is indeed applicable to that case, for details of
the construction we refer to the original paper [4]. Essentially speaking
Theorem 3.1 is applicable to VASSes in which the configurations on the
accepting run are distinguished from the others by keeping some specific ratio
of counter values. The bigger the description size of the ratio the bigger the
separator. In VASSes from [4] the description size is $n$-fold exponential,
which implies the lower bound on the size of separators.

We say that a counter is $B$-bounded if its value is upper bounded by $B$
along the whole run. In [4] counters are assured to be $B$-bounded (for
various values of $B$) in the following way. In order to guarantee that
counter $x$ initially equal to $0$ is $B$-bounded we introduce another counter
$\bar{x}$ which is initialised to $B$ and an invariant $a+\bar{a}=B$ is kept
throughout the whole run. The construction of [4] strongly relies on the fact
that having a triple $(x,y,z)=(B,C,BC)$ one can simulate $C/2$ zero-tests for
a $B$-bounded counter. One zero-test for counter $a$ is realised as follows.
We decrease $y$ by $2$. Then we enter two loops, the first one with the effect
$(-1,1,-1)$ on counters $(a,\bar{a},z)$ and the second one with the effect
$(1,-1,-1)$ on the same counters. It is easy to see that for a $B$-bounded
counter $a$ the maximal possible decrease on $z$ after these two loops is
equal to $2B$ and it can only be realised if before and after the loops we
have $(a,\bar{a})=(0,B)$.

Let $3!^{n}$ be the number $3$ followed by $n$ applications of the factorial
function. For example $3!^{0}=3$, $3!^{1}=6$ and $3!^{2}=720$. Roughly
speaking VASS in [4] consists of a sequence of $n$ gadgets, such that in every
accepting run they compute triples of the form $(3!^{i},k_{i},3!^{i}\cdot
k_{i})$ for some nondeterministically guessed values $k_{i}\in\mathbb{N}$. The
first gadget $\mathcal{B}$ computes triple $(3,k_{1},3\cdot k_{1})$ in a very
easy way: after increasing its counters by $(3,0,0)$ it fires a
nondeterministically guessed number $k_{1}$ of times a loop with the effect
equal to $(0,1,3)$. Next we have a sequence of $n-1$ gadgets $\mathcal{F}$,
the $i$-th one inputing a triple $(3!^{i},k_{i},3!^{i}\cdot k_{i})$ and
outputting a triple $(3!^{i+1},k_{i+1},3!^{i+1}\cdot k_{i+1})$ on some other
set of three counters. It is important to mention that correct value of the
output triple requires that after the run values of the input triple are all
zero. The last triple $(3!^{n},k_{n},3!^{i}\cdot k_{n})$ is used in [4] to
simulate $3!^{n}$-bounded counters of a counter automaton. Here however we
modify this construction in order to obtain VASSes $V_{n}$, which fulfil the
conditions of Theorem 4.3. As all the triples use different counters the
presented VASS has at least dimension $3n$. In the original construction of
[4] some of the counters were actually reused in order to decrease the
dimension. Here we allow for a wasteful use of counters, this however do not
change the idea of the construction.

The family of VASSes $V_{n}$ is defined as follows. We distinguish an initial
state $q_{\textup{in}}$ of $V_{n}$ and a final state $q_{\textup{out}}$ of
$V_{n}$. For $i\in[1,n]$ let $q_{i}$ be the state after the $i$-th gadget.
From the above description we get that in state $q_{i}$ valuation of some
three counters is equal to $(3!^{i},k_{i},3!^{i}\cdot k_{i})$. Let us denote
these counters $(x_{i},y_{i},z_{i})$. Thus in $q_{n}$ we reach counter values
$(x_{n},y_{n},z_{n})=(3!^{n},k_{n},3!^{n}\cdot k_{n})$ for some $k_{n}\geq 0$.
Then after state $q_{n}$ we define a state $q_{\textup{dec}}$ in which we
decrease values of $y_{n}$ and $z_{n}$ by applying some nonzero number of
zero-tests for $3!^{n}$-bounded counters. This operation can be seen as a loop
decreasing counters $(x_{n},y_{n},z_{n})$ by $(0,1,3!^{n})$, but of course
subtracting $(0,1,3!^{n})$ is not realised by a single transition, but by some
smaller sub-gadget of our VASS. Then we go to a state $q_{\textup{out}}$ in
which we can decrease in a loop the counter $x_{n}$ and as well the counter
$y_{n}$. We define $s_{n}=q_{\textup{in}}(0^{d})$ and
$t_{n}=q_{\textup{out}}(0^{d})$ for an appropriate dimension $d$. We set a
vector $e$ to be zero on all the coordinates beside $y_{n}$ on which it is set
to be one. We claim that $V_{n}$ with configurations $s_{n}$, $t_{n}$ and an
elementary vector $e$ satisfy the conditions of Theorem 4.3. It is easy to see
(assuming all the above remarks about the construction of [4]) that all the
accepting runs need to traverse through a configuration
$q_{n}(3!^{n},k,3!^{n}\cdot k)$ for some $k\geq 1$, which implies that all the
accepting runs have at least $n$-fold exponential length. It therefore remains
to show the second point of Theorem 4.3, we apply Theorem 3.1 for that
purpose.

As counters $x_{n}$, $y_{n}$ and $z_{n}$ are important let us assume wlog.
that they correspond to the first three coordinates in our notation,
respectively. Let $\Delta=(0,1,3!^{n},0^{d-3})\in\mathbb{N}^{d}$, namely
$\Delta[i]=0$ for all $i\not\in\\{y_{n},z_{n}\\}$, $\Delta[y_{n}]=1$ and
$\Delta[z_{n}]=3!^{n}$. Properties of $V_{n}$ can be summarised in the
following claim, which can be derived from [4].

######  Claim 4.

If $s_{n}\longrightarrow q_{\textup{dec}}(x,y,z,0^{d-3})$ then $x=3!^{n}$ and
$y\leq 3!^{n}z$. Moreover for any $y\in\mathbb{N}$ we have
$s_{n}\longrightarrow q_{\textup{dec}}(3!^{n},y,3!^{n}\cdot y,0^{d-3})$.

Now we aim at showing that VASS $V_{n}$ together with configurations $s_{n}$,
$t_{n}+e$, vector $\Delta$ and state $q_{\textup{dec}}$ fulfils conditions of
Theorem 3.1. It is immediate to see that condition (1) is satisfied as only
second and third coordinates in $\Delta$ are nonzero (we allow for reordering
the coordinates in Theorem 3.1 without loss of generality). In order to show
(2) we rely on Claim 4. We have $t_{n}+e=q_{\textup{out}}(0,1,0,0^{d-3})$,
thus if $s_{n}\longrightarrow t_{n}+e$ we need to have $s_{n}\longrightarrow
q_{\textup{dec}}(x,y,0,0^{d-3})\longrightarrow t_{n}+e$ for some $y>0$. This
is however a contradiction with Claim 4, as then $y\cdot 3!^{n}>0$. By Claim 4
we also immediately derive condition (3). To show condition (4) notice that
because of the loop in $q_{\textup{dec}}$ of effect $(0,-1,-3!^{n})$ on
counters $(x_{n},y_{n},z_{n})$ we have

$q_{\textup{dec}}(0,k+\ell,k\cdot 3!^{n},0^{d-3})\longrightarrow
q_{\textup{dec}}(0,\ell,0^{d-2})\longrightarrow
q_{\textup{out}}(0,\ell-1,0^{d-2})\longrightarrow
q_{\textup{out}}(0,1,0^{d-2})=t_{n}+e$

for any $k,\ell\geq 1$. This shows that indeed Theorem 3.1 can be applied to
$V_{n}$. Thus each separator for $(V_{n},s_{n},t_{n}+e)$ contains a period of
a form $(r,r\cdot 3!^{n},0,0^{d-3})\in\mathbb{N}$. As $r\in\mathbb{N}$ the
number $r\cdot 3!^{n}$ is $n$-fold exponential and thus the size of any
separator for $(V_{n},s_{n},t_{n}+e)$ is $n$-fold exponential, which finishes
the proof of Theorem 4.3.

##  5 Generalised theorem

Before we start introducing the notions needed for Theorem 5.2 we motivate the
need of a generalisation of Theorem 3.1. Formulation of Theorem 3.1 is rather
simple and it is sufficient for our applications, but it may seem a bit
arbitrary. As mentioned in the paragraph before Theorem 3.1 it is well suited
to the situation when the ratio $\frac{x}{y}$ between some two counters $x$
and $y$ is fixed and bounded at some specific moment at the run. We can
however very easily imagine that in some other, but very related VASS some a
bit more involved ratio is kept fixed. This can be a ratio of a form
$\frac{x_{1}+x_{2}}{y_{1}+y_{2}+y_{3}}$ or something similar. It looks very
natural that we may keep constant a ratio not between two counter values, but
between sums of a few counter values. This motivates introduction of the
linear functions defined below and use of them in Theorem 5.2. When we deal
with more than two counters we cannot easily speak about lines, which was
natural in Theorem 3.1. This is the reason why we are forced to use a more
abstract language in order to be prepared for the above mentioned simple
applications. Theorem 5.2 can be seen as a more powerful tool than Theorem
3.1. At the moment we do not see any applications in which Theorem 5.2 is
needed. However in our opinion it is important to show that the techniques
presented in Theorem 3.1 can be quite easily extended to stronger Theorem 5.2.

Before stating Theorem 5.2 we introduce a few notions.

##### Greatest common divisors

We state here a fact about greatest common divisors, which is helpful in the
sequel. By $\gcd(a_{1},\ldots,a_{k})$ we denote the greatest common divisor of
all the numbers $a_{1},\ldots,a_{k}$.

######  Claim 5.

For all natural numbers $a_{1},\ldots,a_{k}\leq M$ and for each $S\geq
k(M^{2}-M)$ which is divisible by $\gcd(a_{1},\ldots,a_{k})$ there exist
nonnegative coefficients $b_{1},\ldots,b_{k}\in\mathbb{N}$ such that
$S=a_{1}b_{1}+\ldots+a_{k}b_{k}$.

######  Proof 5.1.

The following fact is called Bezout’s identity and can be easily proved by
induction on $k$: for each $a_{1},\ldots,a_{k}\in\mathbb{N}$ there exist some
coefficients $b_{1},\ldots,b_{k}\in\mathbb{Z}$ such that
$\gcd(a_{1},\ldots,a_{k})=\sum_{i=1}^{k}a_{i}b_{i}$. Let us take such a
solution which minimises the sum $\sum_{i:b_{i}<0}|b_{i}|$. We show that in
this solution actually all the $b_{i}$ are nonnegative. Assume otherwise and
let $b_{i}<0$ for some $i\in[1,k]$. As $S\geq k(M^{2}-M)$ then for some
$b_{j}\in[1,k]$ we have $b_{j}\geq M$. Then substituting $b_{j}$ by
$b_{j}-a_{i}$ and $b_{i}$ by $b_{i}+a_{j}$ we obtain a solution with smaller
$\sum_{i:b_{i}<0}|b_{i}|$, contradiction.

##### Linear functions

Let a linear function $\textup{Lin}:\mathbb{N}^{d}\to\mathbb{N}$ be of a form
$\textup{Lin}(x_{1},\ldots,x_{d})=\sum_{i=1}^{d}n_{i}x_{i}$, with all the
coefficients $n_{i}\in\mathbb{N}_{+}$. We call a linear function _reduced_ if
$\gcd(n_{1},\ldots,n_{d})=1$, let us assume that Lin is reduced. Notice that
each linear function is a reduced linear function multiplied by some natural
number. Let $M=\max_{i\in[1,d]}n_{i}$. The _support_ of a linear function
$\textup{supp}(\textup{Lin})\subseteq[1,d]$ is the set of coordinates for
which coefficient $n_{i}$ is nonzero. Let the set of vectors
$\textsc{zero}(\textup{Lin})\subseteq\mathbb{Z}^{d}$ contain all the vectors
$n_{j}e_{i}-n_{i}e_{j}$ for $i,j\in\textup{supp}(\textup{Lin})$. Clearly for
any $v\in\textsc{zero}(\textup{Lin})$ and any $u\in\mathbb{N}^{d}$ such that
$u+v\in\mathbb{N}^{d}$ we have $\textup{Lin}(u+v)=\textup{Lin}(u)$. The
following claim tells that set $\textsc{zero}(\textup{Lin})$ in some way spans
the set of vectors with the same value of Lin in case it is big.

######  Claim 6.

For any $u,v\in\mathbb{N}^{d}$ such that $\textup{Lin}(u)=\textup{Lin}(v)\geq
d\cdot M^{3}$ there is a sequence of vectors
$u=x_{0},x_{1},\ldots,x_{k}=v\in\mathbb{N}^{d}$ such that for all $i\in[1,k]$
we have $x_{i}-x_{i-1}\in\textsc{zero}(\textup{Lin})$.

The proof of Claim 6 can be found in the appendix. It uses Claim 5 and a bit
of other rather simple number theory.

##### Modification of a VASS

For two linear functions
$\textup{Lin}_{1},\textup{Lin}_{2}\in\mathbb{N}^{d}\to\mathbb{N}$ with
disjoint supports and a VASS $V$ with state $q$ we define VASS
$V^{q}_{\textup{Lin}_{1},\textup{Lin}_{2}}$ as $V$ with additional transitions
whose aim is to be able to increase the ratio
$\frac{\textup{Lin}_{1}(\cdot)}{\textup{Lin}_{2}(\cdot)}$, but never decrease
it. Let $\textup{Lin}_{1}(x_{1},\ldots,x_{d})=\sum_{i=1}^{d}n_{i,1}x_{i}$ and
let $\textup{Lin}_{2}(x_{1},\ldots,x_{d})=\sum_{i=1}^{d}n_{i,2}x_{i}$. The set
of states of $V^{q}_{\textup{Lin}_{1},\textup{Lin}_{2}}$ is inherited from $V$
similarly to the set of transitions of $V$. We additionally add to $V$
transitions of the form $(q,v,q)$, which are loops in the state $q\in Q$, of
the following form:

  1. 1.

for each coordinate $i\in\textup{supp}(\textup{Lin}_{2})$ add a loop which
decreases coordinate $i$ by one

  2. 2.

for each coordinate
$i\not\in\textup{supp}(\textup{Lin}_{1})\,\cup\,\textup{supp}(\textup{Lin}_{2})$
add two loops: one, which increases and one which decreases coordinate $i$ by
one

  3. 3.

for each $v\in\textsc{zero}(\textup{Lin}_{1})$ which is nonzero only at
$\textup{supp}(\textup{Lin}_{1})$ and similarly for each
$v\in\textsc{zero}(\textup{Lin}_{2})$ which is nonzero only at
$\textup{supp}(\textup{Lin}_{2})$ add a loop with effect $v$.

Notice that condition 2 means that we can freely modify in
$V^{q}_{\textup{Lin}_{1},\textup{Lin}_{2}}$ the coordinates outside
$\textup{supp}(\textup{Lin}_{1})\,\cup\,\textup{supp}(\textup{Lin}_{2})$ We
are ready to state the theorem.

######  Theorem 5.2.

Let $\textup{Lin}_{1},\textup{Lin}_{2}:\mathbb{N}^{d}\to\mathbb{N}$ be two
reduced linear functions with disjoint supports. Let $V=(Q,T)$ be a $d$-VASS,
$q\in Q$ be its state, $s,t\in Q\times\mathbb{N}^{d}$ be two its
configurations and $R\in\mathbb{Q}$ be a rational number. Assume that

  1. (1)

for each $v\in\mathbb{N}^{d}$ if $s\longrightarrow q(v)$ then
$\textup{Lin}_{1}(v)\geq R\cdot\textup{Lin}_{2}(v)$,

  2. (2)

for each $u,v\in\mathbb{N}^{d}$ if $q(v)\longrightarrow t+u$ then
$\textup{Lin}_{1}(v-u)\leq R\cdot\textup{Lin}_{2}(v-u)$,

  3. (3)

each run from $\textup{state}(s)$ to $\textup{state}(t)$ traverses through a
configuration $c$ with $\textup{state}(c)=q$,

  4. (4)

the set $\\{\textup{proj}_{I}(v)\mid s\longrightarrow q(v)\longrightarrow
t\\}$ is infinite, where
$I=\textup{supp}(\textup{Lin}_{1})\cup\textup{supp}(\textup{Lin}_{2})$.

Then for any $i\in\textup{supp}(\textup{Lin}_{2})$ there is no run from $s$ to
$t+e_{i}$ in $V^{\prime}=V^{q}_{\textup{Lin}_{1},\textup{Lin}_{2}}$ and each
separator for $(V^{\prime},s,t+e_{i})$ contains a period $p$ such that
$\textup{proj}_{I}(p)\neq 0$ and
$\textup{Lin}_{1}(p)=R\cdot\textup{Lin}_{2}(p)$.

######  Proof 5.3.

Due to condition (4) in the theorem statement there exists an infinite
sequence of vectors $v_{i}\in\mathbb{N}^{d}$ with $\textup{proj}_{I}(v_{i})$
pairwise different such that $s\longrightarrow q(v_{i})\longrightarrow t$. Let
$\rho^{1}_{i}$ be the corresponding runs from $s$ to $q(v_{i})$ and
$\rho^{2}_{i}$ be the corresponding runs from $q(v_{i})$ to $t$. Recall that
$\unlhd$ is a well-quasi order and its modified version (denoted here
$\unlhd^{\prime}$) with comparison on sources instead of targets is also a
well-quasi order. Therefore there exist $i<j$ such that
$\rho^{1}_{i}\unlhd\rho^{1}_{j}$ and
$\rho^{2}_{i}\unlhd^{\prime}\rho^{2}_{j}$. Let
$\Delta=v_{j}-v_{i}\in\mathbb{N}^{d}$. Clearly $\textup{proj}_{I}(\Delta)\neq
0$, as $\textup{proj}_{I}(v_{i})\neq\textup{proj}_{I}(v_{j})$. Let $a=v_{i}$.
By Corollary 2.1 we get that for any $n\in\mathbb{N}$ there is a run of $V$
from $s$ to $a+n\Delta$. An analogous reasoning with targets changed to
sources shows that for any $n\in\mathbb{N}$ there is a run in $V$ from
$a+n\Delta$ to $t$. Therefore for any $n\in\mathbb{N}$ we have
$s\longrightarrow q(a+n\Delta)\longrightarrow t$. By conditions (1) and (2) in
the theorem statement we get that
$\textup{Lin}_{1}(a+n\Delta)=R\cdot\textup{Lin}_{2}(a+n\Delta)$ for any
$n\in\mathbb{N}$. In consequence
$\textup{Lin}_{1}(\Delta)=R\cdot\textup{Lin}_{2}(\Delta)$. Notice that both
$\textup{Lin}_{1}(\Delta),\textup{Lin}_{2}(\Delta)>0$, because
$\textup{proj}_{I}(\Delta)\neq 0$.

We first show that $s\centernot\longrightarrow t+e_{i}$ in $V^{\prime}$.
Assume towards a contradiction that $s\longrightarrow t+e_{i}$. By condition
(3) we know that $s\longrightarrow q(v)\longrightarrow t+e_{i}$ for some
$v\in\mathbb{N}^{d}$. Observe first that conditions (1) and (2) still hold for
the reachability relation defined in $V^{\prime}$, as the added loops in state
$q$ do not invalidate them (for that purpose we demand in point 3. in the
construction of $V^{\prime}$ that vector $v$ is nonzero only on coordinates in
$\textup{supp}(\textup{Lin}_{1})$ or only on coordinates in
$\textup{supp}(\textup{Lin}_{2})$). Notice that by condition (2) setting
$u=e_{i}$ we have

$\textup{Lin}_{1}(v)=\textup{Lin}_{1}(v-e_{i})\leq
R\cdot\textup{Lin}_{2}(v-e_{i})<R\cdot\textup{Lin}_{2}(v).$

where the first equation follows from the fact that
$\textup{Lin}_{1}(e_{i})=0$. On the other hand $s\longrightarrow q(v)$ so by
condition (1) we have $\textup{Lin}_{1}(v)\geq R\cdot\textup{Lin}_{2}(v)$,
which is in contradiction with the above inequality. Thus indeed
$s\centernot\longrightarrow t+e_{i}$.

Now we show that every separator for $(V^{\prime},s,t+e_{i})$ contains an
appropriate period $p$. This proof is quite similar to the proof of Theorem
3.1, but we need to deal with some more technicalities. Consider a separator
$S=\bigcup_{q\in Q}q(S_{q})$ for $(V^{\prime},s,t+e_{i})$. Clearly
$S_{q}=\bigcup_{j\in J}L_{j}$, where $L_{j}$ are linear sets, needs to contain
all the vectors $a+n\Delta$ for $n\in\mathbb{N}$. Let $L$ be one of the
finitely many linear sets $L_{j}$, which contains infinitely many vectors
among $\\{a+n\Delta\mid n\in\mathbb{N}\\}$. Let
$L=b+\mathbb{N}p_{1}+\ldots+\mathbb{N}p_{k}$ and $P$ be the set of periods
$\\{p_{1},\ldots,p_{k}\\}$. We aim at showing that $L$ contains a period $p$
such that $\textup{proj}_{I}(p)\neq 0$ and
$\textup{Lin}_{1}(p)=R\cdot\textup{Lin}_{2}(p)$, namely
$\textup{Lin}_{1}(p)\cdot\textup{Lin}_{2}(\Delta)=\textup{Lin}_{2}(p)\cdot\textup{Lin}_{1}(\Delta)$,
as $R=\frac{\textup{Lin}_{1}(\Delta)}{\textup{Lin}_{2}(\Delta)}$.

We first prove a claim analogous to Claim 3. This one is however much more
challenging to prove. For its purpose we have defined $V^{\prime}$ so
intricately with the additional loops.

######  Claim 7.

For each period $p\in P$ we have
$\textup{Lin}_{1}(\Delta)\cdot\textup{Lin}_{2}(p)\leq\textup{Lin}_{2}(\Delta)\cdot\textup{Lin}_{1}(p)$.

Claim 7 is proven in the appendix, it uses the nontrivial Claim 6.

Now we follow the lines of the proof of Claim 3. Let $P_{\emptyset}$ be the
set of all periods in $P$ for which $\textup{proj}_{I}(p)=\emptyset$ and
$P_{\neq\emptyset}=P\setminus P_{\emptyset}$. Recall that we want to show
existence of a period $p\in P_{\neq\emptyset}$ fulfilling
$\textup{Lin}_{1}(p)\cdot\textup{Lin}_{2}(\Delta)=\textup{Lin}_{2}(p)\cdot\textup{Lin}_{1}(\Delta)$.
Assume towards a contradiction that there is no such period. Therefore by
Claim 7 each period $p\in P_{\neq\emptyset}$ satisfies
$\textup{Lin}_{1}(\Delta)\cdot\textup{Lin}_{2}(p)<\textup{Lin}_{2}(\Delta)\cdot\textup{Lin}_{1}(p)$.
In particular for each period $p\in P_{\neq\emptyset}$ we have
$\textup{Lin}_{1}(p)>0$, thus we can equivalently write that for all $p\in
P_{\neq\emptyset}$ it holds

$\frac{\textup{Lin}_{2}(p)}{\textup{Lin}_{1}(p)}<\frac{\textup{Lin}_{2}(\Delta)}{\textup{Lin}_{1}(\Delta)}.$

Let $F$ be the maximal value of
$\frac{\textup{Lin}_{2}(p)}{\textup{Lin}_{1}(p)}$ for $p\in
P_{\neq\emptyset}$, clearly
$\frac{\textup{Lin}_{2}(\Delta)}{\textup{Lin}_{1}(\Delta)}>F$, so

$\textup{Lin}_{2}(\Delta)>F\cdot\textup{Lin}_{1}(\Delta).$ (4)

Recall now that for arbitrary big $n$ we have that $a+n\Delta\in
b+\mathbb{N}p_{1}+\ldots+\mathbb{N}p_{k}$, thus
$(a-b)+n\Delta\in\mathbb{N}p_{1}+\ldots+\mathbb{N}p_{k}$. Let $v=a-b$. We have
then that

$(\textup{Lin}_{1}(v+n\Delta),\textup{Lin}_{2}(v+n\Delta))=\sum_{p_{i}\in
P_{\neq\emptyset}}n_{i}(\textup{Lin}_{1}(p),\textup{Lin}_{2}(p)).$

By the above we know that

$\frac{\textup{Lin}_{2}(v+n\Delta)}{\textup{Lin}_{1}(v+n\Delta)}\leq F,$

as $v+n\Delta$ is a positive linear combination of periods from $P$, for each
$p\in P_{\emptyset}$ we have $\textup{Lin}_{1}(p)=\textup{Lin}_{2}(p)=0$ and
for each $p\in P_{\neq\emptyset}$ we have
$\frac{\textup{Lin}_{2}(p)}{\textup{Lin}_{1}(p)}\leq F$. Therefore

$\textup{Lin}_{2}(v)+n\textup{Lin}_{2}(\Delta)\leq
F(\textup{Lin}_{1}(v)+n\textup{Lin}_{1}(\Delta))$

and equivalently

$n(\textup{Lin}_{2}(\Delta)-F\cdot\textup{Lin}_{1}(\Delta))\leq
F\cdot\textup{Lin}_{1}(v)-\textup{Lin}_{2}(v).$

By (4) we have that
$\textup{Lin}_{2}(\Delta)-F\cdot\textup{Lin}_{1}(\Delta)>0$ therefore

$n\leq\frac{F\cdot\textup{Lin}_{1}(v)-\textup{Lin}_{2}(v)}{\textup{Lin}_{2}(\Delta)-F\cdot\textup{Lin}_{1}(\Delta)}.$

This is in contradiction with the fact that $n$ can be arbitrarily big and
finishes the proof.

#### Acknowledgements

We thank Sławomir Lasota and Michał Pilipczuk for inspiring discussions.

## References

  * [1] Michael Blondin, Alain Finkel, Stefan Göller, Christoph Haase, and Pierre McKenzie.  Reachability in Two-Dimensional Vector Addition Systems with States Is PSPACE-Complete.  In Proceedings of LICS 2015, pages 32–43, 2015.
  * [2] Lorenzo Clemente, Wojciech Czerwinski, Slawomir Lasota, and Charles Paperman.  Separability of Reachability Sets of Vector Addition Systems.  CoRR, 2016.
  * [3] Lorenzo Clemente, Wojciech Czerwinski, Slawomir Lasota, and Charles Paperman.  Separability of Reachability Sets of Vector Addition Systems.  In Proceedings of STACS 2017, pages 24:1–24:14, 2017.
  * [4] Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, and Filip Mazowiecki.  The reachability problem for Petri nets is not elementary.  In Proceedings of STOC 2019, pages 24–33, 2019.
  * [5] Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, and Filip Mazowiecki.  Reachability in fixed dimension vector addition systems with states.  In Proceedings of CONCUR 2020, pages 48:1–48:21, 2020.
  * [6] Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, and Filip Mazowiecki.  The Reachability Problem for Petri Nets Is Not Elementary.  J. ACM, 68(1):7:1–7:28, 2021.
  * [7] Wojciech Czerwiński and Łukasz Orlikowski.  Reachability in Vector Addition Systems is Ackermann-complete.  In Proceedings of FOCS 2021, pages 1229–1240. IEEE, 2021.
  * [8] Wojciech Czerwiński and Łukasz Orlikowski.  Lower Bounds for the Reachability Problem in Fixed Dimensional VASSes.  CoRR, abs/2203.04243, 2022.
  * [9] Matthias Englert, Ranko Lazic, and Patrick Totzke.  Reachability in Two-Dimensional Unary Vector Addition Systems with States is NL-Complete.  In Proceedings of LICS ’16, pages 477–484, 2016.
  * [10] Petr Jancar.  Decidability of a Temporal Logic Problem for Petri Nets.  Theor. Comput. Sci., 74(1):71–93, 1990.
  * [11] S. Rao Kosaraju.  Decidability of Reachability in Vector Addition Systems (Preliminary Version).  In Proceedings of STOC ’82, pages 267–281, 1982.
  * [12] Jean-Luc Lambert.  A Structure to Decide Reachability in Petri Nets.  Theor. Comput. Sci., 99(1):79–104, 1992.
  * [13] Jérôme Leroux.  The General Vector Addition System Reachability Problem by Presburger Inductive Invariants.  In Proceedings of LICS ’09, pages 4–13, 2009.
  * [14] Jérôme Leroux.  The Reachability Problem for Petri Nets is Not Primitive Recursive.  In Proceedings of FOCS 2021, pages 1241–1252. IEEE, 2021.
  * [15] Jérôme Leroux and Sylvain Schmitz.  Demystifying Reachability in Vector Addition Systems.  In Proceedings of LICS 2015, pages 56–67, 2015.
  * [16] Jérôme Leroux and Sylvain Schmitz.  Reachability in Vector Addition Systems is Primitive-Recursive in Fixed Dimension.  In Proceedings of LICS 2019, pages 1–13, 2019.
  * [17] Richard J. Lipton.  The Reachability Problem Requires Exponential Space.  Technical report, Yale University, 1976.
  * [18] Ernst W. Mayr.  An Algorithm for the General Petri Net Reachability Problem.  In Proceedings of STOC’81, pages 238–246, 1981.
  * [19] Charles Rackoff.  The Covering and Boundedness Problems for Vector Addition Systems.  Theor. Comput. Sci., 6:223–231, 1978.
  * [20] Sylvain Schmitz.  Complexity Hierarchies beyond Elementary.  ACM Trans. Comput. Theory, 8(1):3:1–3:36, 2016.

##  Appendix A Missing proof

######  Proof A.1 (Proof of Claim 6).

We prove the claim by induction on $d$. For $d=1$ clearly $u=v$ and there is
nothing to show. Let us assume that the claim holds for $d-1$, our aim is to
prove it for $d$. Adding a vector $y\in\textsc{zero}(\textup{Lin})$ to
$x_{i-1}$ in order to obtain $x_{i}=x_{i-1}+y\in\mathbb{N}^{d}$ we call a
_step_. Clearly it is enough find a sequence of steps from $u$ to $v$. The
plan is to apply first such a sequence of steps from $u$ to some $u^{\prime}$
such that $u^{\prime}[i]=v[i]$ for some $i\in[1,d]$ and then show by induction
assumption that a sequence of steps from $u^{\prime}$ to $v$ exists as well.

For a subset of coordinates $I\subseteq[1,d]$ and $x\in\mathbb{N}^{d}$ by
$\textup{Lin}_{I}(x)$ we denote $\sum_{i\in I}n_{i}x[i]$. As
$\textup{Lin}(v)\geq d\cdot M^{3}$ there exists some $j\in[1,d]$ such that
$\textup{Lin}_{[1,d]\setminus\\{j\\}}(v)\geq(d-1)M^{3}$. Assume wlog. that
$j=d$, so

$\textup{Lin}_{[1,d-1]}(v)\geq(d-1)M^{3}.$ (5)

We first aim to reach $u^{\prime\prime}$ such that
$u^{\prime\prime}[d]-v[d]\geq M^{2}$. Clearly until for some $i\neq d$ we have
$u[i]\geq M$ we can apply the step $n_{i}e_{d}-n_{d}e_{i}$ to $u$ and increase
value of $u[d]$. We continue this until we reach some $u^{\prime\prime}$ with
$\sum_{i=1}^{d-1}u^{\prime\prime}[i]<(d-1)M$. This is indeed possible as
$\sum_{i=1}^{d-1}u^{\prime\prime}[i]\geq(d-1)M$ implies that for some $i\neq
d$ we have $u^{\prime\prime}[i]\geq M$. Then we have that
$\textup{Lin}_{[1,d-1]}(u^{\prime\prime})<(d-1)M^{2}$ as
$M=\max_{i\in[1,d]}n_{i}$, so $n_{d}\cdot
u^{\prime\prime}[d]>dM^{3}-(d-1)M^{2}$. By (5) we have $n_{d}\cdot v[d]\leq
dM^{3}-(d-1)M^{3}=M^{3}$. Therefore
$n_{d}(u^{\prime\prime}[d]-v[d])>(d-1)(M^{3}-M^{2})$ and thus
$u^{\prime\prime}[d]-v[d]\geq(d-1)(M^{2}-M)$. By Claim 5 we have that
$u^{\prime\prime}[d]-v[d]=\sum_{i=1}^{d-1}n_{i}b_{i}$ for some
$b_{i}\in\mathbb{N}$ (notice that here we use the fact that Lin is reduced and
therefore $\gcd(n_{1},\ldots,n_{d-1})=1$ and divides
$u^{\prime\prime}[d]-v[d]$). Therefore in order to obtain $u^{\prime}$ such
that $u^{\prime}[d]=v[d]$ we apply for each $i\in[1,d-1]$ exactly $b_{i}$
number of times the step $n_{d}e_{i}-n_{i}e_{d}$ to $u^{\prime\prime}$. Notice
that all the other coordinates beside the $d$-th one increase, so these steps
lead to vectors with nonnegative coordinates. As
$\textup{Lin}_{i\in[1,d-1]}(u^{\prime})=\textup{Lin}_{i\in[1,d-1]}(v)\geq(d-1)M^{3}$
we apply the induction assumption to show that indeed starting from
$u^{\prime}$ one can reach $v$ by a sequence of steps. This finishes the
proof.

######  Proof A.2 (Proof of Claim 7).

Similarly as in Claim 3 we intuitively mean to show that for all $p\in P$ we
have
$\frac{\textup{Lin}_{1}(\Delta)}{\textup{Lin}_{2}(\Delta)}\leq\frac{\textup{Lin}_{1}(p)}{\textup{Lin}_{2}(p)}$,
but this is not a formally correct statement as it may be that
$\textup{Lin}_{2}(p)=0$. Assume towards a contradiction that there is a period
$p$ such that
$\textup{Lin}_{1}(\Delta)\cdot\textup{Lin}_{2}(p)>\textup{Lin}_{2}(\Delta)\cdot\textup{Lin}_{1}(p)$.
Clearly $a\in L$, therefore also $a+mp\in L$ for any $m\in\mathbb{N}$. We aim
at showing that $a+mp\longrightarrow a+n\Delta+e_{i}$ in $V^{\prime}$ for some
$m,n\in\mathbb{N}$. This would lead to a contradiction as we know that
$a+n\Delta\longrightarrow t$, so also $a+n\Delta+e_{i}\longrightarrow
t+e_{i}$. Therefore we would have that $a+mp\in L$ and also
$a+mp\longrightarrow a+n\Delta+e_{i}\longrightarrow t+e_{i}$, which is a
contradiction with the definition of the separator.

Let $\textup{Lin}_{2}(x_{1},\ldots,x_{d})=\sum_{i=1}^{d}n_{i,2}x_{i}$ and let
$M$ be the maximal coefficient in $\textup{Lin}_{2}$, namely
$M=\max_{i\in[1,d]}n_{i,2}$. We set $m=dM^{3}\cdot\textup{Lin}_{1}(\Delta)$
and $n=dM^{3}\cdot\textup{Lin}_{1}(p)$. Observe now that
$\textup{Lin}_{1}(a+mp)=\textup{Lin}_{1}(a+n\Delta+e_{i})$. Indeed

$\displaystyle\textup{Lin}_{1}(a+mp)$
$\displaystyle=\textup{Lin}_{1}(v)+m\cdot\textup{Lin}_{1}(p)=\textup{Lin}_{1}(v)+dM^{3}\cdot\textup{Lin}_{1}(\Delta)\cdot\textup{Lin}_{1}(p)$
$\displaystyle=\textup{Lin}_{1}(v)+n\cdot\textup{Lin}_{1}(\Delta)=\textup{Lin}_{1}(a+n\Delta+e_{i}),$

as $i\not\in\textup{supp}(\textup{Lin}_{1})$, so $\textup{Lin}_{1}(e_{i})=0$.
Let $p=p_{1}+p_{2}+p_{\textup{trash}}$ and
$\Delta=\Delta_{1}+\Delta_{2}+\Delta_{\textup{trash}}$, where
$p_{1},\Delta_{1}$ are positive only on $\textup{supp}(\textup{Lin}_{1})$,
$p_{2},\Delta_{2}$ are positive only on $\textup{supp}(\textup{Lin}_{2})$ and
$p_{\textup{trash}},\Delta_{\textup{trash}}$ are positive only outside
$\textup{supp}(\textup{Lin}_{1})\,\cup\,\textup{supp}(\textup{Lin}_{2})$.
First notice that thanks to transitions in $V^{\prime}$, which can freely
modify coordinates outside
$\textup{supp}(\textup{Lin}_{1})\,\cup\,\textup{supp}(\textup{Lin}_{2})$ we
can assume wlog. that $p_{\textup{trash}}=\Delta_{\textup{trash}}=0$.
Therefore by Claim 6 and because $\textup{Lin}_{1}$ is reduced there is a run
in $V^{\prime}$ from $a+mp=a+mp_{1}+mp_{2}$ to $a+n\Delta_{1}+mp_{2}$, as
$\textup{Lin}_{1}(a+mp_{1})=\textup{Lin}_{1}(a+n\Delta_{1})\geq
dM^{3}\geq|\textup{supp}(\textup{Lin}_{1})|\cdot M^{3}$. We claim now that

$\textup{Lin}_{2}(mp_{2})=\textup{Lin}_{2}(n\Delta_{2}+e_{i}+v_{\textup{trash}})\geq
dM^{3}\geq|\textup{supp}(\textup{Lin}_{2})|\cdot M^{3}$ (6)

for some $v_{\textup{trash}}$ positive only on
$\textup{supp}(\textup{Lin}_{2})$. This would finalise the argument as then

$a+n\Delta_{1}+mp_{2}\longrightarrow
a+n\Delta_{1}+n\Delta_{2}+e_{i}+v_{\textup{trash}}\longrightarrow
a+n\Delta_{1}+n\Delta_{2}+e_{i}=a+n\Delta+e_{i},$

where the first relation $\longrightarrow$ follows from Claim 6 and fact that
$\textup{Lin}_{2}$ is reduced and the second one follows from existence of
transitions in $V^{\prime}$ which arbitrarily decrease any coordinate in
$\textup{supp}(\textup{Lin}_{2})$.

Recall first that
$\textup{Lin}_{1}(\Delta)\cdot\textup{Lin}_{2}(p)>\textup{Lin}_{2}(\Delta)\cdot\textup{Lin}_{1}(p)$,
so

$\textup{Lin}_{1}(\Delta)\cdot\textup{Lin}_{2}(p)-\textup{Lin}_{2}(\Delta)\cdot\textup{Lin}_{1}(p)\geq
1$

and that we set $m=dM^{3}\cdot\textup{Lin}_{1}(\Delta)$ and
$n=dM^{3}\cdot\textup{Lin}_{1}(p)$. Therefore

$\textup{Lin}_{2}(mp_{2})-\textup{Lin}_{2}(n\Delta_{2})=dM^{3}\cdot\textup{Lin}_{1}(\Delta)\cdot\textup{Lin}_{2}(p)-dM^{3}\cdot\textup{Lin}_{2}(\Delta)\cdot\textup{Lin}_{1}(p)\geq
dM^{3}.$

So $\textup{Lin}_{2}(mp_{2})-\textup{Lin}_{2}(n\Delta_{2}+e_{i})\geq
dM^{3}-M\geq d(M^{2}-M)$. Thus by Claim 5 there exist some
$b_{1},\ldots,b_{d}\in\mathbb{N}$ such that
$\sum_{j=1}^{d}n_{j,2}b_{j}=\textup{Lin}_{2}(mp_{2})-\textup{Lin}_{2}(n\Delta_{2}+e_{i})$.
Hence
$\textup{Lin}_{2}(mp_{2})=\textup{Lin}_{2}(n\Delta_{2}+e_{i}+\sum_{j=1}^{n}b_{j}e_{j})\geq
dM^{3}$ and we can set $v_{\textup{trash}}=\sum_{j=1}^{n}b_{j}e_{j}$ thus
satisfying (6) and finishing the proof of the claim.