New Pumping Technique for 2-dimensional VASS

TL;DR

This paper introduces a novel geometric pumping technique for 2-dimensional VASS, enabling new bounds and lemmas that could impact decidability and language analysis.

Contribution

It presents a new geometric pumping method for 2-VASS, providing a fresh approach to analyzing their language properties and bounds.

Findings

Reproved exponential bound on shortest accepting run length

Proved a new pumping lemma for 2-VASS languages

Potential applications in decidability and regular separability

Abstract

We propose a new pumping technique for 2-dimensional vector addition systems with states (2-VASS) building on natural geometric properties of runs. We illustrate its applicability by reproving an exponential bound on the length of the shortest accepting run, and by proving a new pumping lemma for languages of 2-VASS. The technique is expected to be useful for settling questions concerning languages of 2-VASS, e.g., for establishing decidability status of the regular separability problem.

Equations

$$\rho =(c_0,t_1,c_1),(c_1,t_2,c_2),\dots ,(c_{n-1},t_n,c_n)\in (\text{Conf}\times T\times \text{Conf}{)}^{\ast }$$

$$\text{scCone}(v_1,\dots ,v_k):=\{{\Sigma }_{j=1}^k{a}_j{v}_j\in {\mathbb{Q}}^2\mid a_1,\dots ,a_k\in {\mathbb{Q}}_{\ge 0}\}.$$

$$\text{scSeqCone}(v_1,\dots ,v_k):=\{{\Sigma }_{j=1}^k{a}_j{v}_j\in {\mathbb{Q}}_{\ge 0}^2\mid a_1,\dots ,a_k\in {\mathbb{Q}}_{\ge 0},{\forall }_i{\Sigma }_{j=1}^i{a}_j{v}_j\in {\mathbb{Q}}_{\ge 0}^2\}.$$

$$\text{scSeqCone}(v_1,\dots ,v_k)=$$

$$=\{\begin{array}{ll}\text{scCone}(v_k,v)& \text{if }{v}_k\in \measuredangle [v_0,u)\\ \text{scCone}(u,v)& \text{if }{v}_k\in \measuredangle [u,v]\\ \text{scCone}(u,v_k)& \text{if }{v}_k\in \measuredangle (v,h_0]\\ \text{scCone}(u,h_0)& \text{if }{v}_k\in \measuredangle (h_0,-u]\\ \text{scCone}(v_0,h_0)& \text{if }{v}_k\in \measuredangle (-u,-v)\\ \text{scCone}(v_0,v)& \text{if }{v}_k\in \measuredangle [-v,v_0).\end{array}$$

$${\mathcal{B}}_{v,W}=\{u\in {\mathbb{N}}^2\mid \text{dist}(u,{\ell }_v)\le W\},$$

$$\displaystyle p(nM)^{n}\geq\sqrt{2}\cdot\big{(}\left(P(nM)\right)^{n}+(nM+1)^{3}\big{)}\cdot nM.$$

$$c_{i+1}=c_i+s+\bar{v},$$

$$u:=u^{\prime }+s$$

$$\Vert u-c_{i+1}\Vert =\Vert u^{\prime }+s-c_i-s-\bar{v}\Vert \le \Vert u^{\prime }-c_i\Vert +\Vert \bar{v}\Vert \le \Vert u^{\prime }-c_i\Vert +nM\le P(nM{)}^n+(i+1)nM$$

$$a_1{v}_1$$

$$a_1{v}_1+a_2{v}_2$$

$$a_1{v}_1+a_2{v}_2+a_3{v}_3$$

$$a_1{v}_1+a_2{v}_2+a_3{v}_3+a_4{v}_4$$

$$(x,y)=(x^{\prime },y^{\prime }).$$

$${\rho }_1{\alpha }_1{\rho }_2{\alpha }_2{\rho }_3{\alpha }_3{\rho }_4{\alpha }_4{\rho }_5{\rho }_5^{\prime }{\alpha }_4^{\prime }{\rho }_4^{\prime }{\alpha }_3^{\prime }{\rho }_3^{\prime }{\alpha }_2^{\prime }{\rho }_2^{\prime }{\alpha }_1^{\prime }{\rho }_1^{\prime }.$$

$${\rho }_1{\alpha }_1^i{\rho }_2{\alpha }_2^i{\rho }_3{\alpha }_3^i{\rho }_4{\alpha }_4^i{\rho }_5{\rho }_5^{\prime }({\alpha }_4^{\prime }{)}^i{\rho }_4^{\prime }({\alpha }_3^{\prime }{)}^i{\rho }_3^{\prime }({\alpha }_2^{\prime }{)}^i{\rho }_2^{\prime }({\alpha }_1^{\prime }{)}^i{\rho }_1^{\prime }$$

$$(x,y)+({\delta }_x,{\delta }_y)=(x^{\prime },y^{\prime }).$$

$$\tilde{\rho }={\rho }_1{\tilde{\rho }}_2{\tilde{\rho }}_3{\tilde{\rho }}_4{\tilde{\rho }}_5,{\tilde{\rho }}^{\prime }={\tilde{\rho }}_5^{\prime }{\tilde{\rho }}_4^{\prime }{\tilde{\rho }}_3^{\prime }{\tilde{\rho }}_2^{\prime }{\sigma }_1,$$

$$\text{eff}(\tilde{\rho })-\text{eff}(\text{rev}({\tilde{\rho }}^{\prime }))=(am,bm)\text{for some integers a,b∈Z polynomial in A.}$$

$$\bar{\rho }={\rho }_1{\pi }_1^{a_1}{\tilde{\rho }}_2{\pi }_2^{a_2}{\tilde{\rho }}_3{\pi }_3^{a_3}{\tilde{\rho }}_4{\pi }_4^{a_4}{\tilde{\rho }}_5,{\bar{\rho }}^{\prime }={\tilde{\rho }}_5^{\prime }({\pi }_4^{\prime }{)}^{a_4^{\prime }}{\tilde{\rho }}_4^{\prime }({\pi }_3^{\prime }{)}^{a_3^{\prime }}{\tilde{\rho }}_3^{\prime }({\pi }_2^{\prime }{)}^{a_2^{\prime }}{\tilde{\rho }}_2^{\prime }({\pi }_1^{\prime }{)}^{a_1^{\prime }}{\rho }_1^{\prime },$$

$$\begin{array}{rl}{a}_{1}m{v}_1& \ge \max (e_2,f_2)\\ a_{1}m{v}_1+a_{2}m{v}_2& \ge \max (e_2,e_3,f_3)\\ a_{1}m{v}_1+a_{2}m{v}_2+a_{3}m{v}_3& \ge \max (e_3,e_4,f_4)\\ a_{1}m{v}_1+a_{2}m{v}_2+a_{3}m{v}_3+a_{4}m{v}_4& \ge \max (e_4,e_5,f_5)\end{array}$$

$$\text{eff}(\bar{\rho })-\text{eff}(\text{rev}({\bar{\rho }}^{\prime }))=(am,bm)\text{for some integers a,b∈Z polynomial in A.}$$

$$t[2]\le c_m[2]\le c_0[2]+mM\le s[2]+mM.$$

$$t[2]>s[2]+KnM.$$

$$\displaystyle Q(x)\$$

$$t[2]\le (s+r+p^{\prime })[2].$$

$$t[2]\le (\Vert s\Vert +\Vert r\Vert )\cdot (1+nM)\le (\Vert s\Vert +(n-1)M)\cdot (1+nM).$$

$$\Vert t_i\Vert \le Q(n,M)\cdot (\Vert s_i\Vert +1)$$

$$\Vert t_{i+1}\Vert \le$$

$$Q(nM)\cdot (\Vert t_i\Vert +M+1)\le$$

$$Q(nM)\cdot (P(nM{)}^i+M+1)\le P(nM{)}^{i+1},$$

$$\Vert p_u-p_v\Vert =w^{\prime }[2]\frac{|u[1]v[2]-v[1]u[2]|}{u[2]v[2]}.$$

Full text

1 Introduction

Vector addition systems [8] are a widely accepted model of concurrency equivalent to Petri nets. Another equivalent model, called vector addition systems with states (VASS) [7], is an extension of finite automata with integer counters, on which the transitions can perform operations of increment or decrement (but no zero tests), with the proviso that counter values are 0 initially and must stay non-negative along a run. The number of counters $d$ defines the dimension of a VASS. For brevity, we call a VASS of dimension $d$ a $d$-VASS. Formally, every transition of a $d$-VASS $V$ has adjoined a vector $v\in\mathbb{Z}^{d}$ describing the effect of executing this transition on counter values; thus a transition is a triple $(q,v,q^{\prime})\in Q\times\mathbb{Z}^{d}\times Q$, where $Q$ is the set of control states of $V$. A finite path, i.e., a sequence of transitions of the form $\pi\ =\ (q_{0},v_{1},q_{1}),(q_{1},v_{2},q_{2}),\ldots,(q_{n-1},v_{n},q_{n})$, induces a run if the counter values stay non-negative, i.e., $v_{1}+\ldots+v_{i}\in\mathbb{N}^{d}$ for every $i$.

In this paper we concentrate on pumping, i.e., techniques exploiting repetitions of states in runs. Pumping is an ubiquitous phenomenon which typically provides valuable tools in proving short run properties, or showing language inexpressibility results. It seems to be particularly relevant in case of VASS, as even the core of the seminal decision procedure for the reachability problem in VASS by Mayr and Kosaraju [11, 9] is fundamentally based on pumping: briefly speaking, the decision procedure decomposes a VASS into a finite number of VASS, each of them admitting a property that every path can be pumped up so that it induces a run. Pumping techniques are used even more explicitly when dealing with subclasses of VASS of bounded dimension. The PSpace upper bound for the reachability problem in 2-VASS [2] relies on various un-pumping transformations of an original run, leading to a simple run of at most exponential length, in the form of a short path with adjoined short disjoint cycles. A smart surgery on those simple runs was also used to obtain a stronger upper bound (NL) in case when the transition effects are represented in unary [6]. Un-pumping is also used in [3] to provide a quadratic bound on the length of the shortest run for 1-VASS, also known as one counter automata without zero tests, and for unrestricted one counter automata. See also [1, 10] for pumping techniques in one counter automata.

Contribution.

The above-mentioned techniques are mostly oriented towards reachable sets, and henceforth may ignore certain runs as long as the reachable set is preserved. In consequence, they are not very helpful in solving decision problems formulated in terms of the whole language accepted by a VASS, like the regular separability problem (cf. the discussion below). Our primary objective is to design a pumping infrastructure applicable to every run of a 2-VASS. Therefore, as our main technical contribution we perform a thorough classification of runs, in the form of a dichotomy (see the illustrations on the right): for every run $\pi$ of a 2-VASS, whose initial and final values of both counters are 0,

• •

either $\pi$ is thin, by which we mean that the counter values along the run stay within belts, whose direction and width are all bounded polynomially in the number of states and the largest absolute value of vectors of the 2-VASS;

• •

or $\pi$ is thick, by which we mean that a number of cycles is enabled along the run, the effect vectors of these cycles span (slightly oversimplifying) the whole plane, and furthermore the lengths of cycles and the extremal factors of $\pi$ are all bounded polynomially in $M$ and exponentially in $n$. (For the sake of simplicity some details are omitted here; the fully precise statement of the dichotomy is theorem 1 in section 3).

The dichotomy immediately entails a pumping lemma for 2-VASS by using, essentially, the pumping scheme of 1-VASS in case of thin runs, and the cycles enabled along a run in case of thick runs (cf. theorem 2). As a more subtle application of the dichotomy, we derive an alternative proof of the exponential run property (shown originally in [2]), which immediately implies PSpace-membership of the reachability problem (cf. theorem 3).

Further applications.

We envisage other possible applications of the dichotomy. One important case can be the regular separability problem: given two labeled 2-VASS $V_{1}$ and $V_{2}$, decide if there is a regular language separating languages of $V_{1}$ and $V_{2}$, i.e., including one of them and disjoint from the other. The problem is decidable in PSpace for 1-VASS [5] while the decidability status for 2-VASS is still open. A cornerstone of the decision procedure of [5] is a well-behaved over-approximation of a language of a 1-VASS $V$ by a sequence of regular languages $(V_{n})_{n\in\mathbb{N}}$, where the precision of approximation increases with increasing $n$. In case of 1-VASS, the language $V_{n}$ is obtained by abstraction of $V$ modulo $n$; on the other hand, as argued in [5], the very same approach necessarily fails for dimensions larger than 1. It seems that our dichotomy classification of runs of a 2-VASS prepares the ground for the right definition of abstraction $V_{n}$ modulo $n$. Indeed, intuitively speaking, as long as the run stays within belts, 1-dimensional counting modulo $n$ along the direction of a belt is sufficient; otherwise, a 2-dimensional abstraction modulo $n$ can be applied as soon as a sufficient number of pumpable cycles has been identified along a run.

As our approach builds on natural geometric properties of runs, we believe that it can be generalized to dimensions larger than 2. However, one should not expect efficient length bounds from this generalization itself, as already in dimension 3 the prefix of a run preceding the first pumpable cycle has non-elementary length (the length can be as large as tower of $n$ exponentials in the composition of $n$ copies of the Hopcroft and Pansiot example [7]).

2 Preliminaries

2-dimensional vector addition systems with states.

We use standard symbols $\mathbb{Q},\mathbb{Z},\mathbb{N}$ for the sets of rationals, integers, and non-negative integers, respectively. Whenever convenient we use subscripts to specify subsets, e.g., $\mathbb{Q}_{\geq 0}$ for non-negative rationals. We refer to elements of $\mathbb{Z}^{2}$ briefly as vectors. Non-negative vectors are elements of $\mathbb{N}^{2}$, and positive vectors are elements of $\mathbb{Z}_{>0}^{2}$. A vector with only non-negative coordinates and at least one positive coordinate is called semi-positive; it is either positive, or vertical of the form $(0,a)$, or horizontal of the form $(a,0)$, for $a\in\mathbb{Z}_{>0}$.

A $2$-dimensional vector addition system with states (2-VASS) $V$ consists of a finite set of control states $Q$ and a finite set of transitions $T\subseteq Q\times\mathbb{Z}^{2}\times Q$. We refer to the vector $v$ as the effect of a transition $(p,v,q)$. A path in $V$ from control state $p$ to $q$ is a sequence of transitions $\pi=(q_{0},v_{1},q_{1}),(q_{1},v_{2},q_{2}),\ldots,(q_{n-1},v_{n},q_{n})\in T^{*}$ where $p=q_{0}$ and $q=q_{n}$; it is called a cycle whenever the starting and ending control states coincide ($q_{0}=q_{n}$). The effect of a path is defined as $\textup{eff}(\pi)=v_{1}+\ldots+v_{n}\in\mathbb{Z}^{2}$, and its length is $n$. A cycle is called non-negative, semi-positive or positive, if its effect is so.

A configuration of $V$ is an element of $\textup{Conf}=Q\times\mathbb{N}^{2}$. A transition $t=(p,v,q)$ is enabled in a configuration $c=(p^{\prime},u)$ if $p=p^{\prime}$ and $u+v\in\mathbb{N}^{2}$. Analogously, a path $\pi$ is enabled in a configuration $c=(p^{\prime},u)$ if $q_{0}=p^{\prime}$ and $u_{i}=u+v_{1}+\ldots+v_{i}\in\mathbb{N}^{2}$ for every $i$. In such case we say that $\pi$ induces a run of the form

[TABLE]

with intermediate configurations $c_{i}=(q_{i},u_{i})$, from the source configuration $\textup{src}(\rho)=c_{0}$ to the target one $\textup{trg}(\rho)=c_{n}$. If the source configuration $c_{0}$ is clear from the context, we do not distinguish between a path enabled in $c_{0}$ and a run with source $c_{0}$, and simply say that the path is the run. A $(0,0)$-run is a run whose source and target are $(0,0)$-configurations, i.e., a configuration whose vector is $(0,0)$.

We will sometimes relax the non-negativeness requirement on some coordinates: For $j\in\{1,2\}$, we say that a path $\pi$ is $\{j\}$-enabled in a configuration $c=(p^{\prime},u)$ if $q_{0}=p^{\prime}$ and $(u+v_{1}+\ldots+v_{i})[j]\in\mathbb{N}$ for every $i$. We also say that $\pi$ is $\emptyset$-enabled in $c$ if just $q_{0}=p^{\prime}$.

The reversal of a 2-VASS $V=(Q,T)$, denoted $\textup{rev}(V)$, is a 2-VASS with the same control states and with transitions $\{(q,-v,p)\mid(p,v,q)\in T\}$. We sometimes speak of the reversal $\textup{rev}(\rho)$ of a run $\rho$ of $V$, implicitly meaning a run in the reversal of $V$.

As the norm of $v=(v_{1},v_{2})\in\mathbb{Q}^{2}$, we take the largest of absolute values of $v_{1}$ and $v_{2}$, $\lVert v\rVert:=\max\{|v_{1}|,|v_{2}|\}.$ By the norm of a configuration $c=(q,v)$ we mean the norm of its vector $v$, and by the norm $\lVert V\rVert$ of a 2-VASS $V$ we mean the largest among norms of effects of transitions.

Sequential cones.

For a vector $v\in\mathbb{Z}^{2}$, define the half-line induced by $v$ as $\ell_{v}:=\mathbb{Q}_{\geq 0}\cdot v=\{\alpha v\mid\alpha\in\mathbb{Q}_{\geq 0}\}$. We call two vectors $v,w$ colinear if $\ell_{v}=\ell_{w}$, and contralinear if $\ell_{v}=\ell_{-w}$. For two vectors $u,v\in\mathbb{Z}^{2}\setminus\{(0,0)\}$, define the angle $\measuredangle[u,v]\subseteq\mathbb{Q}^{2}$ as the union of all half-lines which lie clock-wise between $\ell_{u}$ and $\ell_{v}$, including the two half-lines themselves. In particular, $\measuredangle[v,v]=\ell_{v}$. Analogously we define the sets $\measuredangle[u,v)$, $\measuredangle(u,v]$ and $\measuredangle(u,v)$ which exclude one or both of the half-lines. We refer to an angle of the form $\measuredangle[v,-v]$ as half-plane. We write $v\circlearrowright u$ when $u\in\measuredangle(v,-v)$, i.e., $u$ is oriented clock-wise with respect to $v$ (see Figure 2 for an illustration). Note that $\circlearrowright$ defines a total order on pairwise non-colinear non-negative vectors.

By the cone of a finite set of vectors $\{v_{1},\ldots,v_{k}\}\subseteq\mathbb{Z}^{2}$ we mean the set of all non-negative rational linear combinations of these vectors:

[TABLE]

We call the cone of a single vector $\textup{\sc Cone}(v)=\ell_{v}$ trivial, and the cone of zero vectors $\textup{\sc Cone}(\emptyset)=\{(0,0)\}$ degenerate. Two non-zero vectors $v_{1}$ and $v_{2}$ can be in four distinct relations: (i) they are colinear, (ii) they are contralinear, (iii) $v_{1}\circlearrowright v_{2}$ and hence $\textup{\sc Cone}(v_{1},v_{2})=\measuredangle[v_{1},v_{2}]$, (iv) $v_{2}\circlearrowright v_{1}$ and hence $\textup{\sc Cone}(v_{1},v_{2})=\measuredangle[v_{2},v_{1}]$.

Lemma 1**.**

Every cone either equals the whole plane $\mathbb{Q}^{2}$, or is included in some half-plane.

Proof.

Assume, w.l.o.g. that the vectors $v_{1},\ldots,v_{k}$ are non-zero and include no colinear pair. Suppose there is a contralinear pair $v_{i},v_{j}$ among $v_{1},\ldots,v_{k}$. If all other vectors $v_{h}$ satisfy $v_{i}\circlearrowright v_{h}\circlearrowright v_{j}$ then $\textup{\sc Cone}(v_{1},\ldots,v_{k})$ is included in the half-plane $\measuredangle[v_{i},v_{j}]$. Otherwise $\textup{\sc Cone}(v_{1},\ldots,v_{k})$ is the whole plane.

Now suppose there is no contralinear pair among $v_{1},\ldots,v_{k}$. If some three $v_{i},v_{j},v_{h}$ of them satisfy $v_{i}\circlearrowright v_{j}\circlearrowright v_{h}\circlearrowright v_{i}$ then $\textup{\sc Cone}(v_{1},\ldots,v_{k})$ includes the three angles $\measuredangle[v_{i},v_{j}]$, $\measuredangle[v_{j},v_{h}]$ and $\measuredangle[v_{h},v_{i}]$, the union of which is the whole plane. Otherwise, the relation $\circlearrowright$ is transitive and hence defines a (strict) total order on $\{v_{1},\ldots,v_{k}\}$. The minimal and maximal element $v_{i}$ and $v_{j}$ w.r.t. the order satisfy $v_{i}\circlearrowright v_{j}$, and hence $\textup{\sc Cone}(v_{1},\ldots,v_{k})=\measuredangle[v_{i},v_{j}]$ is included in the half-plane $\measuredangle[v_{i},-v_{i}]$. ∎

The sequential cone of vectors $v_{1},\ldots,v_{k}\in\mathbb{Z}^{2}$ imposes additional non-negativeness conditions, namely for every $i$, the partial sum $a_{1}v_{1}+\ldots+a_{i}v_{i}$ must be non-negative (this is required later, when pumping cycles in a run whose effects are $v_{1},\ldots,v_{k}$ in that order):

[TABLE]

Note that $v_{1}$ may be assumed w.l.o.g. to be semi-positive, but other vectors $v_{i}$ are not necessarily non-negative; and that every sequential cone is a subset of the non-negative orthant $\mathbb{Q}_{\geq 0}^{2}$. Importantly, contrarily to cones, the order of vectors $v_{1},\ldots,v_{k}$ matters for sequential cones. In fact, sequential cones are just convenient syntactic sugar for cones of pairs of non-negative vectors:

Lemma 2**.**

For all vectors $v_{1},\ldots,v_{k}$, the sequential cone $\textup{\sc SeqCone}(v_{1},\ldots,v_{k})$, if not degenerate, equals $\textup{\sc Cone}(u,v)$, for two non-negative vectors $u$, $v$, and each of them either belongs to $\{v_{1},\ldots,v_{k}\}$, or is horizontal, or vertical.

Proof.

We proceed by induction on $k$. For $k=1$ we have $\textup{\sc SeqCone}(v_{1})=\ell_{v_{1}}=\textup{\sc Cone}(v_{1},v_{1})$. Let $v_{0}$ and $h_{0}$ denote some fixed vertical and horizontal vector, respectively. For the induction step we assume $\textup{\sc SeqCone}(v_{1},\ldots,v_{k-1})=\textup{\sc Cone}(u,v)$ for non-negative vectors $u$, $v$; and compute the value of $\textup{\sc SeqCone}(v_{1},\ldots,v_{k})$, separately in each of the following distinct cases (assume w.l.o.g. $u\circlearrowright v$):

[TABLE]

∎

3 Thin-Thick Dichotomy

The main result of this section (cf. theorem 1 below) classifies $(0,0)$-runs in a 2-VASS into thin and thick ones. Throughout this section we consider an arbitrary fixed 2-VASS $V=(Q,T)$.

Let $n=|Q|$ and $M=\lVert V\rVert$.

Thin runs.

The belt of direction $v\in\mathbb{N}^{2}$ and width $W$ is the set

[TABLE]

where $\textup{dist}(u,\ell_{v})$ denotes the Euclidean distance between the point $u$ and the half-line $\ell_{v}$. For $A\in\mathbb{N}$, we call ${\cal B}_{v,W}$ an $A$-belt if $\lVert v\rVert\leq A$ and $W\leq A$. We say that a run $\rho$ of $V$ is $A$-thin if for every configuration $c$ in $\rho$ there exists an $A$-belt $B$ such that $c\in Q\times B$.

Thick runs.

Let $A\in\mathbb{N}$. Four cycles $\pi_{1},\pi_{2},\pi_{3},\pi_{4}\in T^{*}$ are $A$-sequentially enabled in a run $\rho$ if their lengths are at most $A$, and the run $\rho$ factors into $\rho=\rho_{1}\,\rho_{2}\,\rho_{3}\,\rho_{4}\,\rho_{5}$ so that (denote by $v_{1},v_{2},v_{3},v_{4}$ the effects of $\pi_{1},\pi_{2},\pi_{3},\pi_{4}$, respectively):

• •

The effect $v_{1}$ is semi-positive, the cycle $\pi_{1}$ is enabled in $c_{1}:=\textup{trg}(\rho_{1})$, and both coordinates are bounded by $A$ along $\rho_{1}$.

• •

If $v_{1}$ is positive then $\pi_{2}$ is $\emptyset$-enabled in $c_{2}:=\textup{trg}(\rho_{2})$. Otherwise (let $j$ be the coordinate s.t. $v_{1}[j]=0$) $\pi_{2}$ is $\{j\}$-enabled in $c_{2}:=\textup{trg}(\rho_{2})$, and $j$th coordinate is bounded by $A$ along $\rho_{2}$.

• •

The cycle $\pi_{i}$ is $\emptyset$-enabled in $c_{i}:=\textup{trg}(\rho_{i})$, for $i=3,4$.

We also say that the four vectors $v_{1},v_{2},v_{3},v_{4}$ are $A$-sequentially enabled in $\rho$, quantifying the cycles existentially. A $(0,0)$-run $\tau$ is called A-thick if it partitions into $\tau=\rho\,\rho^{\prime}$ so that

some vectors $v_{1},v_{2},v_{3},v_{4}$ are $A$-sequentially enabled in $\rho$, 2. 2.

some vectors $v^{\prime}_{1},v^{\prime}_{2},v^{\prime}_{3},v^{\prime}_{4}$ are $A$-sequentially enabled in $\textup{rev}(\rho^{\prime})$, 3. 3.

$\textup{\sc SeqCone}(v_{1},v_{2},v_{3},v_{4})\cap\textup{\sc SeqCone}(v^{\prime}_{1},v^{\prime}_{2},v^{\prime}_{3},v^{\prime}_{4})$ is non-trivial.

Figure 4 illustrates the geometric ideas underlying these three conditions for $A$-thick runs. Concerning condition 1, a cycle $\pi_{1}$ depicted by a dotted line, with vertical effect $v_{1}$, can be used to increase the second (vertical) coordinate arbitrarily, which justifies the relaxed requirement that a cycle $\pi_{2}$ with effect $v_{2}$ is only $\{1\}$-enabled. Note that the norm of the configuration enabling $\pi_{1}$, as well as the first coordinate of the configuration enabling $\pi_{2}$, are bounded by $A$. Concerning condition 2, a cycle $\pi^{\prime}_{1}$ with positive effect $v^{\prime}_{1}$ can be used to increase both coordinates arbitrarily; therefore a cycle $\pi^{\prime}_{2}$ with effect $v^{\prime}_{2}$ is only required to be $\emptyset$-enabled, and no coordinate of the configuration enabling $\pi^{\prime}_{2}$ is required to be bounded by $A$. In the illustrated example, vectors $v^{\prime}_{3}$ and $v^{\prime}_{4}$ are not needed; formally, one can assume $v^{\prime}_{2}=v^{\prime}_{3}=v^{\prime}_{4}$ and $\rho^{\prime}_{3}=\rho^{\prime}_{4}=\varepsilon$. Condition 3 ensures that the cycles $\pi_{1},\ldots,\pi_{4}$ and $\pi_{1}^{\prime},\ldots,\pi_{4}^{\prime}$ can be pumped such that the pumped versions of $\rho$ and $\rho^{\prime}$ are still connected. In the illustrated example, observe that $\textup{\sc SeqCone}(v_{1},v_{2})\cap\textup{\sc SeqCone}(v^{\prime}_{1})=\emptyset$. Intuitively, both coordinates in the target of $\rho$ can be increased arbitrarily using $v_{1}$ and $v_{2}$, and similarly both coordinates of the target of $\textup{rev}(\rho^{\prime})$ can be increased arbitrarily using $v^{\prime}_{1}$, but ‘directions of increase’ are non-crossing. Adding $v_{3}$ and $v^{\prime}_{2}$ is not sufficient, as still $\textup{\sc SeqCone}(v_{1},v_{2},v_{3})\cap\textup{\sc SeqCone}(v^{\prime}_{1},v^{\prime}_{2})=\emptyset$. When vector $v_{4}$ is adjoined, condition 3 holds as $\textup{\sc SeqCone}(v_{1},v_{2},v_{3},v_{4})=\mathbb{Q}_{\geq 0}^{2}$. Finally, the four vectors are really needed here, e.g., vector $v_{3}$ can not be omitted as $\textup{\sc SeqCone}(v_{1},v_{2},v_{4})=\textup{\sc SeqCone}(v_{1},v_{2})$.

Here is the main result of this section:

Theorem 1** (Thin-Thick Dichotomy).**

There is a polynomial $p$ such that every $(0,0)$-run in a 2-VASS $V$ is either $p(nM)^{n}$-thin or $p(nM)^{n}$-thick.

For the proof of theorem 1 we need the following core fact (shown in the appendix):

Lemma 3** (Non-negative Cycle Lemma).**

There is a polynomial $P$ such that every run $\rho$ in $V$ from a $(0,0)$-configuration to a target configuration of norm larger than $P(nM)^{n}$, contains a configuration enabling a semi-positive cycle of length at most $P(nM)$.

Proof of theorem 1.

Let $P$ be the polynomial from lemma 3. The polynomial $p$ required in theorem 1 can be chosen arbitrarily as long as p(x)\geq\sqrt{2}\cdot\big{(}P(x)+(x+1)^{3}\big{)}\cdot x. for all $x$; note that the following inequality follows:

[TABLE]

In the sequel we deliberately confuse configurations $c=(q,v)$ with their vectors $v$: whenever convenient, we use $c$ to denote the vector $v$, hoping that this does not lead to any confusion.

Let $\tau$ be a $(0,0)$-run of $V$ which is not $p(nM)^{n}$-thin, i.e., $\tau$ contains therefore a configuration $t$ which lies outside of all the $p(nM)^{n}$-belts. We need to demonstrate points 1–3 in the definition of thick run. To this aim we split $\tau$ into $\tau=\rho\,\rho^{\prime}$ where $\textup{trg}(\rho)=t=\textup{src}(\rho^{\prime})$, and are going to prove the following two claims (a) and (a’). Let $D:=P(nM)^{n}+(nM+1)^{3}$. For $x,y\in\mathbb{Q}^{2}$, let $\textup{dist}(x,y)$ denote their Euclidean distance.

1. (a)

Some vectors $v_{1},v_{2},v_{3},v_{4}$ are $P(nM)^{n}$-sequentially enabled in $\rho$, and the sequential cone $\textup{\sc SeqCone}(v_{1},v_{2},v_{3},v_{4})$ contains a point $u\in\mathbb{Q}_{\geq 0}^{2}$ with $\lVert u-t\rVert\leq D$. 2. (a’)

Some vectors $v^{\prime}_{1},v^{\prime}_{2},v^{\prime}_{3},v^{\prime}_{4}$ are $P(nM)^{n}$-sequentially enabled in $\textup{rev}(\rho^{\prime})$, and the sequential cone $\textup{\sc SeqCone}(v^{\prime}_{1},v^{\prime}_{2},v^{\prime}_{3},v^{\prime}_{4})$ contains a point $u\in\mathbb{Q}_{\geq 0}^{2}$ with $\lVert u-t\rVert\leq D$.

In simple words, instead of proving point 3, we prove that both sequential cones contain a point $v$ which is sufficiently close to $t$.

Claim 1**.**

The conditions (a) and (a’) guarantee that $\tau$ is thick.

Indeed, points 1–2 in the definition of thick run are immediate as $P(nM)\leq p(nM)$. For point 3, observe that the inequality (1) implies $p(nM)^{n}\geq\sqrt{2}\cdot D$, which guarantees that the circle $\{u\in\mathbb{Q}_{\geq 0}^{2}\mid\textup{dist}(u,t)\leq\sqrt{2}\cdot D\}$ does not touch any half-line $\ell_{w}$ induced by a non-negative vector $w$ with $\lVert w\rVert\leq p(nM)^{n}$. In consequence, neither does the square $X:=\{u\in\mathbb{Q}_{\geq 0}^{2}\mid\lVert u-t\rVert\leq D\}$ inscribed in the circle, and hence $X$ lies between two consecutive half-lines $\ell_{w}$ induced by a non-negative vector $w$ with $\lVert w\rVert\leq p(nM)^{n}$. Hence, as $\textup{\sc SeqCone}(v_{1},v_{2},v_{3},v_{4})$ contains some point of $X$, by lemma 2 it includes the whole $X$, and likewise $\textup{\sc SeqCone}(v^{\prime}_{1},v^{\prime}_{2},v^{\prime}_{3},v^{\prime}_{4})$. In consequence, the whole $X$ is included in $\textup{\sc SeqCone}(v_{1},v_{2},v_{3},v_{4})\cap\textup{\sc SeqCone}(v^{\prime}_{1},v^{\prime}_{2},v^{\prime}_{3},v^{\prime}_{4})$ which entails point 3. 1 is thus proved.

As condition (a’) is fully symmetric to (a), we focus exclusively on proving condition (a), i.e., on constructing sequentially enabled vectors $v_{1},v_{2},v_{3},v_{4}$.

Vector $t$ lies outside of $p(nM)^{n}$-belts, hence outside of all the $P(nM)^{n}$-belts, therefore its norm $\lVert t\rVert>P(nM)^{n}$. Relying on lemma 3, let $c_{1}$ be the first configuration in the run $\rho$ which enables a semi-positive cycle $\pi_{1}$ of length bounded by $P(nM)$, and let $v_{1}=\textup{eff}(\pi_{1})$. We start with the following obvious claim (let $v_{0}$ be some vertical vector, e.g. $v_{0}=(0,1)$):

Claim 2**.**

$\textup{\sc SeqCone}(v_{0})$* contains a point $u\in\mathbb{Q}_{\geq 0}^{2}$ such that $\lVert u-c_{1}\rVert\leq P(nM)^{n}+nM$.*

Indeed, due to lemma 3 we may assume $\lVert c_{1}\rVert\leq P(nM)^{n}+M$ and hence $u=(0,0)$ does the job.

Recall that the relation $\circlearrowright$ defines a total order on pairwise non-colinear non-negative vectors.

Claim 3**.**

We can assume w.l.o.g. that $v_{1}\circlearrowright t$.

Indeed, if $v_{1}$ and $t$ were colinear then $t\in\textup{\sc Cone}(v_{1})$ and hence condition (a) would hold.

Split $\rho$ into the prefix ending in $c_{1}$ and the remaining suffix: $\rho=\rho_{1}\,\sigma$, where $\textup{trg}(\rho_{1})=c_{1}=\textup{src}(\sigma)$. As the next step we will identify a configuration $c_{2}$ in $\sigma$ which satisfies 4 (which will serve later as the basis of induction) and enables a cycle $\pi_{2}$ with effect $v_{2}$ (as stated in 5).

Claim 4**.**

$\textup{\sc SeqCone}(v_{0},v_{1})$* contains a point $u\in\mathbb{Q}_{\geq 0}^{2}$ such that $\lVert u-c_{2}\rVert\leq P(nM)^{n}+2nM$.*

The proof of 4 depends on whether $v_{1}$ is positive. If $v_{1}$ is so, we simply duplicate the first cycle: $c_{2}:=c_{1}$ and $\pi_{2}:=\pi_{1}$, and use 2. Otherwise $v_{1}$ is vertical due to 3. If $t[1]\leq W=P(nM)^{n}+(n+1)M$ then condition (a) holds immediately as $\textup{\sc SeqCone}(v_{1})=\ell_{v_{1}}$ contains a point $u\in\mathbb{Q}_{\geq 0}^{2}$ with $\lVert u-t\rVert\leq P(nM)^{n}+(n+1)M\leq D$. Therefore suppose $t[1]>P(nM)^{n}+(n+1)M$, and define the sequence $d_{1},\ldots,d_{m}$ of configurations as follows: let $d_{1}:=c_{1}$, and let $d_{i+1}$ be the first configuration in $\sigma$ with $d_{i+1}[1]>d_{i}[1]$. Recall that $d_{1}[1]\leq P(nM)^{n}+M$, and observe that $d_{i+1}[1]\leq d_{i}[1]+M$. Thus by the pigeonhole principle $m>n$ and hence for some $i<j\leq n+1$ the configurations $d_{i}$ and $d_{j}$ must have the same control state. The infix $\sigma_{ij}$ of the path $\sigma$ from $d_{i}$ to $d_{j}$ is thus a cycle, enabled in $d_{i}$, whose effect is positive on the first (horizontal) coordinate. Let $c_{2}:=d_{i}$. As $c_{2}[1]\leq P(nM)^{n}+(n+1)M$, $\textup{\sc SeqCone}(v_{0},v_{1})=\ell_{v_{0}}$ contains necessarily a point $u\in\mathbb{Q}_{\geq 0}^{2}$ such that $\lVert u-c_{2}\rVert\leq P(nM)^{n}+(n+1)M$, which proves 4.

Claim 5**.**

The configuration $c_{2}$ $\{1\}$-enables a cycle $\pi_{2}$ of length bounded by $p(nM)^{n}$, such that the first coordinate of $\textup{eff}(\pi_{2})$ is positive.

Recalling the proof of the previous claim, observe that the first (horizontal) coordinate in the infix $\sigma_{ij}$ is bounded by $P(nM)^{n}+(n+1)M$, and think of the second (vertical) coordinate as irrelevant. Let $\pi_{2}$ be the path inducing $\sigma_{ij}$. For bounding the length of $\pi_{2}$, as long as $\pi_{2}$ contains a cycle $\alpha$ with vertical effect $(0,w)$, remove $\alpha$ from $\pi_{2}$. This process ends yielding a cycle $\pi_{2}$ of length at most $(P(nM)^{n}+(n+1)M)\cdot n$, and hence at most $p(nM)^{n}$ (by the inequality (1)), which is $\{1\}$-enabled in $c_{2}$, but not necessarily enabled. Let $v_{2}:=\textup{eff}(\pi_{2})$.

Claim 6**.**

We can assume w.l.o.g. that $v_{2}\circlearrowright t$.

Indeed, if $v_{1}=v_{2}$ then 3 does the job; otherwise $v_{1}$ is vertical and then $t\circlearrowright v_{2}$ (or $t$ colinear with $v_{2}$) would imply $t\in\textup{\sc SeqCone}(v_{1},v_{2})$, hence condition (a) would hold again.

Split $\sigma$ further into the prefix ending in $c_{2}$ and the remaining suffix: $\sigma=\rho_{2}\sigma^{\prime}$, where $\textup{trg}(\rho_{2})=c_{2}=\textup{src}(\sigma^{\prime})$. If $\sigma^{\prime}$ contains a configuration which $\emptyset$-enables a simple cycle whose effect $w$ belongs to $\measuredangle[t,-v_{2})$ then $t\in\textup{\sc SeqCone}(v_{2},w)$ and hence condition (a) holds. We aim at achieving this objective incrementally.

For $i\geq 2$, let $c_{i+1}$ be the first configuration in $\sigma^{\prime}$ after $c_{i}$ that $\emptyset$-enables a simple cycle $\pi_{i+1}$ with effect $v_{i+1}\in\measuredangle(v_{i},-v_{i})$. As discussed above, if $v_{i+1}\in\measuredangle[t,-v_{i})$ for some $i$ then $t\in\textup{\sc SeqCone}(v_{i},v_{i+1})$ and hence condition (a) holds. Assume therefore that the sequence $v_{1},\ldots,v_{m}$ so defined satisfies $v_{i+1}\in\measuredangle(v_{i},t)$ for all $i\geq 2$. Let $c_{m+1}:=t$. As vectors $v_{3},\ldots,v_{m}$ are pairwise different, semi-positive and, being effects of simple cycles, have norms at most $nM$, we know that $m\leq(nM+1)^{2}+1$.

Claim 7**.**

For every $i=1,\ldots,m$, $\textup{\sc SeqCone}(v_{0},v_{i})$ contains a point $u\in\mathbb{Q}_{\geq 0}^{2}$ such that $\lVert u-c_{i+1}\rVert\leq P(nM)^{n}+(i+1)nM$.

Proof.

By induction on $i$. The induction base is exactly 4. For the induction step, we are going to show that $\textup{\sc SeqCone}(v_{0},v_{i})$ contains a vector $u$ such that $\lVert u-c_{i+1}\rVert\leq P(nM)^{n}+(i+1)nM$. Decompose the infix of $\sigma^{\prime}$ which starts in $c_{i}$ and ends in $c_{i+1}$ into simple cycles, plus the remaining path $\bar{\rho}$ of length at most $n$. The norm of the effect $\bar{v}$ of $\bar{\rho}$ is hence bounded by $nM$, and we have

[TABLE]

where $s$ is the sum of effects of all the simple cycles. By the definition of $v_{i+1}$, the effects of all the simple cycles belong to the half-plane $\measuredangle[-v_{i},v_{i}]$, and hence there belongs $s$. By induction assumption there is $u^{\prime}\in\textup{\sc SeqCone}(v_{0},v_{i-1})$ such that $\lVert u^{\prime}-c_{i}\rVert\leq P(nM)^{n}+inM$. As $v_{i-1}\circlearrowright v_{i}$, we also have $u^{\prime}\in\textup{\sc SeqCone}(v_{0},v_{i})$. Consider the point

[TABLE]

which necessarily belongs to the half-plane $\measuredangle[-v_{i},v_{i}]$ but not necessarily to $\textup{\sc SeqCone}(v_{0},v_{i})=\measuredangle[-v_{i},v_{i}]\cap\mathbb{Q}_{\geq 0}^{2}$. Ignoring this issue, by routine calculations we get

[TABLE]

as required for the induction step. Finally, if $u\notin\mathbb{Q}_{\geq 0}^{2}$, translate $u$ towards $c_{i+1}$ until it enters the non-negative orthant $\mathbb{Q}_{\geq 0}^{2}$; clearly, the translation can only decrease the value of $\lVert u-c_{i+1}\rVert$. ∎

Applying the claim to $i=m$, and knowing that $m\leq(nM+1)^{2}+1$, we get some point $u\in\textup{\sc SeqCone}(v_{0},v_{m})$ such that $\lVert u-t\rVert\leq P(nM)^{n}+((nM+1)^{2}+1)\cdot nM\leq P(nM)^{n}+(nM+1)^{3}$. Furthermore, relying on the assumptions that $t$ lies outside of all $p(nM)^{n}$-belts and that $v_{1}\circlearrowright t$ we prove, similarly as in the proof of 1, that $v_{1}\circlearrowright u$ and hence the point $u$ belongs also to $\textup{\sc SeqCone}(v_{1},v_{m})$. This completes the proof of theorem 1. ∎

4 Dichotomy in Action

This section illustrates applicability of theorem 1. As before, we use symbols $n$ and $M$ for the number of control states, and the norm of a 2-VASS, respectively. As the first corollary we provide a pumping lemma for 2-VASS: in case of thin runs apply, essentially, pumping schemes of 1-VASS, and in case of thick runs use the cycles enabled along a run. As another application, we derive an alternative proof of the exponential run property for 2-VASS.

Theorem 2** (Pumping).**

There is a polynomial $p$ such that every $(0,0)$-run $\tau$ in a 2-VASS of length greater that $p(nM)^{n}$ factors into $\tau\ =\ \tau_{0}\,\tau_{1}\,\ldots\,\tau_{k}$ ($k\geq 1$), so that for some non-empty cycles $\alpha_{1},\ldots,\alpha_{k}$ of length at most $p(nM)^{n}$, the path $\tau_{0}\,\alpha_{1}^{i}\,\tau_{1}\,\alpha_{2}^{i}\,\ldots,\,\alpha_{k}^{i}\,\tau_{k}$ is a $(0,0)$-run for every $i\in\mathbb{N}$. Furthermore, the lengths of $\tau_{0}$ and $\tau_{k}$ are also bounded by $p(nM)^{n}$.

Theorem 3** (Exponential run).**

There is a polynomial $p$ such that for every $(0,0)$-run $\tau$ in a 2-VASS, there is a $(0,0)$-run of length bounded by $p(nM)^{n}$ with the same source and target as $\tau$.

We fix from now on a 2-VASS $V=(Q,T)$ and the polynomial $p$ of theorem 1. Let $A=p(nM)^{n}$. Both proofs proceed separately for thin and thick runs $\tau$. The former (fairly standard) case is moved to the appendix, so assume below $\tau$ to be $A$-thick. The polynomials required in theorems 2 and 3 can be read out from the constructions.

We rely on the standard tool, cf. Prop. 2 in [4] (the norm of a system of inequalities is the largest absolute value of its coefficient, and likewise we define the norm of a solution):

Lemma 4**.**

Let ${\cal U}$ be a system of $d$ linear inequalities of norm $M$ with $k$ variables. Then the smallest norm of a non-negative-integer solution of ${\cal U}$ is in ${\cal O}(k\cdot M)^{d}$.

Consider a split $\tau=\rho\rho^{\prime}$, where $\rho=\rho_{1}\,\rho_{2}\,\rho_{3}\,\rho_{4}\,\rho_{5}$ and $\rho^{\prime}=\rho^{\prime}_{5}\,\rho^{\prime}_{4}\,\rho^{\prime}_{3}\,\rho^{\prime}_{2}\,\rho^{\prime}_{1}$, as well as cycles $\pi_{1},\ldots,\pi_{4}$ and $\pi^{\prime}_{1},\ldots,\pi^{\prime}_{4}$ given by the definition of thick run. Let $v_{1},\ldots,v_{4}$ and $v^{\prime}_{1},\ldots,v^{\prime}_{4}$ be the respective effects of $\pi_{1},\ldots,\pi_{4}$ and $\pi^{\prime}_{1},\ldots,\pi^{\prime}_{4}$. For $j=1,\ldots,4$ let $c_{j}=\textup{trg}(\rho_{j})$ and for $j=2,\ldots,4$ let $e_{j}\in\mathbb{N}^{2}$ be the minimal non-negative vector such that the configuration $c_{j}+e_{j}$ enables cycle $\pi_{j}$. We define the following system ${\cal U}$ of linear inequalities with 6 variables $a_{1},a_{2},a_{3},a_{4},x,y$ ($\max$ is understood point-wise):

[TABLE]

(Observe that when $v_{1}[j]=0$, i.e., in case when $v_{1}$ is vertical or horizontal, $e_{j}=0$ and therefore one of the two first inequalities is always satisfied, namely $a_{1}v_{1}[j]\,\geq\,e_{2}[j]$.) Likewise, we have a system of inequalities ${\cal U}^{\prime}$ with 6 variables $a^{\prime}_{1},a^{\prime}_{2},a^{\prime}_{3},a^{\prime}_{4},x^{\prime},y^{\prime}$. Observe that the sequential cone $\textup{\sc SeqCone}(v_{1},v_{2},v_{3},v_{4})$ contains exactly (projections on $(x,y)$ of) non-negative rational solutions of the modified system ${\cal U}^{(0,0)}$ obtained by replacing all the right-hand sides with $(0,0)$. Likewise we define ${{\cal U}^{\prime}}^{(0,0)}$. Finally, we define the compound system $\mathcal{C}$ by enhancing the union of ${\cal U}$ and ${\cal U}^{\prime}$ with two additional equalities (likewise we define the system $\mathcal{C}^{(0,0)}$)

[TABLE]

Claim 8**.**

$\mathcal{C}$* admits a non-negative integer solution $(a_{1},a_{2},a_{3},a_{4},x,y,a^{\prime}_{1},a^{\prime}_{2},a^{\prime}_{3},a^{\prime}_{4},x^{\prime},y^{\prime})$.*

Proof.

The system $\mathcal{C}^{(0,0)}$ admits a non-negative rational solution as the intersection of the cones $\textup{\sc SeqCone}(v_{1},v_{2},v_{3},v_{4})$ and $\textup{\sc SeqCone}(v^{\prime}_{1},v^{\prime}_{2},v^{\prime}_{3},v^{\prime}_{4})$ is non-empty by assumption. As intersection of cones is stable under multiplications by non-negative rationals, the solution can be scaled up arbitrarily, to yield a non-negative integer one, and even a non-negative integer solution of the stronger system $\mathcal{C}$. ∎

Claim 9**.**

For every non-negative integer solution of $\mathcal{C}$, for the cycles defined as $\alpha_{j}:=\pi_{j}^{a_{j}}$ and $\alpha^{\prime}_{j}:={(\pi^{\prime}_{j})}^{a^{\prime}_{j}}$, for $j=1,2,3,4$, the following path is a $(0,0)$-run:

[TABLE]

Proof.

The first two inequalities (2) enforce that the first cycle $\pi_{1}$ is repeated sufficiently many $a_{1}$ times so that $\pi_{2}$ is enabled in configuration $\textup{trg}(\rho_{1}\,\alpha_{1}\,\rho_{2})$. Then the next two inequalities (3) enforce that $\pi_{1}$ and $\pi_{2}$ are jointly repeated sufficiently many $a_{1}$, $a_{2}$ times so that $\pi_{2}$ is still enabled after its last repetition (which guarantees that every of intermediate repetitions of $\pi_{2}$ is also enabled), and that $\pi_{3}$ is enabled in configuration $\textup{trg}(\rho_{1}\,\alpha_{1}\,\rho_{2}\,\alpha_{2}\,\rho_{3})$. Likewise for (4). Finally, the inequalities (5) enforce that $\pi_{1},\ldots,\pi_{4}$ are jointly repeated sufficiently many times so that $\pi_{4}$ is still enabled after its last repetition. Analogous argument, but in the reverse order, applies for the repetitions of $\pi^{\prime}_{4},\ldots,\pi^{\prime}_{1}$. Finally, equalities (6) ensure that the total effect of $\alpha_{1},\ldots,\alpha_{4}$ is precisely compensated by the total effect of $\textup{rev}(\alpha^{\prime}_{1}),\ldots,\textup{rev}(\alpha^{\prime}_{4})$. ∎

Proof of theorem 2.

Consider a solution of $\mathcal{C}$. In particular the sum $\textup{eff}(\alpha_{1})+\ldots+\textup{eff}(\alpha_{j})$, as well as $\textup{eff}(\textup{rev}(\alpha^{\prime}_{1}))+\ldots+\textup{eff}(\textup{rev}(\alpha^{\prime}_{j}))$, is necessarily non-negative for every $j=1,\ldots,4$. Therefore, as a direct corollary of 9, for every $i\in\mathbb{N}$ the path

[TABLE]

is also a $(0,0)$-run. For bounding the lengths of cycles we use 8 and apply lemma 4 to $\mathcal{C}$, to deduce that $\mathcal{C}$ admits a non-negative integer solution of norm polynomial in $A=p(nM)^{n}$. This, together with the bounds on lengths of cycles $\pi_{1},\ldots,\pi_{4}$ and $\pi^{\prime}_{1},\ldots,\pi^{\prime}_{4}$ in the definition of $A$-thick run, entails required bounds on the lengths of the pumpable cycles. Finally, the lengths of the extremal factors $\rho_{1}$ and $\rho^{\prime}_{1}$ can be also bounded: if $\rho_{1}$ (resp. $\rho^{\prime}_{1}$) is long enough it must admit a repetition of configuration, we add one more cycle determined by the first (resp. last) such repetition, thus increasing $k$ from 8 to 10. ∎

For proving theorem 3 we will need a slightly more elaborate pumping. By the definition of thick run, both coordinates are bounded by $A$ along $\rho_{1}$ and $\rho^{\prime}_{1}$. W.l.o.g. assume that no configuration repeats in each of the two runs, and hence their lengths are bounded by $A^{2}$.

Let $\mathcal{C}_{\delta}$ denote the union of of ${\cal U}$ and ${\cal U}^{\prime}$ enhanced, this time, by the two equalities

[TABLE]

The two additional variables $\delta_{x},\delta_{y}$ describe, intuitively, possible differences between the total effect of $\pi_{1}^{a_{1}},\ldots,\pi_{4}^{a_{4}}$ and the total effect of $\textup{rev}(\pi^{\prime}_{1})^{a^{\prime}_{1}},\ldots,\textup{rev}(\pi^{\prime}_{4})^{a^{\prime}_{4}}$. The projection of any solution of $\mathcal{C}_{\delta}$ on variables $(\delta_{x},\delta_{y})$ we call below a shift.

Claim 10**.**

For some non-negative integer $m$ bounded polynomially with respect to $A$, all the four vectors $(0,m)$, $(m,0)$, $(0,-m)$ and $(-m,0)$ are shifts.

Proof.

We reason analogously as in the proof of 8, but this time we rely on the assumption that intersection of the cones $\textup{\sc SeqCone}(v_{1},v_{2},v_{3},v_{4})$ and $\textup{\sc SeqCone}(v^{\prime}_{1},v^{\prime}_{2},v^{\prime}_{3},v^{\prime}_{4})$ is non-trivial, and hence contains, for some $v\in\mathbb{Q}_{>0}^{2}$ and $a\in\mathbb{Q}_{>0}$, the points $v$ and $v+(0,a)$. By scaling we obtain an integer point $v^{\prime}\in\mathbb{N}^{2}$ and a non-negative integer $m_{1}\in\mathbb{N}$ so that $v^{\prime}$ and $v^{\prime}+(0,m_{1})$ both belong to the intersection of cones. Therefore the vector $(0,m_{1})$ is a shift. Likewise we obtain three other non-negative integers $m_{2},m_{3},m_{4}\in\mathbb{N}$ such that $(m_{2},0)$, $(0,-m_{3})$ and $(-m_{4},0)$ are all shifts. Each of the integers $m_{1},\ldots,m_{4}$ can be bounded polynomially in $A$ using lemma 4. As shifts are stable under multiplication by non-negative integers, it is enough to take as $m$ the least common multiple of the four integers. ∎

Proof of theorem 3.

We use $m$ from the last claim to modify all factors of $\tau$ except for $\rho_{1}$ and $\rho^{\prime}_{1}$, in order to reduce their lengths to at most $n\cdot m^{2}$. W.l.o.g. assume $m$ to be larger than $A$ (take a sufficient multiplicity of $m$ otherwise); this assumption allows us to proceed uniformly, irrespectively whether $v_{1}$ is positive or not. Observe that any path longer than $n\cdot m^{2}$ must contain two configurations with the same control state whose vectors are coordinate-wise congruent modulo $m$. As long as this happens, we remove the infix; note that this operation changes the effect of the whole path by a multiplicity of $m$ on every coordinate. If this operation is performed on factors $\rho_{2},\,\rho_{3},\,\rho_{4},\,\rho_{5},\,\rho^{\prime}_{5},\,\rho^{\prime}_{4},\,\rho^{\prime}_{3},\,\rho^{\prime}_{2},$ the paths $\rho,\rho^{\prime}$ are transformed into contracted paths (see the left picture in fig. 5) of the form:

[TABLE]

each of total length at most $5\,n\cdot m^{2}$. Importantly, their effects $\textup{eff}(\widetilde{\rho})$ and $\textup{eff}(\widetilde{\rho}^{\prime})$ are bounded polynomially in $A$, and their difference is (coordinate-wise) divisible by $m$:

[TABLE]

Our aim is now to pump up the cycles $\pi_{1},\ldots,\pi_{4}$ and $\textup{rev}(\pi^{\prime}_{1}),\ldots,\textup{rev}(\pi^{\prime}_{4})$ (see the right picture in fig. 5), to finally end up with the paths of the form

[TABLE]

such that $\bar{\tau}=\bar{\rho}\,\bar{\rho}^{\prime}$ is a $(0,0)$-run. In other words, we aim at $\textup{eff}(\bar{\rho})=\textup{eff}(\textup{rev}(\bar{\rho}^{\prime}))$. We are going to use Lemma 4 twice. For $j=2,\ldots,5$ let $c_{j}:=\textup{eff}(\rho_{1}\widetilde{\rho}_{2}\ldots\widetilde{\rho}_{j})\in\mathbb{Z}^{2}$, and let $f_{j}$ be the minimal non-negative vector such that the configuration $c_{j-1}+f_{j}$ enables $\widetilde{\rho}_{j}$. For $j=2,\ldots,4$ let $e_{j}\in\mathbb{N}^{2}$ be the minimal non-negative vector such that the configuration $c_{j}+e_{j}$ enables $\pi_{j}$. Finally, let $e_{5}$ be the minimal non-negative vector such that $c_{5}+e_{5}\geq(0,0)$. Analogously to the system ${\cal U}$ (2)–(5), we define the system $\widetilde{\cal U}$ of linear inequalities:

[TABLE]

In words, $\widetilde{\cal U}$ requires that every prefix of $\bar{\rho}$ is enabled in the source $(0,0)$-configuration, and that the number of repetitions of every cycle $\pi_{i}$ is divisible by $m$. Clearly $\widetilde{\cal U}$ has a non-negative integer solution, as $v_{1}$ is either positive, or vertical or horizontal in which case $v_{2}$ is positive on the relevant coordinate. Likewise we define a system of inequalities $\widetilde{\cal U}^{\prime}$ that requires that every prefix of $\textup{rev}(\bar{\rho}^{\prime})$ is enabled in the target $(0,0)$-configuration. Consider some fixed solutions of $\widetilde{\cal U}$ and $\widetilde{\cal U}^{\prime}$ bounded, by the virtue of lemma 4, polynomially in $A$. We have thus two fixed runs $\bar{\rho}$ and $\textup{rev}(\bar{\rho}^{\prime})$ of the form (7), with source vector $(0,0)$; the number of repetitions of each cycles is divisible by $m$, and the difference of their effects is (coordinate-wise) divisible by $m$:

[TABLE]

As shifts are closed under addition, by 10 we know that $(am,bm)$ is a shift. Substituting $(am,bm)$ for $(\delta_{x},\delta_{y})$ in the system $\mathcal{C}_{\delta}$ yields a system which admits, again by lemma 4, a solution bounded polynomially in $A$. We use such a solution to increase the numbers of repetitions of respective cycles $a_{1},\ldots,a_{4}$ and $a^{\prime}_{4},\ldots,a^{\prime}_{1}$ in $\bar{\rho}$ and $\bar{\rho}^{\prime}$, respectively. This turns the path $\bar{\tau}=\bar{\rho}\,\bar{\rho}^{\prime}$ into a $(0,0)$-run of length bounded polynomially in $A$. ∎

Appendix A Proof of Non-negative Cycle Lemma

In this section we prove lemma 3. Fix a 2-VASS $V$ with $n$ states, and let $M=\lVert V\rVert$. We proceed by a sequence of auxiliary lemmas.

Lemma 5**.**

Let $\rho$ be a run such that one of coordinates is smaller than $K$ in all configurations in $\rho$, and such that $\lVert\textup{trg}(\rho)\rVert>\lVert\textup{src}(\rho)\rVert+KnM$. Then

1. (i)

$\rho$* contains, as an infix, a cycle with vertical or horizontal effect,* 2. (ii)

$\rho$* contains a configuration enabling such a cycle of length polynomial in $KnM$.*

Proof.

W.l.o.g. assume that the first (horizontal) coordinate is bounded by $K$ in all configurations in $\rho$. Let $s=\textup{src}(\rho)$ and $t=\textup{trg}(\rho)$.

We first prove that $\rho$ contains a cycle with vertical effect. Define a sequence of configurations $c_{0},c_{1},\ldots,c_{m}$ as follows. Let $c_{0}$ be the first configuration which minimizes the value of the second (vertical) coordinate; clearly $c_{0}[2]\leq s[2]$. Further, let $c_{i+1}$ be the first configuration in $\rho$ such that $c_{i+1}[2]>c_{i}[2]$. Thus $c_{i+1}[2]\leq c_{i}[2]+M$, and in consequence

[TABLE]

According to the assumption we have $\lVert t\rVert>\lVert s\rVert+KnM$ hence, as the first coordinate is bounded by $K$, we deduce the inequality

[TABLE]

The two above inequalities relating $t[2]$ and $s[2]$ imply $m>Kn$. Therefore there must be two configurations $c_{i}$ and $c_{j}$, for $0\leq i<j\leq Kn$, with the same control state $q$ and the same first coordinate $c_{i}[1]=c_{j}[1]$, and thus the infix $\rho_{ij}$ of $\rho$ from $c_{i}$ to $c_{j}$ is a cycle with effect $(0,y)$, where $0<y\leq(j-i)M\leq KnM$.

Now we bound the length of the cycle. For all configurations in $\rho_{ij}$, we observe that the first coordinate stays between [math] and $K-1$, and the second coordinate stays between $c_{0}[2]$ and $c_{j}[2]$. We know that $j\leq Kn$, hence $c_{j}[2]\leq c_{0}[2]+KnM$. In consequence, the counter values in all configurations in the cycle $\rho_{ij}$ are restricted to at most $K(KnM+1)$ different vectors, and therefore there are at most $L=Kn(KnM+1)$ different configurations in $\rho_{ij}$. By removing repetitions of configurations, i.e., by removing cycles of effect $(0,0)$, we reduce the length of the cycle to at most $L$, which is bounded polynomially in $KnM$. ∎

Every 2-VASS $V$ induces a directed graph whose vertices are control states of $V$, with an edge from $p$ to $q$ if and only if $V$ has a transition of the form $(p,v,q)$. This graph allows us to split control states of $V$ into strongly connected components, which we call briefly sccs. The following lemma distinguishes two kinds of sccs:

Lemma 6**.**

Every scc $S$ satisfies one of the following conditions:

1. (a)

every control state in $S$ belongs to some positive cycle of length polynomial in $nM$; 2. (b)

the effects of all cycles in $S$ belong to some half-plane containing no positive vector.

Proof.

Let $U$ be the set of effects of simple cycles included in $S$. We consider two cases:

Case 1: $\textup{\sc Cone}(U)$ contains a positive vector.

Fix an arbitrary positive vector $v\in\textup{\sc Cone}(U)$. By Caratheodory’s Theorem, $v=a_{1}u_{1}+a_{2}u_{2}\in\textup{\sc Cone}(u_{1},u_{2})$ for some two vectors $u_{1},u_{2}\in U$ and $a_{1},a_{2}\in\mathbb{N}$. By lemma 4 we know that $a_{1}u_{1}+a_{2}u_{2}$ is positive for some non-negative integers $\alpha_{1},\alpha_{2}\leq(2M)^{2}$. We also know that $u_{1}$ is the effect of a simple cycle $\pi_{1}$ from, say, state $q_{1}$ to $q_{1}$; and $u_{2}$ is the effect of a simple cycle $\pi_{2}$ from state $q_{2}$ to $q_{2}$.

Fix a state $q\in S$. As $S$ is strongly connected it contains a cycle $\pi$ of length at most $3n$ which contains all $q$, $q_{1}$ and $q_{2}$. Thus absolute values of $\textup{eff}(\pi)$ on both coordinates are at most $3nM$, hence are larger or equal than $-3nM$. Therefore $\pi$, together with cycle $\pi_{1}$ repeated $a_{1}\cdot(3nM+1)$ times, and with cycle $\pi_{2}$ repeated $a_{2}\cdot(3nM+1)$ times, form a cycle with positive effect. The length of this cycle is at most $3n+2n(2M)^{2}(3nM+1)$, hence bounded polynomially in $nM$. Condition (a) holds.

Case 2: $\textup{\sc Cone}(U)$ contains no positive vector.

By lemma 1 we deduce that $\textup{\sc Cone}(U)$ is included in some half-plane $\Pi$. If $\Pi$ intersects the positive orthant $\mathbb{Q}_{>0}^{2}$, rotate the half-plane so that it is disjoint from $\mathbb{Q}_{>0}^{2}$. The so obtained half-plane $\Pi^{\prime}$ contains no positive vector and still includes $\textup{\sc Cone}(U)$, hence condition (b) holds. ∎

Lemma 7**.**

There is a polynomial $Q$ such that every run $\rho$ within one scc with $\lVert\textup{trg}(\rho)\rVert>Q(nM)\cdot(\lVert\textup{src}(\rho)\rVert+1)$ contains a configuration enabling a semi-positive cycle of length at most $Q(nM)$.

Proof.

Let $Q_{1}$ and $Q_{2}$ be the polynomials from lemma 6(ii) and lemma 5(a), respectively. Let $s=\textup{src}(\rho)$ and $t=\textup{trg}(\rho)$, and let $S$ be the scc containg $\rho$. We split the proof according to the two cases (a) and (b) of lemma 6. The proof goes through for every polynomial $Q$ satisfying the following two inequalities:

[TABLE]

Case 1: $S$ satisfies (a).

If $\rho$ visits some configuration with both coordinates at least $Q_{2}(nM)\cdot M=K$ then this configuration necessarily enables a positive cycle of length bounded by $Q_{2}(nM)\leq Q(nM)$. Otherwise, we know that in every configuration in $\rho$ one of coordinates is smaller than $K$. W.l.o.g. assume $t[1]<K$. Let $\rho^{\prime}$ be the longest suffix of $\rho$ such that the first coordinate is bounded by $K-1$ along $\rho^{\prime}$, and let $s^{\prime}=\textup{src}(\rho^{\prime})$. We claim that $\lVert s^{\prime}\rVert\leq\lVert s\rVert+K-1+M$; indeed, if $s^{\prime}\neq s$, the first coordinate of the configuration $u$ preceding $s^{\prime}$ in $\rho$ is at least $K$, and therefore $u[2]\leq K-1$, which implies that $s^{\prime}[2]\leq K-1+M$.

By assumption we know that $\lVert t\rVert>Q(nM)\cdot(\lVert s\rVert+1)$, and hence necessarily $\lVert t\rVert>\lVert s^{\prime}\rVert+KnM$. We can thus apply lemma 5(ii) to $\rho^{\prime}$, to learn that some configuration in $\rho^{\prime}$ enables a vertical cycle of length at most $Q_{1}(KnM)\leq Q(nM)$.

Case 2: $S$ satisfies (b).

Denoting by $U$ the set of all simple cycles in $S$, due to condition (b) we know that $\textup{\sc Cone}(U)$ is included in some half-plane $\Pi=\measuredangle[-w,w]$, where $-w\in\mathbb{N}\times(-\mathbb{N})$ and $w\in(-\mathbb{N})\times\mathbb{N}$. We aim at showing the following claim:

Claim 11**.**

$U$* contains a vertical or horizontal cycle.*

Towards contradiction suppose $U$ contains no vertical nor horizontal cycle. Whenever a vector $p=(-x,y)\in(-\mathbb{N})\times\mathbb{N}$, for $y>x>0$, is the effect of a simple cycle, its ratio $y/x$ is necessarily bounded by $nM$. Therefore, the vector $w$ determining $\Pi$ can be assumed to have ratio bounded by $nM$ as well. Note that all cycles contained as an infix in $\rho$, necessarily belong to $\Pi$. We are going to show bounds on $t[1]$ and $t[2]$ which contradict the assumption on $\lVert t\rVert$.

Factor the run $\rho$ into a at most $n$ (not necessarily simple) cycles, interleaved with at most $n-1$ remaining transitions. Thus we have $t=s+r+p$, where $p\in\Pi$ is the total effect of the cycles and $r$ is the total effect of at most $n-1$ transitions. Let $p^{\prime}$ denote the total effect of those among the cycles whose vertical effect is non-negative (and hence horizontal effect is forcedly negative). Thus

[TABLE]

As the half-plane $\Pi=\measuredangle[-w,w]$ contains all these cycles, and the ratio of $w$ is bounded by $nM$ as discussed above, we know that ratio of $p^{\prime}$ is also bounded by $nM$. In consequence $p^{\prime}[2]\ \leq\ -p^{\prime}[1]\ \leq\ (s+r)[1]\cdot nM$, and hence

[TABLE]

As the same bound is obtained symmetrically for $t[1]$, we have arrived at a contradiction with the assumption $\lVert t\rVert>Q(nM)\cdot(\lVert s\rVert+1)$. 11 is thus proved.

Claim 12**.**

The run $\rho$ contains, as an infix, a vertical or horizontal cycle $\pi$.

W.l.o.g. supose $U$ contains a vertical cycle. In consequence, no cycle in $S$ has positive first (horizontal) coordinate. Therefore the horizontal coordinate is smaller than $K=s[1]+(n-1)M+1$ in all configurations in $\rho$. By lemma 5(i) $\rho$ contains, as an infix, a vertical cycle.

Relying on the 12, w.l.o.g. assume $\rho$ contains a vertical cycle $\pi$ as infix. For completing the proof of lemma 7 we need to bound the length of $\pi$. As $S$ satisfies condition (b), it contains no cycle with positive horizontal effect; in consequence, decomposition of $\pi$ into simple cycles uses only cycles with effect $(0,a)$, where $a\in\mathbb{Z}$. Split these simple cycles into increasing ($a>0$) and non-increasing ($a\leq 0$). Suppose the length of $\pi=\pi_{0}$ is greater than $n$ and consider the first simple cycle $\sigma_{1}$ contained as its infix. If $\sigma_{1}$ is non-increasing remove $\sigma_{1}$ from $\pi$, thus obtaining the path $\pi_{1}$, and consider the first simple cycle $\sigma_{2}$ contained in $\pi_{1}$ as an infix. Again, remove $\sigma_{2}$ if it is non-increasing. And so on, continue this process until finally certain cycle $\sigma_{i}$ in $\pi_{i-1}$ is increasing. As all the removed simple cycles $\sigma_{1},\ldots,\sigma_{i-1}$ were non-increasing, inserting back to $\pi_{i-1}$ those of them which preceed $\sigma_{i}$ necessarily increases the configuration $\textup{src}(\sigma_{i})$ in $\pi_{i-1}$ so that it enables $\sigma$. The proof is thus completed.

∎

Proof of lemma 3.

Let $Q$ be the polynomial from lemma 7. We define a polynomial $P(x)=Q(x)\cdot(x+1)$. Consider a run $\rho$ from a $(0,0)$-configuration to some target configuration $t$. Let $k\leq n$ be the number of sccs traversed by the run $\rho$ and, for $i=1,\ldots,k$, let $s_{i}$ and $t_{i}$ be the first and the last configuration in the $i$-th scc, respectively. Then $s_{1}=(0,0)$ and $t_{k}=t$. Suppose, towards contradiction, that $\rho$ contains no configuration enabling a semi-positive cycle of length at most $P(nM)$. As $Q(nM)\leq P(nM)$, by lemma 7 we obtain

[TABLE]

for $i=1,\ldots,k$. We show by induction on $i$ that $\lVert t_{i}\rVert\leq P(nM)^{i}$. For $i=1$ we use (8) and the equality $\lVert s_{1}\rVert=0$, to obtain $\lVert t_{1}\rVert\leq Q(nM)\leq P(nM)$. For the induction step we use (8) and the inequality $\lVert s_{i+1}\rVert\leq\lVert t_{i}\rVert+M$, to obtain:

[TABLE]

as required. Thus $\lVert t\rVert\leq P(nM)^{n}$ which contradicts the assumption on $\lVert t\rVert$ and therefore completes the proof. ∎

Appendix B Missing proof from section 4 – the case of thin run

As usual we use $n=|Q|$ for the number of control states, and $M=\lVert V\rVert$ for the norm of $V$. Assume a $(0,0)$-run $\tau$ to be $A$-thin: every configuration in $\tau$ lies in some $A$-belt $\mathcal{B}_{v,W}$. Fix $W=A+\sqrt{2}M$ and $B=6WA^{2}+3W$, and let $S=[0,B]^{2}$. Let $\lVert v\rVert_{2}$ denote the Euclidean norm of $v$. Note that $\lVert v\rVert_{2}\leq\sqrt{2}\lVert v\rVert$.

Claim 13**.**

The run $\tau$ does not change belts outside of $S$, i.e., any two consecutive configurations $(q,w)$, $(q^{\prime},w^{\prime})$ in $\tau$ satisfying $w,w^{\prime}\notin S$ share a common belt.

Proof.

Assume that $w\in{\cal B}_{u,A}$ for some $u$ ($\lVert u\rVert\leq A$). We will show $w^{\prime}\in{\cal B}_{u,A}$. Notice that $w^{\prime}\in{\cal B}_{u,W}$ (since $\lVert w^{\prime}-w\rVert_{2}\leq\sqrt{2}\lVert w^{\prime}-w\rVert\leq\sqrt{2}M$). Towards contradiction assume that $v^{\prime}$ also belongs to some $A$-belt ${\cal B}_{v,A}\neq{\cal B}_{u,A}$ (i.e. $v$ and $u$ non-colinear). Then of course $w^{\prime}\in{\cal B}_{v,W}$ too. We will show that this implies $w^{\prime}\in S$.

W.l.o.g. assume that $u\circlearrowright v$. Let $I=(1,1)$. Notice that when $u\circlearrowright I\circlearrowright v$ then $w^{\prime}$ also belongs to ${\cal B}_{I,W}$. Thus we can assume that $u\circlearrowright v\circlearrowright I$ or $I\circlearrowright u\circlearrowright v$. W.l.o.g. let us choose the first option. Note that this implies that $u[2],v[2]>0$.

Let $p_{u}$ and $p_{v}$ be the intersection points of $\ell_{u}$ and $\ell_{v}$ with the horizontal line $\ell:y=w^{\prime}[2]$. Their horizontal coordinates are $\frac{u[1]}{u[2]}\cdot w^{\prime}[2]$ and $\frac{v[1]}{v[2]}\cdot w^{\prime}[2]$, respectively, so

[TABLE]

Because the belts intersect with $\ell$ at an angle between $45^{\circ}$ and $90^{\circ}$, the line segments ${\cal B}_{u,W}\cap\ell$ and ${\cal B}_{v,W}\cap\ell$ are of length $\leq 2\sqrt{2}W<3W$. Thus $\lVert p_{u}-p_{v}\rVert\leq\lVert p_{u}-w^{\prime}\rVert+\lVert p_{v}-w^{\prime}\rVert<6W$. Consequently:

[TABLE]

Furthermore $p_{v}[1]<p_{v}[2]=w^{\prime}[2]$ and $\lVert p_{v}-w^{\prime}\rVert<3W$ so $w^{\prime}[1]<B$ too, contradiction. ∎

Claim 14**.**

Let $C=(A^{2}\cdot n)^{2}$. If $\tau$ visits a configuration of norm larger than $D=B+C\cdot A$, then it decomposes into $\tau=\tau_{0}\,\alpha_{1}\,\tau_{1}\,\alpha_{2}\,\tau_{2},$ for two cycles $\alpha_{1},\alpha_{2}$ of opposite effects $\textup{eff}(\alpha_{1})=-\textup{eff}(\alpha_{2})\geq(0,0)$ containing jointly at most $C(C+1)$ different configurations.

Proof.

For a configuration $c$ of norm larger than $D$, let us decompose $\tau$ into

[TABLE]

such that $\textup{trg}(\gamma)=c=\textup{src}(\gamma^{\prime})$ and $\gamma\gamma^{\prime}$ is a maximal infix of $\pi$ that visits only configurations of norm greater than $B$. By 13, there exists unique belt $\mathcal{B}={\cal B}_{u,A}$ that contains $\gamma\gamma^{\prime}$. Assume w.l.o.g. that $\lVert u\rVert>M$. Let us divide $\mathcal{B}\setminus S$ into segments $\mathcal{B}_{i}$ as follows:

[TABLE]

Observe that $\gamma\gamma^{\prime}$ visits more than $C$ initial blocks $\mathcal{B}_{i}$ starting from $\mathcal{B}_{0}$ up to $\mathcal{B}_{C}$, since a single transition cannot ‘jump’ over a block without visiting it. Let $c_{i}=(q_{i},v_{i})$ be the first configuration in $\gamma$ beloging to $\mathcal{B}_{i}$, and symmetrically let $c^{\prime}_{i}=(q^{\prime}_{i},v^{\prime}_{i})$ be the last configuration in $\gamma^{\prime}$ beloging to $\mathcal{B}_{i}$. Observe that each block $\mathcal{B}_{i}$ has the same shape as $\mathcal{B}_{0}$ and differs only by translation by $iu$. Furthermore, as $\lVert u\rVert\leq A$, each $\mathcal{B}_{i}$ fits inside a square of size $A$ so it contains at most $A^{2}$ points. By the pigeonhole principle, there are at least two $i,j$ ($0\leq i<i+d=j\leq C$) such that

[TABLE]

Taking as $\alpha_{1}$ the infix from $c_{i}$ to $c_{j}$, and as $\alpha_{2}$ the infix from $c^{\prime}_{j}$ to $c^{\prime}_{i}$, we obtain two required cycles. ∎

Claim 15**.**

Under assumption of 14, $\tau$ decomposes into $\tau=\tau_{0}\,\alpha_{1}\,\tau_{1}\,\alpha_{2}\,\tau_{2}$ so that $\tau_{0}\,\tau_{1}\,\tau_{2}$ is also an $A$-thin $(0,0)$-run.

Proof.

The same proof as for 14, with one modification: take as $c_{i}$ the last configuration in $\gamma$ belonging to $\mathcal{B}_{i}$, and symmetrically take as $c^{\prime}_{i}$ the first configuration in $\gamma^{\prime}$ belonging to $\mathcal{B}_{i}$. ∎

Proof of theorem 2.

Applying 14 simultaneously to the first belt in which the norm $D$ is exceeded, and to the very last such belt, we get $(0,0)$-runs

[TABLE]

for $i\in\mathbb{N}$, where cycles $\alpha_{1},\alpha_{2}$ belong to the first belt and cycles $\alpha_{3},\alpha_{4}$ belong to the last one. The lengths of the cycles can be reduced to at most $C(C+1)$ by removing repetitions of configurations. Then the length of the very first factor $\tau_{0}$ can be bounded by $(D+1)^{2}+C(C+1)$ by replacing, if needed, cycles $\alpha_{1},\alpha_{2}$ with the first cycle of effect $(0,0)$ in $\tau_{0}$. Likewise for the very last factor $\tau_{4}$. ∎

Proof of theorem 3.

Immeediate using 15, according to which every $A$-thin $(0,0)$-run exceeding norm $D$ can be shortened. Once all configurations along a run have norm bounded by $D$, by eliminating repetitions of configurations we arrive at a run of length at most $n\cdot(D+1)^{2}$. ∎