The Polynomial Complexity of Vector Addition Systems with States

TL;DR

This paper characterizes the asymptotic computational complexity of vector addition systems with states, showing it is either polynomial with a computable degree or exponential, and provides methods to determine this degree efficiently.

Contribution

It establishes a precise complexity classification for vector addition systems with states, including a polynomial-time method to compute the degree of polynomial complexity.

Findings

Complexity is either polynomial with a computable degree or exponential.

The degree of polynomial complexity can be computed in polynomial time.

The degree k satisfies 1 ≤ k ≤ 2^n, where n is the system's dimension.

Abstract

Vector addition systems are an important model in theoretical computer science and have been used in a variety of areas. In this paper, we consider vector addition systems with states over a parameterized initial configuration. For these systems, we are interested in the standard notion of computational complexity, i.e., we want to understand the length of the longest trace for a fixed vector addition system with states depending on the size of the initial configuration. We show that the asymptotic complexity of a given vector addition system with states is either $\Theta(N^k)$ for some computable integer $k$, where $N$ is the size of the initial configuration, or at least exponential. We further show that $k$ can be computed in polynomial time in the size of the considered vector addition system. Finally, we show that $1 \le k \le 2^n$, where $n$ is the dimension of the considered vector addition system.

Equations

$$D\mu$$

$$\mu$$

$$F\mu$$

$$r$$

$$z$$

$$D^{T}r+F^{T}z$$

$$D_{\mathit{ext}}((x,\eta),t):=\left\{\begin{array}[]{cc}D(x,t),&\text{if }t\in\mathit{Trns}(\mathtt{VASS}(\eta)),\\ 0,&\text{otherwise}.\\ \end{array}\right.$$

$$D_{ext}\mu$$

$$\mu$$

$$F{|}_U\mu$$

$$r$$

$$z$$

$$D_{ext}^{T}r+F{|}_U^{T}z$$

$${\mathtt{tbound}}_t(N)\le \underset{(s,\nu )\in Cfg(\mathcal{V}),\Vert \nu \Vert \le N}{\max }w(s,\nu )+\sum _{t^{\prime }\in Trns(\mathcal{V})\setminus U}{\mathtt{tbound}}_{t^{\prime }}(N)\cdot {\mathtt{inc}}_{t^{\prime }}(N).$$

$${\mathtt{vbound}}_x(N)\le \underset{(s,\nu )\in Cfg(\mathcal{V}),\Vert \nu \Vert \le N}{\max }w(s,\nu )+\sum _{t^{\prime }\in Trns(\mathcal{V})\setminus U}{\mathtt{tbound}}_{t^{\prime }}(N)\cdot {\mathtt{inc}}_{t^{\prime }}(N).$$

$$\mathtt{ext}_{s}(\nu)(x,\eta)=\left\{\begin{array}[]{cc}\nu(x),&\text{if }s\in\mathit{St}(\mathtt{VASS}(\eta)),\\ 0,&\text{otherwise.}\\ \end{array}\right.$$

$$w(s,\nu )=rank(r,z)(s,{\mathtt{ext}}_s(\nu ))\text{ for all }(s,\nu )\in Cfg(\mathcal{V}).$$

$$D\mu$$

$$\mu$$

$$F\mu$$

$$\mu (t)$$

$$r$$

$$z$$

$$D^{T}r+F^{T}z$$

$$\left(\begin{array}{c}D\\ \mathbf{Id}\end{array}\right)\mu$$

$$F\mu$$

$$\left(\begin{array}{c}r\\ y\end{array}\right)$$

$${\left(\begin{array}{c}D\\ \mathbf{Id}\end{array}\right)}^T\left(\begin{array}{c}r\\ y\end{array}\right)+F^{T}z$$

$${\left(\begin{array}{c}0\\ {\mathtt{char}}_t\end{array}\right)}^T\left(\begin{array}{c}r\\ y\end{array}\right)+0^{T}z$$

$$r$$

$$y$$

$$D^{T}r+y+F^{T}z$$

$$y(t)$$

$$D\mu$$

$$\mu$$

$$F\mu$$

$$r$$

$$z$$

$$D^{T}r+F^{T}z$$

$$r(x)$$

$$\left(\begin{array}{c}D\\ \mathbf{Id}\end{array}\right)\mu$$

$$F\mu$$

$$\left(\begin{array}{c}r\\ y\end{array}\right)$$

Full text

1 Introduction

Vector addition systems (VASs) [13], which are equivalent to Petri nets, are a popular model for the analysis of parallel processes [7]. Vector addition systems with states (VASSs) [10] are an extension of VASs with a finite control and are a popular model for the analysis of concurrent systems, because the finite control can for example be used to model shared global memory [12]. In this paper, we consider VASSs over a parameterized initial configuration. For these systems, we are interested in the standard notion of computational time complexity, i.e., we want to understand the length of the longest execution for a fixed VASS depending on the size of the initial configuration. VASSs over a parameterized initial configuration naturally arise in two areas:

1. The parameterized verification problem. For concurrent systems the number of system processes is often not known in advance, and thus the system is designed such that a template process can be instantiated an arbitrary number of times. The problem of analyzing the concurrent system for all possible system sizes is a common theme in the literature [9, 8, 1, 11, 4, 2, 3].
2. Automated complexity analysis of programs. VASSs (and generalizations) have been used as backend in program analysis tools for automated complexity analysis [18, 19, 20]. The VASS considered by these tools are naturally parameterized over the initial configuration, modelling the dependency of the program complexity on the program input. The cited papers have proposed practical techniques but did not give complete algorithms.

Two recent papers have considered the computational time complexity of VASSs over a parameterized initial configuration. [15] presents a PTIME procedure for deciding whether a VASS is polynomial or at least exponential, but does not give a precise analysis in case of polynomial complexity. [5] establishes the precise asymptotic complexity for the special case of VASSs whose configurations are linearly bounded in the size of the initial configuration. In this paper, we generalize both results and fully characterize the asymptotic behaviour of VASSs with polynomial complexity: We show that the asymptotic complexity of a given VASS is either $\Theta(N^{k})$ for some computable integer $k$, where $N$ is the size of the initial configuration, or at least exponential. We further show that $k$ can be computed in PTIME in the size of the considered VASS. Finally, we show that $1\leq k\leq 2^{n}$, where $n$ is the dimension of the considered VASS.

1.1 Overview and Illustration of Results

We discuss our approach on the VASS $\mathcal{V}_{\mathit{run}}$, stated in Figure 1, which will serve as running example. The VASS has dimension $3$ (i.e., the vectors annotating the transitions have dimension $3$) and four states $s_{1},s_{2},s_{3},s_{4}$. In this paper we will always represent vectors using a set of variables $\mathit{Var}$, whose cardinality equals the dimension of the VASS. For $\mathcal{V}_{\mathit{run}}$ we choose $\mathit{Var}=\{x,y,z\}$ and use $x,y,z$ as indices for the first, second and third component of 3-dimensional vectors. The configurations of a VASS are pairs of states and valuations of the variables to non-negative integers. A step of a VASS moves along a transition from the current state to a successor state, and adds the vector labelling the transition to the current valuation; a step can only be taken if the resulting valuation is non-negative. For the computational time complexity analysis of VASSs, we consider traces (sequences of steps) whose initial configurations consist of a valuation whose maximal value is bounded by $N$ (the parameter used for bounding the size of the initial configuration). The computational time complexity is then the length of the longest trace whose initial configuration is bounded by $N$. For ease of exposition, we will in this paper only consider VASSs whose control-flow graph is connected. (For the general case, we remark that one needs to decompose a VASS into its strongly-connected components (SCCs), which can then be analyzed in isolation, following the DAG-order of the SCC decomposition; for this, one slightly needs to generalize the analysis in this paper to initial configurations with values $\Theta(N^{k_{x}})$ for every variable $x\in\mathit{Var}$, where $k_{x}\in\mathbb{Z}$.) For ease of exposition, we further consider traces over arbitrary initial states (instead of some fixed initial state); this is justified because for a fixed initial state one can always restrict the control-flow graph to the reachable states, and then the two options result in the same notion of computational complexity (up to a constant offset, which is not relevant for our asymptotic analysis).

In order to analyze the computational time complexity of a considered VASS, our approach computes variable bounds and transition bounds. A variable bound is the maximal value of a variable reachable by any trace whose initial configuration is bounded by $N$. A transition bound is the maximal number of times a transition appears in any trace whose initial configuration is bounded by $N$. For $\mathcal{V}_{\mathit{run}}$, our approach establishes the linear variable bound $\Theta(N)$ for $x$ and $y$, and the quadratic bound $\Theta(N^{2})$ for $z$. We note that because the variable bound of $z$ is quadratic and not linear, $\mathcal{V}_{\mathit{run}}$ cannot be analyzed by the procedure of [5]. Our approach establishes the bound $\Theta(N)$ for the transitions $s_{1}\rightarrow s_{3}$ and $s_{4}\rightarrow s_{2}$, the bound $\Theta(N^{2})$ for transitions $s_{1}\rightarrow s_{2}$, $s_{2}\rightarrow s_{1}$, $s_{3}\rightarrow s_{4}$, $s_{4}\rightarrow s_{3}$, and the bound $\Theta(N^{3})$ for all self-loops. The computational complexity of $\mathcal{V}_{\mathit{run}}$ is then the maximum of all transition bounds, i.e., $\Theta(N^{3})$. In general, our main algorithm (Algorithm 1 presented in Section 4) either establishes that the VASS under analysis has at least exponential complexity or computes asymptotically precise variable and transition bounds $\Theta(N^{k})$, with $k$ computable in PTIME and $1\leq k\leq 2^{n}$, where $n$ is the dimension of the considered VASS. We note that our upper bound $2^{n}$ also improves the analysis of [15], which reports an exponential dependence on the number of transitions (and not only on the dimension).

We further state a family $\mathcal{V}_{n}$ of VASSs, which illustrate that $k$ can indeed be exponential in the dimension (the example can be skipped on first reading). $\mathcal{V}_{n}$ uses variables $x_{i,j}$ and consists of states $s_{i,j}$, for $1\leq i\leq n$ and $j=1,2$. We note that $\mathcal{V}_{n}$ has dimension $2n$. $\mathcal{V}_{n}$ consists of the transitions

• •

$s_{i,1}\xrightarrow{d}s_{i,2}$, for $1\leq i\leq n$, with $d(x_{i,1})=-1$ and $d(x)=0$ for all $x\neq x_{i,1}$,

• •

$s_{i,2}\xrightarrow{d}s_{i,1}$, for $1\leq i\leq n$, with $d(x)=0$ for all $x$,

• •

$s_{i,1}\xrightarrow{d}s_{i,1}$, for $1\leq i\leq n$, with $d(x_{i,1})=-1$, $d(x_{i,2})=1$, $d(x_{i+1,1})=d(x_{i+1,2})=1$ in case $i<n$, and $d(x)=0$ for all other $x$,

• •

$s_{i,2}\xrightarrow{d}s_{i,2}$, for $1\leq i\leq n$, with $d(x_{i,1})=1$, $d(x_{i,2})=-1$, and $d(x)=0$ for all other $x$,

• •

$s_{i,1}\xrightarrow{d}s_{i+1,1}$, for $1\leq i<n$, with $d(x_{i,1})=-1$ and $d(x)=0$ for all $x\neq x_{i,1}$,

• •

$s_{i+1,2}\xrightarrow{d}s_{i,2}$, for $1\leq i<n$, with $d(x)=0$ for all $x$.

$\mathcal{V}_{\mathit{exp}}$ in Figure 1 depicts $\mathcal{V}_{n}$ for $n=3$, where the vector components are stated in the order $x_{1,1},x_{1,2},x_{2,1},x_{2,2},x_{3,1},x_{3,2}$. It is not hard to verify for all $1\leq i\leq n$ that $\Theta(N^{2^{i-1}})$ is the precise asymptotic variable bound for $x_{i,1}$ and $x_{i,2}$, that $s_{i,1}\rightarrow s_{i,2}$, $s_{i,2}\rightarrow s_{i,1}$ and $s_{i,1}\rightarrow s_{i+1,1}$, $s_{i+1,2}\rightarrow s_{i,2}$ in case $i<n$, and that $\Theta(N^{2^{i}})$ is the precise asymptotic transition bound for $s_{i,1}\rightarrow s_{i,1}$, $s_{i,2}\rightarrow s_{i,2}$ (Algorithm 1 can be used to find these bounds).

1.2 Related Work

A celebrated result on VASs is the EXPSPACE-completeness [16, 17] of the boundedness problem. Deciding termination for a VAS with a fixed initial configuration can be reduced to the boundedness problem, and is therefore also EXPSPACE-complete; this also applies to VASSs, whose termination problem can be reduced to the VAS termination problem. In contrast, deciding the termination of VASSs for all initial configurations is in PTIME. It is not hard to see that non-termination over all initial configurations is equivalent to the existence of non-negative cycles (e.g., using Dickson’s Lemma [6]). Kosaraju and Sullivan have given a PTIME procedure for the detection of zero-cycles [14], which can be easily be adapted to non-negative cycles. The existence of zero-cycles is decided by the repeated use of a constraint system in order to remove transitions that can definitely not be part of a zero-cycle. The algorithm of Kosaraju and Sullivan forms the basis for both cited papers [15, 5], as well as the present paper.

A line of work [18, 19, 20] has used VASSs (and their generalizations) as backends for the automated complexity analysis of C programs. These algorithms have been designed for practical applicability, but are not complete and no theoretical analysis of their precision has been given. We point out, however, that these papers have inspired the Bound Proof Principle in Section 5.

2 Preliminaries

Basic Notation.

For a set $X$ we denote by $|X|$ the number of elements of $X$. Let $\mathbb{S}$ be either $\mathbb{N}$ or $\mathbb{Z}$. We write $\mathbb{S}^{I}$ for the set of vectors over $\mathbb{S}$ indexed by some set $I$. We write $\mathbb{S}^{I\times J}$ for the set of matrices over $\mathbb{S}$ indexed by $I$ and $J$. We write $\mathbf{1}$ for the vector which has entry $1$ in every component. Given $a\in\mathbb{S}^{I}$, we write $a(i)\in\mathbb{S}$ for the entry at line $i\in I$ of $a$, and $\left\lVert a\right\rVert=\max_{i\in I}|a(i)|$ for the maximum absolute value of $a$. Given $a\in\mathbb{S}^{I}$ and $J\subseteq I$, we denote by $a|_{J}\in\mathbb{S}^{J}$ the restriction of $a$ to $J$, i.e., we set $a|_{J}(i)=a(i)$ for all $i\in J$. Given $A\in\mathbb{S}^{I\times J}$, we write $A(j)$ for the vector in column $j\in J$ of $A$ and $A(i,j)\in\mathbb{S}$ for the entry in column $i\in I$ and row $j\in J$ of $A$. Given $A\in\mathbb{S}^{I\times J}$ and $K\subseteq J$, we denote by $A|_{K}\in\mathbb{S}^{I\times K}$ the restriction of $A$ to $K$, i.e., we set $A|_{K}(i,j)=A(i,j)$ for all $(i,j)\in I\times K$. We write $\mathbf{Id}$ for the square matrix which has entries $1$ on the diagonal and [math] otherwise. Given $a,b\in\mathbb{S}^{I}$ we write $a+b\in\mathbb{S}^{I}$ for component-wise addition, $c\cdot a\in\mathbb{S}^{I}$ for multiplying every component of $a$ by some $c\in\mathbb{S}$ and $a\geq b$ for component-wise comparison. Given $A\in\mathbb{S}^{I\times J}$, $B\in\mathbb{S}^{J\times K}$ and $x\in\mathbb{S}^{J}$, we write $AB\in\mathbb{S}^{I\times K}$ for the standard matrix multiplication, $Ax\in\mathbb{S}^{I}$ for the standard matrix-vector multiplication, $A^{T}\in\mathbb{S}^{J\times I}$ for the transposed matrix of $A$ and $x^{T}\in\mathbb{S}^{1\times J}$ for the transposed vector of $x$.

Vector Addition System with States (VASS).

Let $\mathit{Var}$ be a finite set of variables. A vector addition system with states (VASS) $\mathcal{V}=(\mathit{St}(\mathcal{V}),\mathit{Trns}(\mathcal{V}))$ consists of a finite set of states $\mathit{St}(\mathcal{V})$ and a finite set of transitions $\mathit{Trns}(\mathcal{V})$, where $\mathit{Trns}(\mathcal{V})\subseteq\mathit{St}(\mathcal{V})\times\mathbb{Z}^{\mathit{Var}}\times\mathit{St}(\mathcal{V})$; we call $n=|\mathit{Var}|$ the dimension of $\mathcal{V}$. We write $s_{1}\xrightarrow{d}s_{2}$ to denote a transition $(s_{1},d,s_{2})\in\mathit{Trns}(\mathcal{V})$; we call the vector $d$ the update of transition $s_{1}\xrightarrow{d}s_{2}$. A path $\pi$ of $\mathcal{V}$ is a finite sequence $s_{0}\xrightarrow{d_{1}}s_{1}\xrightarrow{d_{2}}\cdots s_{k}$ with $s_{i}\xrightarrow{d_{i+1}}s_{i+1}\in\mathit{Trns}(\mathcal{V})$ for all $0\leq i<k$. We define the length of $\pi$ by $\mathit{length}(\pi)=k$ and the value of $\pi$ by $\mathit{val}(\pi)=\sum_{i\in[1,k]}d_{i}$. Let $\mathtt{instance}(\pi,t)$ be the number of times $\pi$ contains the transition $t$, i.e., the number of indices $i$ such that $t=s_{i}\xrightarrow{d_{i}}s_{i+1}$. We remark that $\mathit{length}(\pi)=\sum_{t\in\mathit{Trns}(\mathcal{V})}\mathtt{instance}(\pi,t)$ for every path $\pi$ of $\mathcal{V}$. Given a finite path $\pi_{1}$ and a path $\pi_{2}$ such that the last state of $\pi_{1}$ equals the first state of $\pi_{2}$, we write $\pi=\pi_{1}\pi_{2}$ for the path obtained by joining the last state of $\pi_{1}$ with the first state of $\pi_{2}$; we call $\pi$ the concatenation of $\pi_{1}$ and $\pi_{2}$, and $\pi_{1}\pi_{2}$ a decomposition of $\pi$. We say $\pi^{\prime}$ is a sub-path of $\pi$, if there is a decomposition $\pi=\pi_{1}\pi^{\prime}\pi_{2}$ for some $\pi_{1},\pi_{2}$. A cycle is a path that has the same start- and end-state. A multi-cycle is a finite set of cycles. The value $\mathit{val}(M)$ of a multi-cycle $M$ is the sum of the values of its cycles. $\mathcal{V}$ is connected, if for all $s,s^{\prime}\in\mathit{St}(\mathcal{V})$ there is a path from $s$ to $s^{\prime}$. VASS $\mathcal{V}^{\prime}$ is a sub-VASS of $\mathcal{V}$, if $\mathit{St}(\mathcal{V}^{\prime})\subseteq\mathit{St}(\mathcal{V})$ and $\mathit{Trns}(\mathcal{V}^{\prime})\subseteq\mathit{Trns}(\mathcal{V})$. Sub-VASSs $\mathcal{V}_{1}$ and $\mathcal{V}_{2}$ are disjoint, if $\mathit{St}(\mathcal{V}_{1})\cap\mathit{St}(\mathcal{V}_{2})=\emptyset$. A strongly-connected component (SCC) of a VASS $\mathcal{V}$ is a maximal sub-VASS $S$ of $\mathcal{V}$ such that $S$ is connected and $\mathit{Trns}(S)\neq\emptyset$.

Let $\mathcal{V}$ be a VASS. The set of valuations $\mathit{Val}(\mathcal{V})=\mathbb{N}^{\mathit{Var}}$ consists of $\mathit{Var}$-vectors over the natural numbers (we assume $\mathbb{N}$ includes [math]). The set of configurations $\mathit{Cfg}(\mathcal{V})=\mathit{St}(\mathcal{V})\times\mathit{Val}(\mathcal{V})$ consists of pairs of states and valuations. A step is a triple $((s_{1},\nu_{1}),d,(s_{2},\nu_{2}))\in\mathit{Cfg}(\mathcal{V})\times\mathbb{Z}^{\mathit{dim}(\mathcal{V})}\times\mathit{Cfg}(\mathcal{V})$ such that $\nu_{2}=\nu_{1}+d$ and $s_{1}\xrightarrow{d}s_{2}\in\mathit{Trns}(\mathcal{V})$. We write $(s_{1},\nu_{1})\xrightarrow{d}(s_{2},\nu_{2})$ to denote a step $((s_{1},\nu_{1}),d,(s_{2},\nu_{2}))$ of $\mathcal{V}$. A trace of $\mathcal{V}$ is a finite sequence $\zeta=(s_{0},\nu_{0})\xrightarrow{d_{1}}(s_{1},\nu_{1})\xrightarrow{d_{2}}\cdots(s_{k},\nu_{k})$ of steps. We lift the notions of length and instances from paths to traces in the obvious way: we consider the path $\pi=s_{0}\xrightarrow{d_{1}}s_{1}\xrightarrow{d_{2}}\cdots s_{k}$ that consists of the transitions used by $\zeta$, and set $\mathit{length}(\zeta):=\mathit{length}(\pi)$ and $\mathtt{instance}(\zeta,t)=\mathtt{instance}(\pi,t)$, for all $t\in\mathit{Trns}(\mathcal{V})$. We denote by $\mathtt{init}(\zeta)=\left\lVert\nu_{0}\right\rVert$ the maximum absolute value of the starting valuation $\nu_{0}$ of $\zeta$. We say that $\zeta$ reaches a valuation $\nu$, if $\nu=\nu_{k}$. The complexity of $\mathcal{V}$ is the function $\mathit{comp}_{\mathcal{V}}(N)=\sup_{\text{trace }\zeta\text{ of }\mathcal{V},\mathtt{init}(\zeta)\leq N}\mathit{length}(\zeta)$, which returns for every $N\geq 0$ the supremum over the lengths of the traces $\zeta$ with $\mathtt{init}(\zeta)\leq N$. The variable bound of a variable $x\in\mathit{Var}$ is the function $\mathtt{vbound}_{x}(N)=\sup_{\text{trace }\zeta\text{ of }\mathcal{V},\mathtt{init}(\zeta)\leq N,\zeta\text{ reaches valuation }\nu}\nu(x)$, which returns for every $N\geq 0$ the supremum over the the values of $x$ reachable by traces $\zeta$ with $\mathtt{init}(\zeta)\leq N$. The transition bound of a transition $t\in\mathit{Trns}(\mathcal{V})$ is the function $\mathtt{tbound}_{t}(N)=\sup_{\text{trace }\zeta\text{ of }\mathcal{V},\mathtt{init}(\zeta)\leq N}\mathtt{instance}(\zeta,t)$, which returns for every $N\geq 0$ the supremum over the number of instances of $t$ in traces $\zeta$ with $\mathtt{init}(\zeta)\leq N$.

Rooted Tree.

A rooted tree is a connected undirected acyclic graph in which one node has been designated as the root. We will usually denote the root by $\iota$. We note that for every node $\eta$ in a rooted tree there is a unique path of $\eta$ to the root. The parent of a node $\eta\neq\iota$ is the node connected to $\eta$ on the path to the root. Node $\eta$ is a child of a node $\eta^{\prime}$, if $\eta^{\prime}$ is the parent of $\eta$. $\eta^{\prime}$ is a descendent of $\eta$, if $\eta$ lies on the path from $\eta^{\prime}$ to the root; $\eta^{\prime}$ is a strict descendent, if furthermore $\eta\neq\eta^{\prime}$. $\eta$ is an ancestor of $\eta^{\prime}$, if $\eta^{\prime}$ a descendent of $\eta$; $\eta$ is a strict ancestor, if furthermore $\eta\neq\eta^{\prime}$. The distance of a node $\eta$ to the root, is the number of nodes $\neq\eta$ on the path from $\eta$ to the root. We denote by $\mathtt{layer}(l)$ the set of all nodes with the same distance $l$ to the root; we remark that $\mathtt{layer}(0)=\{\iota\}$.

All proofs are stated in the appendix.

3 A Dichotomy Result

We will make use of the following matrices associated to a VASS throughout the paper: Let $\mathcal{V}$ be a VASS. We define the update matrix $D\in\mathbb{Z}^{\mathit{Var}\times\mathit{Trns}(\mathcal{V})}$ by setting $D(t)=d$ for all transitions $t=(s,d,s^{\prime})\in\mathit{Trns}(\mathcal{V})$. We define the flow matrix $F\in\mathbb{Z}^{\mathit{St}(\mathcal{V})\times\mathit{Trns}(\mathcal{V})}$ by setting $F(s,t)=-1$, $F(s^{\prime},t)=1$ for transitions $t=(s,d,s^{\prime})$ with $s^{\prime}\neq s$, and $F(s,t)=F(s^{\prime},t)=0$ for transitions $t=(s,d,s^{\prime})$ with $s^{\prime}=s$; in both cases we further set $F(s^{\prime\prime},t)=0$ for all states $s^{\prime\prime}$ with $s^{\prime\prime}\neq s$ and $s^{\prime\prime}\neq s^{\prime}$. We note that every column $t$ of $F$ either contains exactly one $-1$ and $1$ entry (in case the source and target of transition $t$ are different) or only [math] entries (in case the source and target of transition $t$ are the same).

Example 1

We state the update and flow matrix for $\mathcal{V}_{\mathit{run}}$ from Section 1:

$D=\begin{pmatrix}-1&1&-1&1&0&0&0&0&-1&0\\ 1&-1&1&-1&0&0&0&0&0&0\\ -1&1&1&-1&-1&-1&-1&-1&0&0\end{pmatrix}$, $F=\begin{pmatrix}0&0&0&0&1&-1&0&0&-1&0\\ 0&0&0&0&-1&1&0&0&0&1\\ 0&0&0&0&0&0&1&-1&1&0\\ 0&0&0&0&0&0&-1&1&0&-1\end{pmatrix}$, with column order $s_{1}\rightarrow s_{1}$, $s_{2}\rightarrow s_{2}$, $s_{3}\rightarrow s_{3}$, $s_{4}\rightarrow s_{4}$, $s_{2}\rightarrow s_{1}$, $s_{1}\rightarrow s_{2}$, $s_{4}\rightarrow s_{3}$, $s_{3}\rightarrow s_{4}$, $s_{1}\rightarrow s_{3}$, $s_{4}\rightarrow s_{2}$ (from left to right) and row order $x,y,z$ for $D$ resp. $s_{1},s_{2},s_{3},s_{4}$ for $F$ (from top to bottom).

We now consider the constraint systems ($P$) and ($Q$), stated below, which have maximization objectives. The constraint systems will be used by our main algorithm in Section 4. We observe that both constraint systems are always satisfiable (set all coefficients to zero) and that the solutions of both constraint systems are closed under addition. Hence, the number of inequalities for which the maximization objective is satisfied is unique for optimal solutions of both constraint systems. The maximization objectives can be implemented by suitable linear objective functions. Hence, both constraint systems can be solved in PTIME over the integers, because we can use linear programming over the rationales and then scale rational solutions to the integers by multiplying with the least common multiple of the denominators.

[TABLE]

The solutions of ($P$) and ($Q$) are characterized by the following two lemmata:

Lemma 1 (Cited from [14])

$\mu\in\mathbb{Z}^{\mathit{Trns}(\mathcal{V})}$* is a solution to constraint system ($P$) iff there exists a multi-cycle $M$ with $\mathit{val}(M)\geq 0$ and $\mu(t)$ instances of transition $t$ for every $t\in\mathit{Trns}(\mathcal{V})$.*

Lemma 2 (Cited from [5]111There is no explicit lemma with this statement in [5], however the lemma is implicit in the exposition of Section 4 in [5].

We further note that [5] does not include the constraint $z\geq 0$. However, this difference is minor and was added in order to ensure that ranking functions always return non-negative values, which is more standard than the choice of [5]. A proof of the lemma can be found in the appendix.)

Let $r,z$ be a solution to constraint system ($Q$). Let $\mathit{rank}(r,z):\mathit{Cfg}(\mathcal{V})\rightarrow\mathbb{N}$ be the function defined by $\mathit{rank}(r,z)(s,\nu)=r^{T}\nu+z(s)$. Then, $\mathit{rank}(r,z)$ is a quasi-ranking function for $\mathcal{V}$, i.e., we have

for all $(s,\nu)\in\mathit{Cfg}(\mathcal{V})$ that $\mathit{rank}(r,z)(s,\nu)\geq 0;$ 2. 2.

for all transitions $t=s_{1}\xrightarrow{d}s_{2}\in\mathit{Trns}(\mathcal{V})$ and valuations $\nu_{1},\nu_{2}\in\mathit{Val}(\mathcal{V})$ with $\nu_{2}=\nu_{1}+d$ that $\mathit{rank}(r,z)(s_{1},\nu_{1})\geq\mathit{rank}(r,z)(s_{2},\nu_{2})$; moreover, the inequality is strict for every $t$ with $(D^{T}r+F^{T}z)(t)<0$.

We now state a dichotomy between optimal solutions to constraint systems ($P$) and ($Q$), which is obtained by an application of Farkas’ Lemma. This dichotomy is the main reason why we are able to compute the precise asymptotic complexity of VASSs with polynomial bounds.

Lemma 3

Let $r$ and $z$ be an optimal solution to constraint system ($Q$) and let $\mu$ be an optimal solution to constraint system ($P$). Then, for all variables $x\in\mathit{Var}$ we either have $r(x)>0$ or $(D\mu)(x)\geq 1$, and for all transitions $t\in\mathit{Trns}(\mathcal{V})$ we either have $(D^{T}r+F^{T}z)(t)<0$ or $\mu(t)\geq 1$.

Example 2

Our main algorithm, Algorithm 1 presented in Section 4, will directly use constraint systems ($P$) and ($Q$) in its first loop iteration, and adjusted versions in later loop iterations. Here, we illustrate the first loop iteration. We consider the running example $\mathcal{V}_{\mathit{run}}$, whose update and flow matrices we have stated in Example 1. An optimal solution to constraint systems ($P$) and ($Q$) is given by $\mu=(1441111100)^{T}$ and $r=(220)^{T}$, $z=(0011)^{T}$. The quasi-ranking function $\mathit{rank}(r,z)$ immediately establishes that $\mathtt{tbound}_{t}(N)\in O(N)$ for $t=s_{1}\rightarrow s_{3}$ and $t=s_{4}\rightarrow s_{2}$, because

1. $\mathit{rank}(r,z)$ decreases for these two transitions and does not increase for other transitions (by Lemma 2), and because
2. the initial value of $\mathit{rank}(r,z)$ is bounded by $O(N)$, i.e., we have $\mathit{rank}(r,z)(s,\nu)\in O(N)$ for every state $s\in\mathit{St}(\mathcal{V}_{\mathit{run}})$ and every valuation $\nu$ with $\left\lVert\nu\right\rVert\leq N$. By a similar argument we get $\mathtt{vbound}_{x}(N)\in O(N)$ and $\mathtt{vbound}_{y}(N)\in O(N)$. The exact reasoning for deriving upper bounds is given in Section 5. From $\mu$ we can, by Lemma 1, obtain the cycles $C_{1}=s_{1}\rightarrow s_{2}\rightarrow s_{2}\rightarrow s_{2}\rightarrow s_{2}\rightarrow s_{2}\rightarrow s_{1}\rightarrow s_{1}$ and $C_{2}=s_{3}\rightarrow s_{4}\rightarrow s_{4}\rightarrow s_{4}\rightarrow s_{4}\rightarrow s_{4}\rightarrow s_{4}\rightarrow s_{4}$ with $\nu(C_{1})+\nu(C_{2})\geq(001)^{T}$ (). We will later show that the cycles $C_{1}$ and $C_{2}$ give rise to a family of traces that establish $\mathtt{tbound}_{t}(N)\in\Omega(N^{2})$ for all transitions $t\in\mathit{Trns}(\mathcal{V}_{\mathit{run}})$ with $t\neq s_{1}\rightarrow s_{3}$ and $t\neq s_{4}\rightarrow s_{2}$. Here we give an intuition on the construction: We consider a cycle $C$ of $\mathcal{V}_{\mathit{run}}$ that visits all states at least once. By (), the updates along the cycles $C_{1}$ and $C_{2}$ cancel each other out. However, the two cycles are not connected. Hence, we execute the cycle $C_{1}$ some $\Omega(N)$ times, then (s part of) the cycle $C$, then execute $C_{2}$ as often as $C_{1}$, and finally the remaining part of $C$; this we repeat $\Omega(N)$ times. This construction also establishes the bound $\mathtt{vbound}_{z}(N)\in\Omega(N^{2})$ because, by (*), we increase $z$ with every joint execution of $C_{1}$ and $C_{2}$. The precise lower bound construction is given in Section 6.

4 Main Algorithm

Our main algorithm – Algorithm 1 – computes the complexity as well as variable and transition bounds of an input VASS $\mathcal{V}$, either detecting that $\mathcal{V}$ has at least exponential complexity or reporting precise asymptotic bounds for the transitions and variables of $\mathcal{V}$ (up to a constant factor): Algorithm 1 will compute values $\mathtt{vExp}(x)\in\mathbb{N}$ such that $\mathtt{vbound}_{N}(x)\in\Theta(N^{\mathtt{vExp}(x)})$ for every $x\in\mathit{Var}$ and values $\mathtt{tExp}(t)\in\mathbb{N}$ such that $\mathtt{tbound}_{N}(t)\in\Theta(N^{\mathtt{tExp}(t)})$ for every $t\in\mathit{Trns}(\mathcal{V})$.

Data Structures.

The algorithm maintains a rooted tree $T$. Every node $\eta$ of $T$ will always be labelled by a sub-VASSs $\mathtt{VASS}(\eta)$ of $\mathcal{V}$. The nodes in the same layer of $T$ will always be labelled by disjoint sub-VASS of $\mathcal{V}$. The main loop of Algorithm 1 will extend $T$ by one layer per loop iteration. The variable $l$ always contains the next layer that is going to be added to $T$. For computing variable and transition bounds, Algorithm 1 maintains the functions $\mathtt{vExp}:\mathit{Var}\rightarrow\mathbb{N}\cup\{\infty\}$ and $\mathtt{tExp}:\mathit{Trns}(\mathcal{V})\rightarrow\mathbb{N}\cup\{\infty\}$.

Initialization.

We assume $D$ to be the update matrix and $F$ to be the flow matrix associated to $\mathcal{V}$ as discussed in Section 3. At initialization, $T$ consists of the root node $\iota$ and we set $\mathtt{VASS}(\iota)=\mathcal{V}$, i.e., the root is labelled by the input $\mathcal{V}$. We initialize $l=1$ as Algorithm 1 is going to add layer $1$ to $T$ in the first loop iteration. We initialize $\mathtt{vExp}(x)=\infty$ for all variables $x\in\mathit{Var}$ and $\mathtt{tExp}(t)=\infty$ for all transitions $t\in\mathit{Trns}(\mathcal{V})$.

The constraint systems solved during each loop iteration.

In loop iteration $l$, Algorithm 1 will set $\mathtt{tExp}(t):=l$ for some transitions $t$ and $\mathtt{vExp}(x):=l$ for some variables $x$. In order to determine those transitions and variables, Algorithm 1 instantiates constraint systems ($P$) and ($Q$) from Section 3 over the set of transitions $U=\bigcup_{\eta\in\mathtt{layer}(l-1)}\mathit{Trns}(\mathtt{VASS}(\eta))$, which contains all transitions associated to nodes in layer $l-1$ of $T$. However, instead of a direct instantiation using $D|_{U}$ and $F|_{U}$ (i.e., the restriction of $D$ and $F$ to the transitions $U$), we need to work with an extended set of variables and an extended update matrix. We set $\mathit{Var}_{\mathit{ext}}:=\{(x,\eta)\mid\eta\in\mathtt{layer}(l-\mathtt{vExp}(x))\}$, where we set $n-\infty=0$ for all $n\in\mathbb{N}$. This means that we use a different copy of variable $x$ for every node $\eta$ in layer $l-\mathtt{vExp}(x)$. We note that for a variable $x$ with $\mathtt{vExp}(x)=\infty$ there is only a single copy of $x$ in $\mathit{Var}_{\mathit{ext}}$ because $\iota\in\mathtt{layer}(0)$ is the only node in layer [math]. We define the extended update matrix $D_{\mathit{ext}}\in\mathbb{Z}^{\mathit{Var}_{\mathit{ext}}\times U}$ by setting

[TABLE]

Constraint systems ($\mathit{I}$) and ($\mathit{II}$) stated in Figure 2 can be recognized as instantiation of constraint systems ($P$) and ($Q$) with matrices $D_{\mathit{ext}}$ and $F|_{U}$ and variables $\mathit{Var}_{\mathit{ext}}$, and hence the dichotomy stated in Lemma 3 holds.

We comment on the choice of $\mathit{Var}_{\mathit{ext}}$: Setting $\mathit{Var}_{\mathit{ext}}=\{(x,\eta)\mid\eta\in\mathtt{layer}(i)\}$ for any $i\leq l-\mathtt{vExp}(x)$ would result in correct upper bounds (while $i>l-\mathtt{vExp}(x)$ would not). However, choosing $i<l-\mathtt{vExp}(x)$ does in general result in sub-optimal bounds because fewer variables make constraint system ($\mathit{I}$) easier and constraint system ($\mathit{II}$) harder to satisfy (in terms of their maximization objectives). In fact, $i=l-\mathtt{vExp}(x)$ is the optimal choice, because this choice allows us to prove corresponding lower bounds in Section 6. We will further comment on key properties of constraint systems ($\mathit{I}$) and ($\mathit{II}$) in Sections 5 and 6, when we outline the proofs of the upper resp. lower bound.

We note that Algorithm 1 does not use the optimal solution $\mu$ to constraint system ($\mathit{I}$) for the computation of the $\mathtt{vExp}(x)$ and $\mathtt{tExp}(t)$, and hence the computation of the optimal solution $\mu$ could be removed from the algorithm. The solution $\mu$ is however needed for the extraction of lower bounds in Sections 6 and 8, and this is the reason why it is stated here. The extraction of lower bounds is not explicitly added to the algorithm in order to not clutter the presentation.

Discovering transition bounds.

After an optimal solution $r$, $z$ to constraint system ($\mathit{II}$) has been found, Algorithm 1 collects all transitions $t$ with $(D_{\mathit{ext}}^{T}r+F|_{U}^{T}z)(t)<0$ in the set $R$ (note that the optimization criterion in constraint system ($\mathit{II}$) tries to find as many such $t$ as possible). Algorithm 1 then sets $\mathtt{tExp}(t):=l$ for all $t\in R$. The transitions in $R$ will not be part of layer $l$ of $T$.

Construction of the next layer in $T$.

For each node $\eta$ in layer $l-1$, Algorithm 1 will create children by removing the transitions in $R$. This is done as follows: Given a node $\eta$ in layer $l-1$, Algorithm 1 considers the VASS $\mathcal{V}^{\prime}=\mathtt{VASS}(\eta)$ associated to $\eta$. Then, $(\mathit{St}(\mathcal{V}^{\prime}),\mathit{Trns}(\mathcal{V}^{\prime})\setminus R)$ is decomposed into its SCCs. Finally, for each SCC $S$ of $(\mathit{St}(\mathcal{V}^{\prime}),\mathit{Trns}(\mathcal{V}^{\prime})\setminus R)$ a child $\eta^{\prime}$ of $\eta$ is created with $\mathtt{VASS}(\eta^{\prime})=S$. Clearly, the new nodes in layer $l$ are labelled by disjoint sub-VASS of $\mathcal{V}$.

The transitions of the next layer.

The following lemma states that the new layer $l$ of $T$ contains all transitions of layer $l-1$ except for the transitions $R$; the lemma is due to the fact that every transition in $U\setminus R$ belongs to a cycle and hence to some SCC that is part of the new layer $l$.

Lemma 4

We consider the new layer constructed during loop iteration $l$ of Algorithm 1: we have $U\setminus R=\bigcup_{\eta\in\mathtt{layer}(l)}\mathit{Trns}(\mathtt{VASS}(\eta))$.

Discovering variable bounds.

For each $x\in\mathit{Var}$ with $\mathtt{vExp}(x)=\infty$, Algorithm 1 checks whether $r(x,\iota)>0$ (we point out that the optimization criterion in constraint systems ($\mathit{II}$) tries to find as many such $x$ with $r(x,\iota)>0$ as possible). Algorithm 1 then sets $\mathtt{vExp}(x):=l$ for all those variables.

The check for exponential complexity.

In each loop iteration, Algorithm 1 checks whether there are $x\in\mathit{Var}$, $t\in\mathit{Trns}(\mathcal{V})$ with $l<\mathtt{vExp}(x)+\mathtt{tExp}(t)<\infty$. If this is not the case, then we can conclude that $\mathcal{V}$ is at least exponential (see Theorem 4.1 below). If the check fails, Algorithm 1 increments $l$ and continues with the construction of the next layer in the next loop iteration.

Termination criterion.

The algorithm proceeds until either exponential complexity has been detected or until $\mathtt{vExp}(x)\neq\infty$ and $\mathtt{tExp}(t)\neq\infty$ for all $x\in\mathit{Var}$ and $t\in\mathit{Trns}(\mathcal{V})$ (i.e., bounds have been computed for all variables and transitions).

Invariants.

We now state some simple invariants maintained by Algorithm 1, which are easy to verify:

• •

For every node $\eta$ that is a descendent of some node $\eta^{\prime}$ we have that $\mathtt{VASS}(\eta)$ is a sub-VASS of $\mathtt{VASS}(\eta^{\prime})$.

• •

The value of $\mathtt{vExp}$ and $\mathtt{tExp}$ is changed at most once for each input; when the value is changed, it is changed from $\infty$ to some value $\neq\infty$.

• •

For every transition $t\in\mathit{Trns}(\mathcal{V})$ and layer $l$ of $T$, we have that either $\mathtt{tExp}(t)\leq l$ or there is a node $\eta\in\mathtt{layer}(l)$ such that $t\in\mathit{Trns}(\mathtt{VASS}(\eta))$.

• •

We have $\mathtt{tExp}(t)=l$ for $t\in\mathit{Trns}(\mathcal{V})$ if and only if there is a $\eta\in\mathtt{layer}(l-1)$ with $t\in\mathit{Trns}(\mathtt{VASS}(\eta))$ and there is no $\eta\in\mathtt{layer}(l)$ with $t\in\mathit{Trns}(\mathtt{VASS}(\eta))$.

Example 3

We sketch the execution of Algorithm 1 on $\mathcal{V}_{\mathit{run}}$. In iteration $l=1$, we have $\mathit{Var}_{\mathit{ext}}=\{(x,\iota),(y,\iota),(z,\iota)\}$, and thus matrix $D_{\mathit{ext}}$ is identical to the matrix $D$. Hence, constraint systems ($\mathit{I}$) and ($\mathit{II}$) are identical to constraint systems ($P$) and ($Q$), whose optimal solutions $\mu=(1441111100)^{T}$ and $r=(220)^{T}$, $z=(0011)^{T}$ we have discussed in Example 2. Algorithm 1 then sets $\mathtt{tExp}(s_{1}\rightarrow s_{3})=1$ and $\mathtt{tExp}(s_{4}\rightarrow s_{2})=1$, creates two children $\eta_{A}$ and $\eta_{B}$ of $\iota$ labeled by $\mathcal{V}_{A}=(\{s_{1},s_{2}\},\{s_{1}\rightarrow s_{1},s_{1}\rightarrow s_{2},s_{2}\rightarrow s_{2},s_{2}\rightarrow s_{1}\})$ and $\mathcal{V}_{B}=(\{s_{3},s_{4}\},\{s_{3}\rightarrow s_{3},s_{3}\rightarrow s_{4},s_{4}\rightarrow s_{4},s_{4}\rightarrow s_{3}\})$, and sets $\mathtt{vExp}(x)=1$ and $\mathtt{vExp}(y)=1$. In iteration $l=2$, we have $\mathit{Var}_{\mathit{ext}}=\{(x,\eta_{A}),(y,\eta_{A}),(x,\eta_{B}),(y,\eta_{B}),(z,\iota)\}$ and the matrix $D_{\mathit{ext}}$ stated in Figure 3. Algorithm 1 obtains $\mu=(11110000)^{T}$ and $r=(12211)^{T}$, $z=(0000)^{T}$ as optimal solutions to ($\mathit{I}$) and ($\mathit{II}$). Algorithm 1 then sets $\mathtt{tExp}(s_{1}\rightarrow s_{2})=\mathtt{tExp}(s_{2}\rightarrow s_{1})=\mathtt{tExp}(s_{3}\rightarrow s_{4})=\mathtt{tExp}(s_{4}\rightarrow s_{3})=2$, creates the children $\eta_{1},\eta_{2}$ resp. $\eta_{3},\eta_{4}$ of $\eta_{A}$ resp. $\eta_{B}$ with $\eta_{i}$ labelled by $\mathcal{V}_{i}=(\{s_{i}\},\{s_{i}\rightarrow s_{i}\})$, and sets $\mathtt{vExp}(z)=2$. In iteration $l=3$, we have $\mathit{Var}_{\mathit{ext}}=\{(x,\eta_{1}),(y,\eta_{1}),(x,\eta_{2}),(y,\eta_{2}),(x,\eta_{3}),$ $(y,\eta_{3}),(x,\eta_{4}),(y,\eta_{4}),(z,\eta_{A}),(z,\eta_{B})\}$ and the matrix $D_{\mathit{ext}}$ stated in Figure 3. Algorithm 1 obtains $\mu=(0000)^{T}$ and $r=(1113311111)^{T}$, $z=(0000)^{T}$ as optimal solutions to ($\mathit{I}$) and ($\mathit{II}$). Algorithm 1 then sets $\mathtt{tExp}(s_{i}\rightarrow s_{i})=3$, for all $i$, and terminates.

We now state the main properties of Algorithm 1:

Lemma 5

Algorithm 1 always terminates.

Theorem 4.1

If Algorithm 1 returns “$\mathcal{V}$ has at least exponential complexity”, then $\mathit{comp}_{\mathcal{V}}(N)\in 2^{\Omega(N)}$, and we have $\mathtt{tbound}_{t}(N)\in 2^{\Omega(N)}$ for all $t\in\mathit{Trns}(\mathcal{V})$ with $\mathtt{tExp}(t)=\infty$ and $\mathtt{vbound}_{t}(N)\in 2^{\Omega(N)}$ for all $x\in\mathit{Var}$ with $\mathtt{vExp}(x)=\infty$.

The proof of Theorem 4.1 is stated in Section 8. We now assume that Algorithm 1 does not return “$\mathcal{V}$ has at least exponential complexity”. Then, Algorithm 1 must terminate with $\mathtt{tExp}(t)\neq\infty$ and $\mathtt{vExp}(x)\neq\infty$ for all $t\in\mathit{Trns}(\mathcal{V})$ and $x\in\mathit{Var}$. The following result states that $\mathtt{tExp}$ and $\mathtt{vExp}$ contain the precise exponents of the asymptotic transition and variable bounds of $\mathcal{V}$:

Theorem 4.2

$\mathtt{vbound}_{N}(x)\in\Theta(N^{\mathtt{vExp}(x)})$* for all $x\in\mathit{Var}$ and $\mathtt{tbound}_{N}(t)\in\Theta(N^{\mathtt{tExp}(t)})$ for all $t\in\mathit{Trns}(\mathcal{V})$.*

The upper bounds of Theorem 4.2 will be proved in Section 5 (Theorem 5.1) and the lower bounds in Section 6 (Corollary 2).

We will prove in Section 7 that the exponents of the variable and transition bounds are bounded exponentially in the dimension of $\mathcal{V}$:

Theorem 4.3

We have $\mathtt{vExp}(x)\leq 2^{|\mathit{Var}|}$ for all $x\in\mathit{Var}$ and $\mathtt{tExp}(t)\leq 2^{|\mathit{Var}|}$ for all $t\in\mathit{Trns}(\mathcal{V})$.

Finally, we obtain the following corollary from Theorems 4.2 and 4.3:

Corollary 1

Let $\mathcal{V}$ be a connected VASS. Then, either $\mathit{comp}_{\mathcal{V}}(N)\in 2^{\Omega(N)}$ or $\mathit{comp}_{\mathcal{V}}(N)\in\Theta(N^{i})$ for some computable $1\leq i\leq 2^{|\mathit{Var}|}$.

4.1 Complexity of Algorithm 1

In the remainder of this section we will establish the following result:

Theorem 4.4

Algorithm 1 (with the below stated optimization) can be implemented in polynomial time with regard to the size of the input VASS $\mathcal{V}$.

We will argue that A) every loop iteration of Algorithm 1 only takes polynomial time, and B) that polynomially many loop iterations are sufficient (this only holds for the optimization of the algorithm discussed below).

Let $\mathcal{V}$ be a VASS, let $m=|\mathit{Trns}(\mathcal{V})|$ be the number of transitions of $\mathcal{V}$, and let $n=|\mathit{Var}|$ be the dimension of $\mathcal{V}$. We note that $|\mathtt{layer}(l)|\leq m$ for every layer $l$ of $T$, because the VASSs of the nodes in the same layer are disjoint.

A) Clearly, removing the decreasing transitions and computing the strongly connected components can be done in polynomial time. It remains to argue about constraint systems ($\mathit{I}$) and ($\mathit{II}$). We observe that $|\mathit{Var}_{\mathit{ext}}|=|\{(x,\eta)\mid\eta\in\mathtt{layer}(l-\mathtt{vExp}(x))\}|\leq n\cdot m$ and $|U|\leq m$. Hence the size of constraint systems ($\mathit{I}$) and ($\mathit{II}$) is polynomial in the size of $\mathcal{V}$. Moreover, constraint systems ($\mathit{I}$) and ($\mathit{II}$) can be solved in PTIME as noted in Section 3.

B) We do not a-priori have a bound on the number of iterations of the main loop of Algorithm 1. (Theorem 4.3 implies that the number of iterations is at most exponential; however, we do not use this result here). We will shortly state an improvement of Algorithm 1 that ensures that polynomially many iterations are sufficient. The underlying insight is that certain layers of the tree do not need to be constructed explicitly. This insight is stated in the lemma below:

Lemma 6

We consider the point in time when the execution of Algorithm 1 reaches line $l:=l+1$ during some loop iteration $l\geq 1$. Let $\mathit{RelevantLayers}=\{\mathtt{tExp}(t)+\mathtt{vExp}(x)\mid x\in\mathit{Var},t\in\mathit{Trns}(\mathcal{V})\}$ and let $l^{\prime}=\min\{l^{\prime}\mid l^{\prime}>l,l^{\prime}\in\mathit{RelevantLayers}\}$. Then, $\mathtt{vExp}(x)\neq i$ and $\mathtt{tExp}(t)\neq i$ for all $x\in\mathit{Var}$, $t\in\mathit{Trns}(\mathcal{V})$ and $l<i<l^{\prime}$.

We now present the optimization that achieves polynomially many loop iterations. We replace the line $l:=l+1$ by the two lines $\mathit{RelevantLayers}:=\{\mathtt{tExp}(t)+\mathtt{vExp}(x)\mid x\in\mathit{Var},t\in\mathit{Trns}(\mathcal{V})\}$ and $l:=\min\{l^{\prime}\mid l^{\prime}>l,l^{\prime}\in\mathit{RelevantLayers}\}$. The effect of these two lines is that Algorithm 1 directly skips to the next relevant layer. Lemma 6, stated above, justifies this optimization: First, no new variable or transition bound is discovered in the intermediate layers $l<i<l^{\prime}$. Second, each intermediate layer $l<i<l^{\prime}$ has the same number of nodes as layer $l$, which are labelled by the same sub-VASSs as the nodes in $l$ (otherwise there would be a transition with transition bound $l<i<l^{\prime}$); hence, whenever needed, Algorithm 1 can construct a missing layer $l<i<l^{\prime}$ on-the-fly from layer $l$.

We now analyze the number of loop iterations of the optimized algorithm. We recall that the value of each $\mathtt{vExp}(x)$ and $\mathtt{tExp}(t)$ is changed at most once from $\infty$ to some value $\neq\infty$. Hence, Algorithm 1 encounters at most $n\cdot m$ different values in the set $\mathit{RelevantLayers}=\{\mathtt{tExp}(t)+\mathtt{vExp}(x)\mid x\in\mathit{Var},t\in\mathit{Trns}(\mathcal{V})\}$ during execution. Thus, the number of loop iterations is bounded by $n\cdot m$.

5 Proof of the Upper Bound Theorem

We begin by stating a proof principle for obtaining upper bounds.

Proposition 1 (Bound Proof Principle)

Let $\mathcal{V}$ be a VASS. Let $U\subseteq\mathit{Trns}(\mathcal{V})$ be a subset of the transitions of $\mathcal{V}$. Let $w:\mathit{Cfg}(\mathcal{V})\rightarrow\mathbb{N}$ and $\mathtt{inc}_{t}:\mathbb{N}\rightarrow\mathbb{N}$, for every $t\in\mathit{Trns}(\mathcal{V})\setminus U$, be functions such that for every trace $\zeta=(s_{0},\nu_{0})\xrightarrow{d_{1}}(s_{1},\nu_{1})\xrightarrow{d_{2}}\cdots$ of $\mathcal{V}$ with $\mathtt{init}(\zeta)\leq N$ we have for every $i\geq 0$ that

$s_{i}\xrightarrow{d_{i}}s_{i+1}\in U$* implies $w(s_{i},\nu_{i})\geq w(s_{i+1},\nu_{i+1})$, and* 2. 2)

$s_{i}\xrightarrow{d_{i}}s_{i+1}\in\mathit{Trns}(\mathcal{V})\setminus U$* implies $w(s_{i},\nu_{i})+\mathtt{inc}_{t}(N)\geq w(s_{i+1},\nu_{i+1})$.*

We call such a function $w$ a complexity witness and the associated $\mathtt{inc}_{t}$ functions the increase certificates.

Let $t\in U$ be a transition on which $w$ decreases, i.e., we have $w(s_{1},\nu_{1})\geq w(s_{2},\nu_{2})-1$ for every step $(s_{1},\nu_{1})\xrightarrow{d}(s_{2},\nu_{2})$ of $\mathcal{V}$ with $t=s_{1}\xrightarrow{d}s_{2}$. Then,

[TABLE]

Further, let $x\in\mathit{Var}$ be a variable such that $\nu(x)\leq w(s,\nu)$ for all $(s,\nu)\in\mathit{Cfg}(\mathcal{V})$. Then,

[TABLE]

Proof Outline of the Upper Bound Theorem.

Let $\mathcal{V}$ be a VASS for which Algorithm 1 does not report exponential complexity. We will prove by induction on loop iteration $l$ that $\mathtt{vbound}_{N}(x)\in O(N^{l})$ for every $x\in\mathit{Var}$ with $\mathtt{vExp}(x)=l$ and that $\mathtt{tbound}_{N}(t)\in O(N^{l})$ for every $t\in\mathit{Trns}(\mathcal{V})$ with $\mathtt{tExp}(t)=l$.

We now consider some loop iteration $l\geq 1$. Let $U=\bigcup_{\eta\in\mathtt{layer}(l-1)}\mathit{Trns}(\mathtt{VASS}(\eta))$ be the transitions, $\mathit{Var}_{\mathit{ext}}$ be the set of extended variables and $D_{\mathit{ext}}\in\mathbb{Z}^{\mathit{Var}_{\mathit{ext}}\times U}$ be the update matrix considered by Algorithm 1 during loop iteration $l$. Let $r,z$ be some optimal solution to constraint system ($\mathit{II}$) computed by Algorithm 1 during loop iteration $l$. The main idea for the upper bound proof is to use the quasi-ranking function from Lemma 2 as witness function for the Bound Proof Principle. In order to apply Lemma 2 we need to consider the VASS associated to the matrices in constraint system ($\mathit{II}$): Let $\mathcal{V}_{\mathit{ext}}$ be the VASS over variables $\mathit{Var}_{\mathit{ext}}$ associated to update matrix $D_{\mathit{ext}}$ and flow matrix $F|_{U}$. From Lemma 2 we get that $\mathit{rank}(r,z):\mathit{Cfg}(\mathcal{V}_{\mathit{ext}})\rightarrow\mathbb{N}$ is a quasi-ranking function for $\mathcal{V}_{\mathit{ext}}$. We now need to relate $\mathcal{V}$ to the extended VASS $\mathcal{V}_{\mathit{ext}}$ in order to be able to use this quasi-ranking function. We do so by extending valuations over $\mathit{Var}$ to valuations over $\mathit{Var}_{\mathit{ext}}$. For every state $s\in\mathit{St}(\mathcal{V})$ and valuation $\nu:\mathit{Var}\rightarrow\mathbb{N}$, we define the extended valuation $\mathtt{ext}_{s}(\nu):\mathit{Var}_{\mathit{ext}}\rightarrow\mathbb{N}$ by setting

[TABLE]

As a direct consequence from the definition of extended valuations, we have that $(s,\mathtt{ext}_{s}(\nu))\in\mathit{Cfg}(\mathcal{V}_{\mathit{ext}})$ for all $(s,\nu)\in\mathit{Cfg}(\mathcal{V})$, and that $(s_{1},\mathtt{ext}_{s_{1}}(\nu_{1}))\xrightarrow{D_{\mathit{ext}}(t)}(s_{2},\mathtt{ext}_{s_{2}}(\nu_{2}))$ is a step of $\mathcal{V}_{\mathit{ext}}$ for every step $(s_{1},\nu_{1})\xrightarrow{d}(s_{2},\nu_{2})$ of $\mathcal{V}$ with $s_{1}\xrightarrow{d}s_{2}\in U$. We now define the witness function $w$ by setting

[TABLE]

We immediately get from Lemma 2 that $w$ maps configurations to the non-negative integers and that condition 1) of the Bound Proof Principle is satisfied. Indeed, we get from the first item of Lemma 2 that $w(s,\nu)\geq 0$ for all $(s,\nu)\in\mathit{Cfg}(\mathcal{V})$, and from the second item that $w(s_{1},\nu_{1})\geq w(s_{2},\nu_{2})$ for every step $(s_{1},\nu_{1})\xrightarrow{d}(s_{2},\nu_{2})$ of $\mathcal{V}$ with $t=s_{1}\xrightarrow{d}s_{2}\in U$; moreover, the inequality is strict if $(D_{\mathit{ext}}^{T}r+F|_{U}^{T}z)(t)<0$, i.e., the witness function $w$ decreases for transitions $t$ with $\mathtt{tExp}(t)=l$. It remains to establish condition 2) of the Bound Proof Principle. We will argue that we can find increase certificates $\mathtt{inc}_{t}(N)\in O(N^{l-\mathtt{tExp}(t)})$ for all $t\in\mathit{Trns}(\mathcal{V})\setminus U$. We note that $\mathtt{tExp}(t)<l$ for all $t\in\mathit{Trns}(\mathcal{V})\setminus U$, and hence the induction assumption can be applied for such $t$. We can then derive the desired bounds from the Bound Proof Principle because of $\sum_{t\in\mathit{Trns}(\mathcal{V})\setminus U}\mathtt{tbound}_{t}(N)\cdot\mathtt{inc}_{t}(N)=\sum_{t\in\mathit{Trns}(\mathcal{V})\setminus U}O(N^{\mathtt{tExp}(t)})\cdot O(N^{l-\mathtt{tExp}(t)})=O(N^{l})$.

Theorem 5.1

$\mathtt{vbound}_{N}(x)\in O(N^{\mathtt{vExp}(x)})$* for all $x\in\mathit{Var}$ and $\mathtt{tbound}_{N}(t)\in O(N^{\mathtt{tExp}(t)})$ for all $t\in\mathit{Trns}(\mathcal{V})$.*

6 Proof of the Lower Bound Theorem

The following lemma will allow us to consider traces $\zeta_{N}$ with $\mathtt{init}(\zeta_{N})\in O(N)$ instead of $\mathtt{init}(\zeta_{N})\leq N$ when proving asymptotic lower bounds.

Lemma 7

Let $\mathcal{V}$ be a VASS, let $t\in\mathit{Trns}(\mathcal{V})$ be a transition and let $x\in\mathit{Var}$ be a variable. If there are traces $\zeta_{N}$ with $\mathtt{init}(\zeta_{N})\in O(N)$ and $\mathtt{instance}(\zeta_{N},t)\geq N^{i}$, then $\mathtt{tbound}_{N}(t)\in\Omega(N^{i})$. If there are traces $\zeta_{N}$ with $\mathtt{init}(\zeta_{N})\in O(N)$ that reach a final valuation $\nu$ with $\nu(x)\geq N^{i}$, then $\mathtt{vbound}_{N}(x)\in\Omega(N^{i})$.

The lower bound proof uses the notion of a pre-path, which relaxes the notion of a path: A pre-path $\sigma=t_{1}\cdots t_{k}$ is a finite sequence of transitions $t_{i}=s_{i}\xrightarrow{d_{i}}s_{i}^{\prime}$. Note that we do not require for subsequent transitions that the end state of one transition is the start state of the next transition, i.e., we do not require $s_{i}^{\prime}=s_{i+1}$. We generalize notions from paths to pre-paths in the obvious way, e.g., we set $\mathit{val}(\sigma)=\sum_{i\in[1,k]}d_{i}$ and denote by $\mathtt{instance}(\sigma,t)$, for $t\in\mathit{Trns}(\mathcal{V})$, the number of times $\sigma$ contains the transition $t$. We say the pre-path $\sigma$ can be executed from valuation $\nu$, if there are valuations $\nu_{i}\geq 0$ with $\nu_{i+1}=\nu_{i}+d_{i+1}$ for all $0\leq i<k$ and $\nu=\nu_{0}$; we further say that $\sigma$ reaches valuation $\nu^{\prime}$, if $\nu^{\prime}=\nu_{k}$. We will need the following relationship between execution and traces: in case a pre-path $\sigma$ is actually a path, $\sigma$ can be executed from valuation $\nu$, if and only if there is a trace with initial valuation $\nu$ that uses the same sequence of transitions as $\sigma$. Two pre-paths $\sigma=t_{1}\cdots t_{k}$ and $\sigma^{\prime}=t_{1}^{\prime}\cdots t_{l}^{\prime}$ can be shuffled into a pre-path $\sigma^{\prime\prime}=t_{1}^{\prime\prime}\cdots t_{k+l}^{\prime\prime}$, if $\sigma^{\prime\prime}$ is an order-preserving interleaving of $\sigma$ and $\sigma^{\prime}$; formally, there are injective monotone functions $f:[1,k]\rightarrow[1,k+l]$ and $g:[1,l]\rightarrow[1,k+l]$ with $f([1,k])\cap g([1,l])=\emptyset$ such that $t_{f(i)}^{\prime\prime}=t_{i}$ for all $i\in[1,k]$ and $t_{g(i)}^{\prime\prime}=t_{i}^{\prime}$ for all $i\in[1,l]$. Further, for $d\geq 1$ and pre-path $\sigma$, we denote by $\sigma^{d}=\underbrace{\sigma\sigma\cdots\sigma}_{d}$ the pre-path that consists of $d$ subsequent copies of $\sigma$.

For the remainder of this section, we fix a VASS $\mathcal{V}$ for which Algorithm 1 does not report exponential complexity and we fix the computed tree $T$ and bounds $\mathtt{vExp}$, $\mathtt{tExp}$. We further need to use the solutions to constraint system ($\mathit{I}$) computed during the run of Algorithm 1: For every layer $l\geq 1$ and node $\eta\in\mathtt{layer}(l)$, we fix a cycle $C(\eta)$ that contains $\mu(t)$ instances of every $t\in\mathit{Trns}(\mathtt{VASS}(\eta))$, where $\mu$ is an optimal solution to constraint system ($\mathit{I}$) during loop iteration $l$. The existence of such cycles is stated in Lemma 8 below. We note that this definition ensures $\mathit{val}(C(\eta))=\sum_{t\in\mathit{Trns}(\mathtt{VASS}(\eta))}D(t)\cdot\mu(t)$. Further, for the root node $\iota$, we fix an arbitrary cycle $C(\iota)$ that uses all transitions of $\mathcal{V}$ at least once.

Lemma 8

Let $\mu$ be an optimal solution to constraint system ($\mathit{I}$) during loop iteration $l$ of Algorithm 1. Then there is a cycle $C(\eta)$ for every $\eta\in\mathtt{layer}(l)$ that contains exactly $\mu(t)$ instances of every transition $t\in\mathit{Trns}(\mathtt{VASS}(\eta))$.

Proof Outline of the Lower Bound Theorem.

Step I) We define a pre-path $\tau_{l}$, for every $l\geq 1$, with the following properties:

$\mathtt{instance}(\tau_{l},t)\geq N^{l+1}$ for all transitions $t\in\bigcup_{\eta\in\mathtt{layer}(l)}\mathit{Trns}(\mathtt{VASS}(\eta))$. 2. 2)

$\mathit{val}(\tau_{l})=N^{l+1}\sum_{\eta\in\mathtt{layer}(l)}\mathit{val}(C(\eta))$. 3. 3)

$\mathit{val}(\tau_{l})(x)\geq 0$ for every $x\in\mathit{Var}$ with $\mathtt{vExp}(x)\leq l$. 4. 4)

$\mathit{val}(\tau_{l})(x)\geq N^{l+1}$ for every $x\in\mathit{Var}$ with $\mathtt{vExp}(x)\geq l+1$. 5. 5)

$\tau_{l}$ is executable from some valuation $\nu$ with

1. a)

$\nu(x)\in O(N^{\mathtt{vExp}(x)})$ for $x\in\mathit{Var}$ with $\mathtt{vExp}(x)\leq l$, and 2. b)

$\nu(x)\in O(N^{l})$ for $x\in\mathit{Var}$ with $\mathtt{vExp}(x)\geq l+1$.

The difficulty in the construction of the pre-paths $\tau_{l}$ lies in ensuring Property 5). The construction of the $\tau_{l}$ proceeds along the tree $T$ using that the cycles $C(\eta)$ have been obtained according to solutions of constraint system ($\mathit{I}$).

Step II) It is now a direct consequence of Properties 3)-5) stated above that we can choose a sufficiently large $k>0$ such that for every $l\geq 0$ the pre-path $\rho_{l}=\tau_{0}^{k}\tau_{1}^{k}\cdots\tau_{l}^{k}$ (the concatenation of $k$ copies of each $\tau_{i}$, setting $\tau_{0}=C(\iota)^{N}$), can be executed from some valuation $\nu$ and reaches a valuation $\nu^{\prime}$ with

$\left\lVert\nu\right\rVert\in O(N)$, 2. 2)

$\nu^{\prime}(x)\geq kN^{\mathtt{vExp}(x)}$ for all $x\in\mathit{Var}$ with $\mathtt{vExp}(x)\leq l$, and 3. 3)

$\nu^{\prime}(x)\geq kN^{l+1}$ for all $x\in\mathit{Var}$ with $\mathtt{vExp}(x)\geq l+1$.

The above stated properties for the pre-path $\rho_{l_{\max}}$, where $l_{\max}$ is the maximal layer of $T$, would be sufficient to conclude the lower bound proof except that we need to extend the proof from pre-paths to proper paths.

Step III) In order to extend the proof from pre-paths to paths we make use of the concept of shuffling. For all $l\geq 0$, we will define paths $\gamma_{l}$ that can be obtained by shuffling the pre-paths $\rho_{0},\rho_{1},\ldots,\rho_{l}$. The path $\gamma_{l_{\max}}$, where $l_{\max}$ is the maximal layer of $T$, then has the desired properties and allows to conclude the lower bound proof with the following result:

Theorem 6.1

There are traces $\zeta_{N}$ with $\mathtt{init}(\zeta_{N})\in O(N)$ such that $\zeta_{N}$ ends in configuration $(s_{N},\nu_{N})$ with $\nu_{N}(x)\geq N^{\mathtt{vExp}(x)}$ for all variables $x\in\mathit{Var}$ and we have $\mathtt{instance}(\zeta_{N},t)\geq N^{\mathtt{tExp}(t)}$ for all transitions $t\in\mathit{Trns}(\mathcal{V})$.

With Lemma 7 we get the desired lower bounds from Theorem 6.1:

Corollary 2

$\mathtt{vbound}_{N}(x)\in\Omega(N^{\mathtt{vExp}(x)})$* for all $x\in\mathit{Var}$ and $\mathtt{tbound}_{N}(t)\in\Omega(N^{\mathtt{tExp}(t)})$ for all $t\in\mathit{Trns}(\mathcal{V})$.*

7 The Size of the Exponents

For the remainder of this section, we fix a VASS $\mathcal{V}$ for which Algorithm 1 does not report exponential complexity and we fix the computed tree $T$ and bounds $\mathtt{vExp}$, $\mathtt{tExp}$. Additionally, we fix a vector $z_{l}\in\mathbb{Z}^{\mathit{St}(\mathcal{V})}$ for every layer $l$ of $T$ and a vector $r_{\eta}\in\mathbb{Z}^{\mathit{Var}}$ for every node $\eta\in\mathtt{layer}(l)$ as follows: Let $r,z$ be an optimal solution to constraint system ($\mathit{II}$) in iteration $l+1$ of Algorithm 1. We then set $z_{l}=z$. For every $\eta\in\mathtt{layer}(l)$ we define $r_{\eta}$ by setting $r_{\eta}(x)=r(x,\eta^{\prime})$, where $\eta^{\prime}\in\mathtt{layer}(l-\mathtt{vExp}(x))$ is the unique ancestor of $\eta$ in layer $l-\mathtt{vExp}(x)$. The following properties are immediate from the definition:

Proposition 2

For every layer $l$ of $T$ and node $\eta\in\mathtt{layer}(l)$ we have:

$z_{l}\geq 0$* and $r_{\eta}\geq 0$.* 2. 2)

$r_{\eta}^{T}d+z_{l}(s_{2})-z_{l}(s_{1})\leq 0$* for every transition $s_{1}\xrightarrow{d}s_{2}\in\mathit{Trns}(\mathtt{VASS}(\eta))$; moreover, the inequality is strict for all transitions $t$ with $\mathtt{tExp}(t)=l+1$.* 3. 3)

Let $\eta^{\prime}\in\mathtt{layer}(i)$ be a strict ancestor of $\eta$. Then, $r_{\eta^{\prime}}^{T}d+z_{i}(s_{2})-z_{i}(s_{1})=0$ for every transition $s_{1}\xrightarrow{d}s_{2}\in\mathit{Trns}(\mathtt{VASS}(\eta))$. 4. 4)

For every $x\in\mathit{Var}$ with $\mathtt{vExp}(x)=l+1$ we have $r_{\eta}(x)>0$ and $r_{\eta}(x)=r_{\eta^{\prime}}(x)$ for all $\eta^{\prime}\in\mathtt{layer}(l)$. 5. 5)

For every $x\in\mathit{Var}$ with $\mathtt{vExp}(x)>l+1$ we have $r_{\eta}(x)=0$. 6. 6)

For every $x\in\mathit{Var}$ with $\mathtt{vExp}(x)\leq l$ there is an ancestor $\eta^{\prime}\in\mathtt{layer}(i)$ of $\eta$ such that $r_{\eta^{\prime}}(x)>0$ and $r_{\eta^{\prime}}(x^{\prime})=0$ for all $x^{\prime}$ with $\mathtt{vExp}(x^{\prime})>\mathtt{vExp}(x)$.

For a vector $r\in\mathbb{Z}^{\mathit{Var}}$, we define the potential of $r$ by setting $\mathtt{pot}(r)=\max\{\mathtt{vExp}(x)\mid x\in\mathit{Var},r(x)\neq 0\}$, where we set $\max\emptyset=0$. The motivation for this definition is that we have $r^{T}\nu\in O(N^{\mathtt{pot}(r)})$ for every valuation $\nu$ reachable by a trace $\zeta$ with $\mathtt{init}(\zeta)\leq N$. We will now define the potential of a set of vectors $Z\subseteq\mathbb{Z}^{\mathit{Var}}$. Let $M$ be a matrix whose columns are the vectors of $Z$ and whose rows are ordered according to the variable bounds, i.e., if the row associated to variable $x^{\prime}$ is above the row associated to variable $x$, then we have $\mathtt{vExp}(x^{\prime})\geq\mathtt{vExp}(x)$. Let $L$ be some lower triangular matrix obtained from $M$ by elementary column operations. We now define $\mathtt{pot}(Z)=\sum_{\text{column }r\text{ of }L}\mathtt{pot}(r)$, where we set $\sum\emptyset=0$. We note that $\mathtt{pot}(Z)$ is well-defined, because the value $\mathtt{pot}(Z)$ does not depend on the choice of $M$ and $L$.

We next state an upper bound on potentials. Let $l\geq 0$ and let $B_{l}=\{\mathtt{vExp}(x)\mid x\in\mathit{Var},\mathtt{vExp}(x)<l\}$ be the set of variable bounds below $l$. We set $\mathtt{varsum}(l)=1$, for $B_{l}=\emptyset$, and $\mathtt{varsum}(l)=\sum B_{l}$, otherwise. The following statement is a direct consequence of the definitions:

Proposition 3

Let $Z\subseteq\mathbb{Z}^{\mathit{Var}}$ be a set of vectors such that $r(x)=0$ for all $r\in Z$ and $x\in\mathit{Var}$ with $\mathtt{vExp}(x)>l$. Then, we have $\mathtt{pot}(Z)\leq\mathtt{varsum}(l+1)$.

We define $\mathtt{pot}(\eta)=\mathtt{pot}(\{r_{\eta^{\prime}}\mid\eta^{\prime}\text{ is a strict ancestor }\text{ of }\eta\})$ as the potential of a node $\eta$. We note that $\mathtt{pot}(\eta)\leq\mathtt{varsum}(l+1)$ for every node $\eta\in\mathtt{layer}(l)$ by Proposition 3. Now, we are able to state the main results of this section:

Lemma 9

Let $\eta$ be a node in $T$. Then, every trace $\zeta$ with $\mathtt{init}(\zeta)\leq N$ enters $\mathtt{VASS}(\eta)$ at most $O(N^{\mathtt{pot}(\eta)})$ times, i.e., $\zeta$ contains at most $O(N^{\mathtt{pot}(\eta)})$ transitions $s\xrightarrow{d}s^{\prime}$ with $s\not\in\mathit{St}(\mathtt{VASS}(\eta))$ and $s^{\prime}\in\mathit{St}(\mathtt{VASS}(\eta))$.

Lemma 10

For every layer $l$, we have that $\mathtt{vExp}(x)=l$ resp. $\mathtt{tExp}(t)=l$ implies $\mathtt{vExp}(x)\leq\mathtt{varsum}(l)$ resp. $\mathtt{tExp}(t)\leq\mathtt{varsum}(l)$.

The next result follows from Lemma 10 only by arithmetic manipulations and induction on $l$:

Lemma 11

Let $l$ be some layer. Let $k$ be the number of variables $x\in\mathit{Var}$ with $\mathtt{vExp}(x)<l$. Then, $\mathtt{varsum}(l)\leq 2^{k}$.

Theorem 4.3 is then a direct consequence of Lemma 10 and 11 (using $k\leq|\mathit{Var}|$).

8 Exponential Witness

The following lemma from [15] states a condition that is sufficient for a VASS to have exponential complexity222Our formalization differs from[15], but it is easy to verify that our conditions a) and b) are equivalent to the conditions on the cycles in the ‘iteration schemes’ of [15].. We will use this lemma to prove Theorem 4.1:

Lemma 12 (Lemma 10 of [15])

Let $\mathcal{V}$ be a connected VASS, let $U,W$ be a partitioning of $\mathit{Var}$ and let $C_{1},\ldots,C_{m}$ be cycles such that a) $\mathit{val}(C_{i})(x)\geq 0$ for all $x\in U$ and $1\leq i\leq m$, and b) $\sum_{i}\mathit{val}(C_{i})(x)\geq 1$ for all $x\in W$. Then, there is a $c>1$ and paths $\pi_{N}$ such that 1) $\pi_{N}$ can be executed from initial valuation $N\cdot\mathbf{1}$, 2) $\pi_{N}$ reaches a valuation $\nu$ with $\nu(x)\geq c^{N}$ for all $x\in W$ and 3) $(C_{i})^{c^{N}}$ is a sub-path of $\pi_{N}$ for each $1\leq i\leq m$.

We now outline the proof of Theorem 4.1: We assume that Algorithm 1 returned “$\mathcal{V}$ has at least exponential complexity” in loop iteration $l$. According to Lemma 8, there are cycles $C(\eta)$, for every node $\eta\in\mathtt{layer}(l)$, that contain $\mu(t)$ instances of every transition $t\in\mathit{Trns}(\mathtt{VASS}(\eta))$. One can then show that the cycles $C(\eta)$ and the sets $U=\{x\in\mathit{Var}\mid\mathtt{vExp}(x)\leq l\}$, $W=\{x\in\mathit{Var}\mid\mathtt{vExp}(x)>l\}$ satisfy the requirements of Lemma 12, which establishes Theorem 4.1.

Appendix 0.A Proof of Lemma 1

Proof

”$\Leftarrow$”: We consider some multi-cycle $M$ with $\mu(t)$ instances of each transition $t$ and $\mathit{val}(M)\geq 0$. Clearly, $\mu\geq 0$ because the number of instances of a transition is always non-negative. Because of $\mathit{val}(M)\geq 0$ and $\mathit{val}(M)=D\mu$, we have $D\mu\geq 0$. Because $M$ is a multi-cycle we have that $\mu$ satisfies the flow constraint $F\mu=0$, which encodes for every state that the number of incoming transitions equals the number of out-going transitions.

”$\Rightarrow$”: We assume that $\mu$ is a solution to constraint system ($P$). Hence, we have $\mu\geq 0$. We now consider the multi-graph which contains $\mu(t)$ copies of every transition $t$. From the flow constraint $F\mu=0$ we have that the multi-graph is balanced, i.e., the number of incoming edges equals the number of outgoing edges for every state. It follows that every strongly connected component has an Eulerian cycle. Each of these Eulerian cycles gives us a cycle in the original VASS. The union of these cycles is the desired multi-cycle because we have $D\mu\geq 0$ by assumption. ∎

Appendix 0.B Proof of Lemma 2

Proof

The first item holds because $r,z$ satisfy the constraints $r\geq 0$ and $z\geq 0$ of constraint system ($Q$).

For the second item, we consider a transition $t=s_{1}\xrightarrow{d}s_{2}\in\mathit{Trns}(\mathcal{V})$ and valuations $\nu_{1},\nu_{2}\in\mathit{Val}(\mathcal{V})$ with $\nu_{2}=\nu_{1}+d$. We have $\mathit{rank}(r,z)(s_{2},\nu_{2})=r^{T}\nu_{2}+z(s_{2})=r^{T}(\nu_{1}+d)+z(s_{2})=r^{T}\nu_{1}+r^{T}d+z(s_{2})=r^{T}\nu_{1}+z(s_{1})+d^{T}r+z(s_{2})-z(s_{1})\leq r^{T}\nu_{1}+z(s_{1})=\mathit{rank}(r,z)(s_{1},\nu_{1})$, where we have the inequality because $r,z$ satisfies the constraint $D^{T}r+F^{T}z\leq 0$ of constraint system ($Q$). We further observe that the inequality is strict for every $t$ with $(D^{T}r+F^{T}z)(t)<0$. ∎

Appendix 0.C Proof of Lemma 3

The proof of Lemma 3 will be obtained by two applications of Farkas’ Lemma. We will employ the following version of Farkas’ Lemma, which states that for matrices $A$,$C$ and vectors $b$,$d$, exactly one of the following statements is true:

[TABLE]

We now consider the constraint systems ($A_{t}$) and ($B_{t}$) stated below. Both constraint systems are parameterized by a transition $t\in\mathit{Trns}(\mathcal{V})$ (we note that only Equations (1) and (2) are parameterized by $t$).

[TABLE]

We recognize constraint system ($A_{t}$) as the dual of constraint system ($B_{t}$) in the following Lemma:

Lemma 13

Exactly one of the constraint systems ($A_{t}$) and ($B_{t}$) has a solution.

Proof

We fix some transition $t$. We denote by $\mathtt{char}_{t}\in\mathbb{Z}^{\mathit{St}(\mathcal{V})}$ the vector with $\mathtt{char}_{t}(t^{\prime})=1$, if $t^{\prime}=t$, and $\mathtt{char}_{t}(t^{\prime})=0$, otherwise. Using this notation we rewrite ($A_{t}$) to the equivalent constraint system ($A_{t}^{\prime}$):

[TABLE]

Using Farkas’ Lemma, we see that either ($A_{t}^{\prime}$) is satisfiable or the following constraint system ($B_{t}^{\prime}$) is satisfiable:

[TABLE]

We observe that solutions of constraint system ($B_{t}^{\prime}$) are invariant under shifts of $z$, i.e, if $r$, $y$, $z$ is a solution, then $r$, $y$, $z+c\cdot\mathbf{1}$ is also a solution for all $c\in\mathbb{Z}$ (because every row of $F^{T}$ either contains exactly one $-1$ and $1$ entry or only [math] entries). Hence, we can force $z$ to be non-negative. We recognize that constraint systems ($B_{t}^{\prime}$) and ($B_{t}$) are equivalent. ∎

We now consider the constraint systems ($C_{x}$) and ($D_{x}$) stated below. Both constraint systems are parameterized by a variable $x\in\mathit{Var}$ (we note that only Equations (3) and (4) are parameterized by $x$).

[TABLE]

We recognize constraint system ($C_{x}$) as the dual of constraint system ($D_{x}$) in the following Lemma:

Lemma 14

Exactly one of the constraint systems ($C_{x}$) and ($D_{x}$) has a solution.

Proof

We fix some variable $x\in\mathit{Var}$. We denote by $\mathtt{char}_{x}\in\mathbb{Z}^{\mathit{Var}}$ the vector with $\mathtt{char}_{x}(x^{\prime})=1$, if $x^{\prime}=x$, and $\mathtt{char}_{x}(x^{\prime})=0$, otherwise. Using this notation we rewrite ($A_{x}$) to the equivalent constraint system ($A_{x}^{\prime}$):

[TABLE]

Using Farkas’ Lemma, we see that either ($C_{x}^{\prime}$) is satisfiable or the following constraint system ($D_{x}^{\prime}$) is satisfiable:

[TABLE]

We observe that solutions of constraint system ($D_{x}^{\prime}$) are invariant under shifts of $z$, i.e, if $r$, $y$, $z$ is a solution, then $r$, $y$, $z+c\cdot\mathbf{1}$ is also a solution for all $c\in\mathbb{Z}$ (because every row of $F^{T}$ either contains exactly one $-1$ and $1$ entry or only [math] entries). Hence, we can force $z$ to be non-negative. We recognize that constraint systems ($D_{x}^{\prime}$) and ($D_{x}$) are equivalent. ∎

We are now ready to state the proof of Lemma 3:

Proof

We consider optimal solutions $\mu$ and $r$,$z$ to constraint systems ($P$) and ($Q$). The claim then directly follows from Lemma 13 and Lemma 14. ∎

Appendix 0.D Proof of Lemma 4

Proof

By Lemma 1 there is a multi-cycle $M$ with $\mu(t)$ instances of every transition $t\in U$. By Lemma 3 we have $U\setminus R=\{t\in U\mid\mu(t)\geq 1\}$. Hence, every transition $t\in U\setminus R$ is part of a cycle that uses only edges from $U\setminus R$. Thus, every transition $t\in U\setminus R$ must belong to some SCC of $(\mathit{St}(\mathtt{VASS}(\eta)),\mathit{Trns}(\mathtt{VASS}(\eta))\setminus R)$ for some $\eta\in\mathtt{layer}(l-1)$. We get that $U\setminus R=\bigcup_{\eta\in\mathtt{layer}(l)}\mathit{Trns}(\mathtt{VASS}(\eta))$.

Appendix 0.E Proof of Lemma 5

Proof

We note that $l$ is incremented in every iteration of Algorithm 1. Hence, if the values of $\mathtt{vExp}$ and $\mathtt{tExp}$ are not changed, then the condition ‘there are no $t\in\mathit{Trns}(\mathcal{V})$, $x\in\mathit{Var}$ with $l<\mathtt{tExp}(t)+\mathtt{vExp}(x)<\infty$’ will eventually become true. Hence, Algorithm 1 either terminates after finitely many iterations or there is a change in the values of $\mathtt{vExp}$ and $\mathtt{tExp}$. Now we recall that the value of $\mathtt{vExp}(x)$ and $\mathtt{tExp}(t)$ is changed at most once for every $t\in\mathit{Trns}(\mathcal{V})$ and $x\in\mathit{Var}$. Hence, Algorithm 1 must terminate after finitely many iterations. ∎

Appendix 0.F Proof of Corollary 1

Proof

We consider the run of Algorithm 1 on $\mathcal{V}$. In case Algorithm 1 returns “$\mathcal{V}$ has at least exponential complexity”, then $\mathit{comp}_{\mathcal{V}}(N)\in 2^{\Omega(N)}$ by Theorem 4.1. Otherwise, we have $\mathtt{tExp}(t)\neq\infty$ and $\mathtt{vExp}(x)\neq\infty$ for all $t\in\mathit{Trns}(\mathcal{V})$ and $x\in\mathit{Var}$. Let $i=\max_{t\in\mathit{Trns}(\mathcal{V})}\mathtt{tExp}(t)$. Using Theorem 4.2 we get that $\mathit{length}(\zeta)=\sum_{t\in\mathit{Trns}(\mathcal{V})}\mathtt{instance}(\zeta,t)\in O(N^{i})$ for every trace $\zeta$ of $\mathcal{V}$ with $\mathtt{init}(\zeta)\leq N$. Hence, $\mathit{comp}_{\mathcal{V}}(N)\in O(N^{i})$. For the lower bound, we consider a transition $t\in\mathit{Trns}(\mathcal{V})$ with $i=\mathtt{tExp}(t)$. From Theorem 4.2 we get that there are traces $\zeta_{N}$ of $\mathcal{V}$ with $\mathtt{init}(\zeta_{N})\leq N$ and $\mathtt{instance}(\zeta_{N},t)\in\Omega(N^{i})$. Because of $\mathtt{instance}(\zeta_{N},t)\leq\mathit{length}(\zeta_{N})$ for all $N\geq 0$, we get $\mathit{comp}_{\mathcal{V}}(N)\in\Omega(N^{i})$. Thus, we have shown $\mathit{comp}_{\mathcal{V}}(N)\in\Theta(N^{i})$. Finally, $i\leq 2^{|\mathit{Var}|}$ by Theorem 4.3. ∎

Appendix 0.G Proof of Lemma 6

Proof

We consider the point in time when the execution of Algorithm 1 reaches line $l:=l+1$ during some loop iteration $l\geq 1$. Let $\mathit{RelevantLayers}=\{\mathtt{tExp}(t)+\mathtt{vExp}(x)\mid x\in\mathit{Var},t\in\mathit{Trns}(\mathcal{V})\}$ and let $l^{\prime}=\min\{l^{\prime}\mid l^{\prime}>l,l^{\prime}\in\mathit{RelevantLayers}\}$.

We begin by stating the main consequence of the definition of $l^{\prime}$: For every variable $x\in\mathit{Var}$, every node $\eta\in\mathtt{layer}(l-\mathtt{vExp}(x))$ and every layer $l<i<l^{\prime}$ there is a node $\eta^{\prime}\in\mathtt{layer}(i-\mathtt{vExp}(x))$ such that $\mathtt{VASS}(\eta)=\mathtt{VASS}(\eta^{\prime})$ (+). Assume that this is not the case. Then there is a variable $x\in\mathit{Var}$, a node $\eta\in\mathtt{layer}(l-\mathtt{vExp}(x))$ and a transition $t\in\mathit{Trns}(\mathtt{VASS}(\eta))$ such that $l-\mathtt{vExp}(x)<\mathtt{tExp}(t)<l^{\prime}-\mathtt{vExp}(x)$. However, this implies $l<\mathtt{tExp}(t)+\mathtt{vExp}(x)<l^{\prime}$, which contradicts the definition of $l^{\prime}$.

Let $U=\bigcup_{\eta\in\mathtt{layer}(l-1)}\mathit{Trns}(\mathtt{VASS}(\eta))$ be the transitions, $\mathit{Var}_{\mathit{ext}}$ be the variables and let $D_{\mathit{ext}}$ be the update matrix considered by Algorithm 1 during loop iteration $l$. Let $\mu$ and $r$, $z$ be optimal solutions to constraint systems ($\mathit{I}$) and ($\mathit{II}$), and let $R=\{t\in U\mid(D_{\mathit{ext}}^{T}r+F|_{U}^{T}z)(t)<0\}$ be the transitions removed during loop iteration $l$. We set $U_{\circ}=U\setminus R$. By Lemma 4, we have $U_{\circ}=\bigcup_{\eta\in\mathtt{layer}(l)}\mathit{Trns}(\mathtt{VASS}(\eta))$. We define $\mu_{\circ}$ and $D_{\circ}$ as the restriction of $\mu$ and $D_{\mathit{ext}}$ to $U_{\circ}$, i.e., we set $\mu_{\circ}=\mu|_{U_{\circ}}$ and $D_{\circ}=D_{\mathit{ext}}|_{U_{\circ}}$. From Lemma 3 we get that $U_{\circ}=\{t\mid\mu(t)\geq 1\}$, and hence $D_{\mathit{ext}}\mu=D_{\circ}\mu_{\circ}$. From this and the fact that $\mu\in\mathbb{Z}^{U}$ is a solution to constraint system ($\mathit{I}$) we get that $D_{\circ}\mu_{\circ}\geq 0$, $\mu_{\circ}\geq\mathbf{1}$ and $F|_{U_{\circ}}\mu_{\circ}=0$ (*). From Lemma 3 we further get that $(D_{\circ}\mu_{\circ})(x)=(D_{\mathit{ext}}\mu)(x)\geq 1$ for all variables $x$ with $\mathtt{vExp}(x)>l$ (#).

We now consider the layers $l\leq i<l^{\prime}$. We will show by induction that $U_{\circ}=\bigcup_{\eta\in\mathtt{layer}(i-1)}\mathit{Trns}(\mathtt{VASS}(\eta))$ for all $l\leq i<l^{\prime}$, and that $\mathtt{vExp}(x)\neq i$ and $\mathtt{tExp}(t)\neq i$ for all $l<i<l^{\prime}$, $x\in\mathit{Var}$ and $t\in\mathit{Trns}(\mathcal{V})$. For $i=l$ the statement trivially holds. We now consider some layer $l<i<l^{\prime}$. Layer $i$ is constructed from layer $i-1$ during loop iteration $i$. By induction assumption we have $U_{\circ}=\bigcup_{\eta\in\mathtt{layer}(i-1)}\mathit{Trns}(\mathtt{VASS}(\eta))$. During iteration $i$, thus, Algorithm 1 considers the update matrix $D_{i}\in\mathbb{Z}^{\mathit{Var}_{i}\times U_{\circ}}$ for the set of (extended) variables $\mathit{Var}_{i}=\{(x,\eta)\mid\eta\in\mathtt{layer}(i-\mathtt{vExp}(x))\}$. From (+) we have that there is a bijective function $f:\mathit{Var}_{\mathit{ext}}\rightarrow\mathit{Var}_{i}$ with $f(x,\eta)=(x^{\prime},\eta^{\prime})$ if and only if $x=x^{\prime}$ and $\mathtt{VASS}(\eta)=\mathtt{VASS}(\eta^{\prime})$. Hence, we have $f(D_{\circ})=D_{i}$ 333For a function $f:I\rightarrow K$ and a matrix $A\in\mathbb{S}^{I\times J}$ we denote by $f(A)\in\mathbb{S}^{K\times J}$ the matrix defined by $f(A)(i,j)=A(f(i),j)$ for all $i,j\in I\times J$., i.e., the matrices $D_{i}$ and $D_{\circ}$ are identical up to renaming of the variables. Thus, from (*) we get that $D_{i}\mu_{\circ}\geq 0$, $\mu_{\circ}\geq\mathbf{1}$ and $F|_{U_{\circ}}\mu_{\circ}=0$, i.e., we have that $\mu_{\circ}$ is a solution to constraint system ($\mathit{I}$) during loop iteration $i$. Hence, by Lemma 3 we have that $D_{i}^{T}r+F|_{U_{\circ}}^{T}z=0$ for every optimal solution $r$, $z$ to constraint system ($\mathit{II}$), i.e., no transition is removed during loop iteration $i$. Thus, we get $U_{\circ}=\bigcup_{\eta\in\mathtt{layer}(i)}\mathit{Trns}(\mathtt{VASS}(\eta))$ and $\mathtt{tExp}(t)\neq i$ for all $t\in\mathit{Trns}(\mathcal{V})$. Further, by (#) we have that $(D_{i}\mu_{\circ})(x)\geq 1$ for all variables $x$ with $\mathtt{vExp}(x)>l$. Again by Lemma 3 we have for every variable $x$ with $\mathtt{vExp}(x)>l$ and every optimal solution $r$, $z$ to constraint system ($\mathit{II}$) that $r(x,\iota)=0$, i.e., $\mathtt{vExp}(x)\neq i$ for all $x\in\mathit{Var}$. ∎

Appendix 0.H Proof of Theorem 5.1

Proof

We prove the claim by induction on loop iteration $l$ of Algorithm 1. We consider some $l\geq 1$. Let $U=\bigcup_{\eta\in\mathtt{layer}(l-1)}\mathit{Trns}(\mathtt{VASS}(\eta))$ be the transitions, $\mathit{Var}_{\mathit{ext}}$ be the set of extended variables and $D_{\mathit{ext}}\in\mathbb{Z}^{\mathit{Var}_{\mathit{ext}}\times U}$ be the update matrix considered by Algorithm 1 during loop iteration $l$. For every transition $t\in\mathit{Trns}(\mathcal{V})\setminus U$ we have $\mathtt{tExp}(x)<l$, and hence we can assume $\mathtt{tbound}_{N}(t)\in O(N^{\mathtt{tExp}(t)})$ by the induction assumption. Further, we can apply the induction assumption for variables $x\in\mathit{Var}$ with $\mathtt{vExp}(x)<l$ and assume $\mathtt{vbound}_{N}(x)\in O(N^{\mathtt{vExp}(x)})$. Let $r,z$ be some optimal solution to constraint system ($\mathit{II}$) computed by Algorithm 1 during loop iteration $l$. As discussed earlier, we define the witness function $w$ using the quasi-ranking function from Lemma 2. We note that we have

[TABLE]

We have already argued that $w$ maps configurations to the non-negative integers, that condition 1) of the Bound Proof Principle is satisfied, and that the witness function $w$ decreases for transitions $t$ with $\mathtt{tExp}(t)=l$ (*). It remains to establish condition 2) of the Bound Proof Principle. We will show that there are increase certificates $\mathtt{inc}_{t}(N)\in O(N^{l-\mathtt{tExp}(t)})$ for all transitions $t\in\mathit{Trns}(\mathcal{V})\setminus U$.

We fix some transition $t\in\mathit{Trns}(\mathcal{V})\setminus U$. Let $(s_{1},\nu_{1})\xrightarrow{d}(s_{2},\nu_{2})$ be a step with $s_{1}\xrightarrow{d}s_{2}=t$ in a trace $\zeta$ of $\mathcal{V}$ with $\mathtt{init}(\zeta)\leq N$. We note that $\nu_{2}=\nu_{1}+d$. We will now show that $w(s_{2},\nu_{2})-w(s_{1},\nu_{1})\in O(N^{l-\mathtt{tExp}(t)})$, which is sufficient to conclude that there is an increase certificate $\mathtt{inc}_{t}$ with $\mathtt{inc}_{t}(N)\in O(N^{l-\mathtt{tExp}(t)})$.

Let $(x,\eta)\in\mathit{Var}_{\mathit{ext}}$ be a variable with $\mathtt{vExp}(x)\leq l-\mathtt{tExp}(t)$. For both $i=1$ or $i=2$, we consider the extended valuation $\mathtt{ext}_{s_{i}}(\nu_{i})(x,\eta)$. In case of $s_{i}\in\mathit{St}(\mathtt{VASS}(\eta))$ we have $\mathtt{ext}_{s_{i}}(\nu_{i})(x,\eta)=\nu_{i}(x)\in O(N^{\mathtt{vExp}(x)})$ because of $\mathtt{vExp}(x)\leq l-\mathtt{tExp}(t)<l$, using the induction assumption for $x$. In case of $s_{i}\not\in\mathit{St}(\mathtt{VASS}(\eta))$ we have $\mathtt{ext}_{s_{i}}(\nu_{i})(x,\eta)=0$. The case analysis allow us to conclude that $\mathtt{ext}_{s_{2}}(\nu_{2})(x,\eta)-\mathtt{ext}_{s_{1}}(\nu_{1})(x,\eta)\in O(N^{\mathtt{vExp}(x)})$.

Let $(x,\eta)\in\mathit{Var}_{\mathit{ext}}$ be a variable with $\mathtt{vExp}(x)>l-\mathtt{tExp}(t)$. We note there is a unique node $\eta^{\prime}\in\mathtt{layer}(l-\mathtt{vExp}(x))$ in layer such that $t\in\mathit{Trns}(\mathtt{VASS}(\eta))$ (because of $\mathtt{tExp}(t)>l-\mathtt{vExp}(x)$). In case of $\eta=\eta^{\prime}$, we have $s_{1},s_{2}\in\mathit{St}(\mathtt{VASS}(\eta))$, and hence $\mathtt{ext}_{s_{2}}(\nu_{2})(x,\eta)=\nu_{2}(x)=\nu_{1}(x)+d(x)=\mathtt{ext}_{s_{1}}(\nu_{1})(x,\eta)+d(x)$. In case of $\eta\neq\eta^{\prime}$, we have $s_{1},s_{2}\not\in\mathit{St}(\mathtt{VASS}(\eta))$ because $\mathtt{VASS}(\eta)$ is disjoint from $\mathtt{VASS}(\eta^{\prime})$, and hence $\mathtt{ext}_{s_{2}}(\nu_{2})(x,\eta)=\mathtt{ext}_{s_{1}}(\nu_{1})(x,\eta)=0$. In both cases we get $\mathtt{ext}_{s_{2}}(\nu_{2})(x,\eta)-\mathtt{ext}_{s_{1}}(\nu_{1})(x,\eta)\in O(1)$.

Using the above stated facts, we obtain

[TABLE]

We are now ready to apply the Bound Proof Principle from Proposition 1. We observe that

[TABLE]

because $w(s,\nu)=r^{T}\mathtt{ext}_{s}(\nu)+z(s)$ is a linear expression for all $s\in\mathit{St}(\mathcal{V})$, and we consider valuations $\nu$ with $\left\lVert\nu\right\rVert\leq N$. Further, by the above, we have

[TABLE]

using the induction assumption for $t\in\mathit{Trns}(\mathcal{V})\setminus U$. With (*) we can now conclude from the Bound Proof Principle that $\mathtt{tbound}_{N}(t)\in O(N^{l})$ for all transitions $t$ with $\mathtt{tExp}(t)=l$. Next, we argue that we can also deduce the desired variable bounds. We recall that for each variable $x$ with $\mathtt{vExp}(x)=l$ we have $r(x,\iota)>0$. Hence, $w(s,\nu)=r^{T}\mathtt{ext}_{s}(\nu)+z(s)\geq r(x,\iota)\cdot\nu(x)\geq\nu(x)$ for all $(s,\nu)\in\mathit{Cfg}(\mathcal{V})$. Thus, we can conclude from the Bound Proof Principle that $\mathtt{vbound}_{N}(x)\in O(N^{l})$ for all variables $x$ with $\mathtt{vExp}(x)=l$. ∎

Appendix 0.I Proof of Lemma 7

Proof

Assume that there is a $c>0$ and that there are traces $\zeta_{N}$ with $\mathtt{init}(\zeta_{N})\leq cN$ and $\mathtt{instance}(\pi_{N},t)\geq N^{i}$. We set $N^{\prime}=cN$. We get that there are traces $\zeta_{N^{\prime}}$ with $\mathtt{init}(\zeta_{N^{\prime}})\leq N^{\prime}$ and $\mathtt{instance}(\zeta_{N^{\prime}},t)\geq(\frac{1}{c})^{i}N^{\prime i}$. Hence, $\mathtt{tbound}_{N}(t)\in\Omega(N^{i})$. The second claim can be shown analogously. ∎

Appendix 0.J Proof of Lemma 8

Proof

Let $U\setminus R=\bigcup_{\eta\in\mathtt{layer}(l)}\mathit{Trns}(\mathtt{VASS}(\eta))$ be the transition of the layer constructed during loop iteration $l$ of Algorithm 1. As we have argued in the proof of Lemma 4, we have $U\setminus R=\{t\mid\mu(t)\geq 1\}$ and there is a multi-cycle $M$ with $\mu(t)$ instances of every transition $t\in U$. Because the $\mathtt{VASS}(\eta)$ of the nodes $\eta$ in layer $l$ are disjoint, we have that the transitions of every cycle of $M$ belong to only a single set $\mathit{Trns}(\mathtt{VASS}(\eta))$ for some $\eta\in\mathtt{layer}(l)$. We can now shuffle all cycles that use transitions from the same $\mathtt{VASS}(\eta)$ into a single cycle. We obtain a single cycle for each $\eta\in\mathtt{layer}(l)$ that uses exactly $\mu(t)$ instances of every transition $t\in\mathit{Trns}(\mathtt{VASS}(\eta))$. ∎

Appendix 0.K Proof of Theorem 6.1

We will need the following two properties about pre-paths:

Proposition 4

Let $\sigma$ be a pre-path that can be obtained by shuffling the two pre-paths $\sigma_{a}$ and $\sigma_{b}$. If $\sigma_{a}$ resp. $\sigma_{b}$ are executable from some valuation $\nu_{a}$ resp. $\nu_{b}$, then $\sigma$ is executable from valuation $\nu_{a}+\nu_{b}$; moreover, if $\sigma_{a}$ reaches a valuation $\nu_{a}^{\prime}$ from $\nu_{a}$ and $\sigma_{b}$ reaches a valuation $\nu_{b}^{\prime}$ from $\nu_{b}$, then $\sigma$ reaches valuation $\nu_{a}^{\prime}+\nu_{b}^{\prime}$ from $\nu_{a}+\nu_{b}$.

Proof

Let $\sigma_{a}=t_{1}\cdots t_{k}$ resp. $\sigma_{b}=t_{1}^{\prime}\cdots t_{l}^{\prime}$ be the sequences of transitions $t_{i}=s_{i}\xrightarrow{d_{i}}s_{i+1}$ resp. $t_{i}^{\prime}=s^{\prime}_{i}\xrightarrow{d_{i}^{\prime}}s_{i+1}^{\prime}$. By assumption there are injective monotone functions $f:[1,k]\rightarrow[1,k+l]$ and $g:[1,l]\rightarrow[1,k+l]$ with $f([1,k])\cap g([1,l])=\emptyset$ that define $\sigma=t_{1}^{\prime\prime}\cdots t_{k+l}^{\prime\prime}$, i.e., we have $t_{f(i)}^{\prime\prime}=t_{i}$ for all $i\in[1,k]$ and $t_{g(i)}^{\prime\prime}=t_{i}^{\prime}$ for all $i\in[1,l]$. We define functions $u(i)=\max\{h\in[1,k]\mid f(h)\leq i\}$ and $v(i)=\max\{h\in[1,l]\mid g(h)\leq i\}$ for all $0\leq i\leq l+k$, where we set $\max\emptyset=0$. Because $\sigma_{a}$ resp. $\sigma_{b}$ are executable from some valuation $\nu_{a}$ resp. $\nu_{b}$, there are valuations $\nu_{i}\geq 0$ and $\nu_{i}^{\prime}\geq 0$ such that $\nu_{a}=\nu_{0}$ and $\nu_{i+1}=\nu_{i}+d_{i+1}$ for all $0\leq i<k$ as well as $\nu_{b}=\nu_{0}^{\prime}$ and $\nu_{i+1}^{\prime}=\nu_{i}^{\prime}+d_{i+1}^{\prime}\geq 0$ for all $0\leq i<l$. We now set $\nu_{i}^{\prime\prime}=\nu_{u(i)}+\nu_{v(i)}^{\prime}$ for all $0\leq i\leq k+l$. We observe $\nu_{0}^{\prime\prime}=\nu_{u(0)}+\nu_{v(0)}^{\prime}=\nu_{a}+\nu_{b}$ and $\nu_{k+l}^{\prime\prime}=\nu_{u(k+l)}+\nu_{v(k+l)}^{\prime}=\nu_{a}^{\prime}+\nu_{b}^{\prime}$. Clearly, $\nu_{i}^{\prime\prime}\geq 0$ for all $1\leq i\leq k+l$. We now observe that either $u(i)=u(i+1)$ and $v(i)\neq v(i+1)$ or $u(i)\neq u(i+1)$ and $v(i)=v(i+1)$ for all $0\leq i<k+l$. In particular, $\nu_{i+1}^{\prime\prime}=\nu_{u(i+1)}+\nu_{v(i+1)}^{\prime}=\nu_{u(i)}+d_{u(i+1)}+\nu_{v(i)}^{\prime}=\nu_{i}^{\prime\prime}+d_{u(i+1)}$ or $\nu_{i+1}^{\prime\prime}=\nu_{u(i+1)}+\nu_{v(i+1)}^{\prime}=\nu_{u(i)}+\nu_{v(i)}^{\prime}+d_{v(i+1)}^{\prime}=\nu_{i}^{\prime\prime}+d_{u(i+1)}$ for all $0\leq i<k+l$. Hence, the claim holds. ∎

Proposition 5

Let $U,W$ be a partitioning of $\mathit{Var}$. Let $d\geq 1$ be a natural number and let $\sigma$ be a pre-path such that $\mathit{val}(\sigma)(x)\geq 0$ for all $x\in U$. If $\sigma$ can be executed from some valuation $\nu$, then $\sigma^{d}$ can be executed from valuation $\nu_{d}$ with $\nu_{d}(x)=\nu(x)$ for $x\in U$, and $\nu_{d}(x)=d\nu(x)$, for $x\in W$.

Proof

Let $\nu$ be a valuation from which $\sigma$ can be executed and let $\nu^{\prime}$ be the valuation reached by $\sigma$ from $\nu$. Because of $\nu+\mathit{val}(\sigma)=\nu^{\prime}\geq 0$, we get that $\mathit{val}(\sigma)\geq-\nu$ (*).

We now prove the claim by induction on $d\geq 1$. Clearly the claim holds for $d=1$. We consider some $d>1$. Because of $\nu_{d}\geq\nu$ we have that $\sigma$ can be executed from valuation $\nu_{d}$. Let $\nu_{d}^{\prime}$ be the valuation reached from $\nu_{d}$ by executing $\sigma$. By (*) we have $\nu_{d}^{\prime}(x)\geq\nu_{d}(x)-\nu(x)=\nu_{d-1}(x)$ for all $x\in W$. Because of $\mathit{val}(\sigma)(x)\geq 0$ for all $x\in U$ we have $\nu_{d}^{\prime}(x)\geq\nu_{d}(x)=\nu(x)=\nu_{d-1}(x)$ for all $x\in U$. Hence, the claim follows from the induction assumption. ∎

0.K.1 Step I

The properties stated in the two lemmata below are needed for the construction of the pre-paths $\tau_{l}$ along the tree $T$. These properties are direct consequences of constraint system ($\mathit{I}$), and are the key ingredient for the lower bound proof.

Lemma 15

Let $0\leq i<l$ be some layers. For every $\eta\in\mathtt{layer}(i)$ and variable $x\in\mathit{Var}$ with $\mathtt{vExp}(x)\leq l-i$ we have

[TABLE]

Proof

We first start with a statement that will be helpful to prove the claim. Let $x\in\mathit{Var}$ be a variable with $\mathtt{vExp}(x)\leq l$. Let $\mu$ be the optimal solution to constraint system ($\mathit{I}$) during loop iteration $l$ of Algorithm 1. We consider some node $\eta_{\circ}\in\mathtt{layer}(l-\mathtt{vExp}(x))$ in layer $l-\mathtt{vExp}(x)$ of $T$. Because $\mu$ is a solution to ($\mathit{I}$) we have that

[TABLE]

We recall that we have $\mathit{val}(C(\eta))=\sum_{t\in\mathit{Trns}(\mathtt{VASS}(\eta))}D(t)\cdot\mu(t)$ for all $\eta\in\mathtt{layer}(l)$ by the definition of the cycles $C(\eta)$. With (*) we get

[TABLE]

We are now ready to prove the claim. We now consider some node $\eta\in\mathtt{layer}(i)$ and some variable $x\in\mathit{Var}$ with $\mathtt{vExp}(x)\leq l-i$. We have

[TABLE]

where we have the last inequality from (#). ∎

Lemma 16

Let $l\geq 1$ be a layer. Then we have

[TABLE]

for variables $x\in\mathit{Var}$ with $\mathtt{vExp}(x)>l$.

Proof

Let $x\in\mathit{Var}$ be some variable with $\mathtt{vExp}(x)>l$. Let $\mu$ and $r,z$ be the optimal solutions to constraint systems ($\mathit{I}$) and ($\mathit{II}$) during loop iteration $l$ of Algorithm 1. Because $\mu$ is a solution to ($\mathit{I}$) we have that

[TABLE]

Because of $\mathtt{vExp}(x)>l$ we must have $\mathtt{vExp}(x)=\infty$ during iteration $l$ of Algorithm 1. We now observe that we must have $r(x,\iota)=0$ (otherwise Algorithm 1 would set $\mathtt{vExp}(x):=l$ during loop iteration $l$, contradicting the assumption $\mathtt{vExp}(x)>l$). From the dichotomy stated in Lemma 3 we then get that the inequality (*) must be strict. Now the claim follows because of $\mathit{val}(C(\eta))=\sum_{t\in\mathit{Trns}(\mathtt{VASS}(\eta))}D(t)\cdot\mu(t)$ by definition of the cycles $C(\eta)$. ∎

For the construction of the pre-paths $\tau_{l}$, we need the following convention: For every layer $l\geq 0$ and every node $\eta\in\mathtt{layer}(l)$, we consider the cyclic path $C(\eta)$, and fix once and for all a decomposition $C(\eta)=\pi_{0}\pi_{1}\pi_{2}\cdots\pi_{d}$ and an ordering of the children $\eta_{1},\ldots,\eta_{d}$ of $\eta$ such that each $\pi_{j}$ has the same start state as $C(\eta_{j})$ (e.g., we can order the children $\eta_{1},\ldots,\eta_{d}$ of $\eta$ according to the first appearance of the start state of the path $C(\eta_{j})$ in the path $C(\eta)$).

We will now define the pre-paths $\tau_{l}$ along the structure of the tree $T$. In order to do so, we will define pre-paths $\sigma_{l}(\eta)$ for all layers $l\geq 1$ and nodes $\eta\in\mathtt{layer}(i)$ with $0\leq i\leq l$. We will then set $\tau_{l}=\sigma_{l}(\iota)^{N}$ for all layers $l\geq 1$.

We define the pre-paths $\sigma_{l}(\eta)$ inductively, starting from $i=l$ downto $i=0$. For $\eta\in\mathtt{layer}(l)$ we set $\sigma_{l}(\eta)=C(\eta)$. We now consider some $\eta\in\mathtt{layer}(i)$ with $0\leq i<l$. Let $C(\eta)=\pi_{0}\pi_{1}\pi_{2}\cdots\pi_{d}$ be the fixed decomposition and $\eta_{1},\ldots,\eta_{d}$ the corresponding ordering of the children of $\eta$ such that each $\pi_{j}$ has the same start state as $C(\eta_{j})$. We set $\sigma_{l}(\eta)=\sigma_{l}(\eta_{1})^{N}\sigma_{l}(\eta_{2})^{N}\cdots\sigma_{l}(\eta_{d})^{N}$. We now set $\tau_{l}=\sigma_{l}(\iota)^{N}$ for all layers $l\geq 1$.

We show the following properties of the pre-paths $\sigma_{l}(\eta)$:

Lemma 17

For all $l\geq 1$ and nodes $\eta\in\mathtt{layer}(i)$ with $0\leq i\leq l$ we have:

For every $\eta^{\prime}\in\mathtt{layer}(l)$ that is a descendant of $\eta$ and every transition $t\in\mathit{Trns}(\mathtt{VASS}(\eta^{\prime}))$ we have $\mathtt{instance}(\sigma_{l}(\eta),t)\geq N^{l-i}$ . 2. 2)

$\mathit{val}(\sigma_{l}(\eta))=N^{l-i}\sum_{\eta^{\prime}\in\mathtt{layer}(l),\eta^{\prime}\text{ is descendent of }\eta}\mathit{val}(C(\eta^{\prime}))$* .* 3. 3)

$\mathit{val}(\sigma_{l}(\eta))(x)\geq 0$* for every $x\in\mathit{Var}$ with $\mathtt{vExp}(x)\leq l-i$.* 4. 4)

$\sigma_{l}(\eta)$* is executable from some valuation $\nu$ with*

1. a)

$\nu(x)\in O(N^{\mathtt{vExp}(x)})$* for $x\in\mathit{Var}$ with $\mathtt{vExp}(x)\leq l-i$, and* 2. b)

$\nu(x)\in O(N^{l-i})$* for $x\in\mathit{Var}$ with $\mathtt{vExp}(x)\geq l-i+1$.*

Proof

We prove the properties for nodes $\eta\in\mathtt{layer}(i)$ by induction, starting from $i=l$ downto $i=0$.

Assume $i=l$: We fix some $\eta\in\mathtt{layer}(l)$. We have that $\sigma_{l}(\eta)=C(\eta)$ contains at least one instance of each transition $t\in\mathit{Trns}(\mathtt{VASS}(\eta))$. Hence, Property 1) holds. We have $\mathit{val}(\sigma_{l}(\eta))=\mathit{val}(C(\eta))$ because of $\sigma_{l}(\eta)=C(\eta)$. Hence, Property 2) holds. We note that $\mathtt{vExp}(x)>l-i=0$ for all variables $x\in\mathit{Var}$ (). Hence, Property 3) trivially holds. Because of (), we only have to establish 44b). We observe that there is a $c>0$ such that $\sigma_{l}(\eta)=C(\eta)$ can be executed from valuation $c\cdot\mathbf{1}$. Hence, Property 4) holds.

Assume $i<l$: We fix some $\eta\in\mathtt{layer}(i)$. Let $C(\eta)=\pi_{0}\pi_{1}\pi_{2}\cdots\pi_{d}$ be the fixed decomposition and $\eta_{1},\ldots,\eta_{d}$ the corresponding ordering of the children of $\eta$ such that each $\pi_{j}$ has the same start state as $C(\eta_{j})$.

We show Property 1): By induction assumption we have for every $1\leq j\leq d$ and every node $\eta^{\prime}\in\mathtt{layer}(l)$ that is a descendant of $\eta_{j}$ that $\sigma_{l}(\eta_{j})$ contains at least $N^{l-i-1}$ instances of every $t\in\mathit{Trns}(\mathtt{VASS}(\eta^{\prime}))$. The claim then follows because $\sigma_{l}(\eta)$ contains $N$ copies of each $\sigma_{l}(\eta_{j})$.

We show Property 2): From the induction assumption we get $\mathit{val}(\sigma_{l}(\eta_{j}))=N^{l-i-1}\sum_{\eta^{\prime}\in\mathtt{layer}(l),\eta^{\prime}\text{ is descendent of }\eta_{j}}C(\eta^{\prime})$ for all $1\leq j\leq d$. Hence, we have $\mathit{val}(\sigma_{l}(\eta))=N\sum_{1\leq j\leq d}\mathit{val}(\sigma_{l}(\eta_{j}))=$

$N\sum_{1\leq j\leq d}N^{l-i-1}\sum_{\eta^{\prime}\in\mathtt{layer}(l),\eta^{\prime}\text{ is descendent of }\eta_{j}}\mathit{val}(C(\eta^{\prime}))=$

$N^{l-i}\sum_{1\leq j\leq d}\sum_{\eta^{\prime}\in\mathtt{layer}(l),\eta^{\prime}\text{ is descendent of }\eta_{j}}\mathit{val}(C(\eta^{\prime}))=$

$N^{l-i}\sum_{\eta^{\prime}\in\mathtt{layer}(l),\eta^{\prime}\text{ is descendent of }\eta}\mathit{val}(C(\eta^{\prime}))$, where the last equality holds because every $\eta^{\prime}$ that is a descendent of $\eta$ is also a descendent of some $\eta_{j}$.

We show Property 3): The property is a direct consequence of Property 2) and Lemma 15.

We show Property 4): By induction assumption we have that each $\sigma_{l}(\eta_{j})$ can be executed from some valuation $\nu_{j}$ with $\nu_{j}(x)\in O(N^{\mathtt{vExp}(x)})$, for $x\in\mathit{Var}$ with $\mathtt{vExp}(x)\leq l-i-1$, and $\nu_{j}(x)\in O(N^{l-i-1})$, otherwise. By Property 3) we have for each $\sigma_{l}(\eta_{j})$ that $\mathit{val}(\sigma_{l}(\eta_{j}))(x)\geq 0$ for every $x\in\mathit{Var}$ with $\mathtt{vExp}(x)\leq l-i-1$. With Proposition 5 we get that each $\sigma_{l}(\eta_{j})^{N}$ can be executed from some valuation $\nu_{j}$ with $\nu_{j}(x)\in O(N^{\mathtt{vExp}(x)})$, for $x\in\mathit{Var}$ with $\mathtt{vExp}(x)\leq l-i-1$, and $\nu_{j}(x)\in O(N^{l-i})$, otherwise. With Proposition 4 we get that $\sigma_{l}(\eta)=\sigma_{l}(\eta_{1})^{N}\sigma_{l}(\eta_{2})^{N}\cdots\sigma_{l}(\eta_{d})^{N}$ can be executed from some valuation $\nu$ with $\nu(x)\in O(N^{\mathtt{vExp}(x)})$, for $x\in\mathit{Var}$ with $\mathtt{vExp}(x)\leq l-i-1$, and $\nu(x)\in O(N^{l-i})$, otherwise. We note that the last statement implies Property 4). ∎

We show the following properties of the pre-paths $\tau_{l}$:

Lemma 18

For all $l\geq 1$ we have:

$\mathtt{instance}(\tau_{l},t)\geq N^{l+1}$* for all transitions $t\in\bigcup_{\eta\in\mathtt{layer}(l)}\mathit{Trns}(\mathtt{VASS}(\eta))$.* 2. 2)

$\mathit{val}(\tau_{l})=N^{l+1}\sum_{\eta\in\mathtt{layer}(l)}\mathit{val}(C(\eta^{\prime}))$. 3. 3)

$\mathit{val}(\tau_{l})(x)\geq 0$* for every $x\in\mathit{Var}$ with $\mathtt{vExp}(x)\leq l$.* 4. 4)

$\mathit{val}(\tau_{l})(x)\geq N^{l+1}$* for every $x\in\mathit{Var}$ with $\mathtt{vExp}(x)\geq l+1$.* 5. 5)

$\tau_{l}$* is executable from some valuation $\nu$ with*

1. a)

$\nu(x)\in O(N^{\mathtt{vExp}(x)})$* for $x\in\mathit{Var}$ with $\mathtt{vExp}(x)\leq l$, and* 2. b)

$\nu(x)\in O(N^{l})$* for $x\in\mathit{Var}$ with $\mathtt{vExp}(x)\geq l+1$.*

Proof

Let $l\geq 1$ be some layer. We consider the pre-path $\sigma_{l}(\iota)$. Using the fact that every node in layer $l$ is a descendant of the root node $\iota$, we get from Property 2) in Lemma 17 that $\mathit{val}(\sigma_{l}(\iota))=N^{l}\sum_{\eta\in\mathtt{layer}(l)}\mathit{val}(C(\eta))$ (*). From Lemma 16 we now get that $\mathit{val}(\sigma_{l}(\iota))(x)\geq N^{l}$ for every $x\in\mathit{Var}$ with $\mathtt{vExp}(x)\geq l+1$ (#). From Property 3) in Lemma 17 and (#) we get in particular that $\mathit{val}(\sigma_{l}(\iota))(x)\geq 0$ for all $x\in\mathit{Var}$ (+).

We recall that we defined $\tau_{l}=\sigma_{l}(\iota)^{N}$, i.e., that $\tau_{l}$ consists of $N$ copies of $\sigma_{l}(\iota)$. Then, Properties 1) and 3) directly follow from the corresponding properties in Lemma 17. Properties 2) and 4) follow from (*) and (#). Property 5) follows from Property 4 in Lemma 17 using (+) and Proposition 5. ∎

0.K.2 Step II

By Property 5) of Lemma 18 we can choose a sufficiently large $k>0$ such that every pre-path $\tau_{l}$, for $l\geq 1$, is executable from valuation $\nu_{l}$ with

1. a)

$\nu_{l}(x)=kN^{\mathtt{vExp}(x)}$ for $x\in\mathit{Var}$ with $\mathtt{vExp}(x)\leq l$, and 2. b)

$\nu_{l}(x)=kN^{l}$ for $x\in\mathit{Var}$ with $\mathtt{vExp}(x)\geq l+1$.

For every $l\geq 0$, we now define the pre-path $\rho_{l}=\tau_{0}^{k}\tau_{1}^{k}\tau_{2}^{k}\cdots\tau_{l}^{k}$ (the concatenation of $k$ copies of the pre-paths $\tau_{i}$ for all $0\leq i\leq l$), where we set $\tau_{0}=C(\iota)^{N}$.

The following lemma shows that the pre-path $\rho_{l_{\max}}$, where $l_{\max}$ is the maximal layer of $T$, would be sufficient to conclude the lower bound proof except that we will need to extend the proof from pre-paths to proper paths.

Lemma 19

For every $l\geq 0$, the pre-path $\rho_{l}$ can be executed from a valuation $\nu$ and reaches a valuation $\nu^{\prime}$ with

$\left\lVert\nu\right\rVert\in O(N)$, 2. 2)

$\nu^{\prime}(x)\geq kN^{\mathtt{vExp}(x)}$* for all $x\in\mathit{Var}$ with $\mathtt{vExp}(x)\leq l$, and* 3. 3)

$\nu^{\prime}(x)\geq kN^{l+1}$* for all $x\in\mathit{Var}$ with $\mathtt{vExp}(x)\geq l+1$.*

Proof

The proof proceeds by induction on $l$. We consider $l=0$. We have $\rho_{0}=\tau_{0}^{k}=C(\iota)^{kN}$. Clearly, there is a $c>0$ such that $C(\iota)^{kN}$ can be executed from valuation $cN\cdot\mathbf{1}$ such that $cN\cdot\mathbf{1}+kN\cdot\mathit{val}(C(\iota))\geq kN\cdot\mathbf{1}$. This establishes the base case.

We consider some $l\geq 1$ and assume the induction assumption for $\rho_{l-1}$. We observe that $\rho_{l}=\rho_{l-1}\tau_{l}^{k}$. By Property 2) of Lemma 18 we have $\mathit{val}(\tau_{l})=N^{l+1}\sum_{\eta\in\mathtt{layer}(l)}\mathit{val}(C(\eta))$. By Properties 3) and 4) of Lemma 18 we have $\tau_{l}(x)\geq 0$, for every $x\in\mathit{Var}$ with $\mathtt{vExp}(x)\leq l$, and $\mathit{val}(\tau_{l})(x)\geq N^{l+1}$ for every $x\in\mathit{Var}$ with $\mathtt{vExp}(x)\geq l+1$ (). Hence, we have $\mathit{val}(\tau_{l}^{k})(x)\geq 0$, for variables $x\in\mathit{Var}$ with $\mathtt{vExp}(x)\leq l$, and $\mathit{val}(\tau_{l}^{k})(x)\geq kN^{l+1}$, for $x\in\mathit{Var}$ with $\mathtt{vExp}(x)\geq l+1$. By the definition of $k$ we have that $\tau_{l}$ can be executed from valuation $\nu(x)=kN^{\mathtt{vExp}(x)}$, for $x\in\mathit{Var}$ with $\mathtt{vExp}(x)\leq l$, and $\nu(x)=kN^{l}$, for $x\in\mathit{Var}$ with $\mathtt{vExp}(x)\geq l+1$. By Proposition 5 and (), $\tau_{l}^{k}$ can be executed from valuation $\nu(x)=kN^{\mathtt{vExp}(x)}$, for $x\in\mathit{Var}$ with $\mathtt{vExp}(x)\leq l$, and $\nu(x)=kN^{l}$, for $x\in\mathit{Var}$ with $\mathtt{vExp}(x)\geq l+1$. Because of $\rho_{l}=\rho_{l-1}\tau_{l}^{k}$, the claim now follows from the induction assumption. ∎

0.K.3 Step III

In order to extend the proof from pre-paths to paths we make use of the concept of shuffling. For all $l\geq 0$, we will define paths $\gamma_{l}$ that can be obtained by shuffling the pre-paths $\rho_{0},\rho_{1},\ldots,\rho_{l}$.

We will first define paths $\beta_{l}$ analogously to the pre-paths $\tau_{l}$. We will then set $\gamma_{l}=\beta_{0}^{k}\beta_{1}^{k}\cdots\beta_{l}^{k}$ for all $l\geq 0$, where $k$ is the constant from Step II.

We will define the paths $\beta_{l}$ along the structure of $T$. In order to do so, we will define paths $\alpha_{l}(\eta)$ for all layers $l\geq 0$ and nodes $\eta\in\mathtt{layer}(i)$ with $0\leq i\leq l$. We will then set $\beta_{l}=\alpha_{l}(\iota)^{N}$ for all $l\geq 0$.

We define the paths $\alpha_{l}(\eta)$ inductively, starting from $i=l$ downto $i=0$. For $\eta\in\mathtt{layer}(l)$ we set $\alpha_{l}(\eta)=C(\eta)$. We consider some $\eta\in\mathtt{layer}(i)$ with $0\leq i<l$. Let $C(\eta)=\pi_{0}\pi_{1}\pi_{2}\cdots\pi_{d}$ be the fixed decomposition and $\eta_{1},\ldots,\eta_{d}$ the corresponding ordering of the children of $\eta$ such that each $\pi_{j}$ has the same start state as $C(\eta_{j})$. We set $\alpha_{l}(\eta)=\pi_{0}\alpha_{l}(\eta_{1})^{N}\pi_{1}\alpha_{l}(\eta_{2})^{N}\pi_{2}\cdots\alpha_{l}(\eta_{d})^{N}\pi_{d}$. We finally set $\beta_{l}=\alpha_{l}(\iota)^{N}$ for all $l\geq 0$.

Lemma 20

The pre-path $\sigma_{l}(\eta)$ can be shuffled with the path $\alpha_{l-1}(\eta)$ to obtain the path $\alpha_{l}(\eta)$ for every $\eta\in\mathtt{layer}(i)$ with $0\leq i<l$. Further, the pre-path $\tau_{l}$ can be shuffled with the path $\beta_{l-1}$ to obtain the path $\beta_{l}$ for every $l\geq 1$.

Proof

For the first claim, we consider some $\eta\in\mathtt{layer}(i)$ with $0\leq i<l$. Let $C(\eta)=\pi_{0}\pi_{1}\pi_{2}\cdots\pi_{d}$ be the fixed decomposition and $\eta_{1},\ldots,\eta_{d}$ the corresponding ordering of the children of $\eta$ such that each $\pi_{j}$ has the same start state as $C(\eta_{j})$. We proceed by induction, starting from $i=l-1$ downto $i=0$.

Assume $i=l-1$: By definition, we have $\sigma_{l}(\eta)=C(\eta_{1})^{N}C(\eta_{2})^{N}\cdots C(\eta_{d})^{N}$, $\alpha_{l-1}(\eta)=C(\eta)=\pi_{0}\pi_{1}\pi_{2}\cdots\pi_{d}$ and $\alpha_{l}(\eta)=\pi_{0}C(\eta_{1})^{N}\pi_{1}C(\eta_{2})^{N}\pi_{2}\cdots C(\eta_{d})^{N}\pi_{d}$. Clearly, we can shuffle $C(\eta_{1})^{N}C(\eta_{2})^{N}\cdots C(\eta_{d})^{N}$ with $\pi_{0}\pi_{1}\pi_{2}\cdots\pi_{d}$ in order to obtain $\pi_{0}C(\eta_{1})^{N}\pi_{1}C(\eta_{2})^{N}\pi_{2}\cdots C(\eta_{d})^{N}\pi_{d}$. Hence, the claim holds.

Assume $i<l-1$: By definition, we have $\sigma_{l}(\eta)=\sigma_{l}(\eta_{1})^{N}\sigma_{l}(\eta_{2})^{N}\cdots\sigma_{l}(\eta_{d})^{N}$, $\alpha_{l-1}(\eta)=\pi_{0}\alpha_{l-1}(\eta_{1})^{N}\pi_{1}\alpha_{l-1}(\eta_{2})^{N}\pi_{2}\cdots\alpha_{l-1}(\eta_{d})^{N}\pi_{d}$ and $\alpha_{l}(\eta)=$

$\pi_{0}\alpha_{l}(\eta_{1})^{N}\pi_{1}\alpha_{l}(\eta_{2})^{N}\pi_{2}\cdots\alpha_{l}(\eta_{d})^{N}\pi_{d}$. By induction assumption, we have that each $\sigma_{l}(\eta_{j})$ can be shuffled with $\alpha_{l-1}(\eta_{j})$ to obtain $\alpha_{l}(\eta_{j})$. Clearly, then also $\sigma_{l}(\eta_{j})^{N}$ can be shuffled with $\alpha_{l-1}(\eta_{j})^{N}$ to obtain $\alpha_{l}(\eta_{j})^{N}$. We then get that $\sigma_{l}(\eta)$ can be shuffled with $\alpha_{l-1}(\eta)$ to obtain the path $\alpha_{l}(\eta)$.

For the second claim we consider some $l\geq 1$. By the above, we have that $\sigma_{l}(\iota)$ can be shuffled with $\alpha_{l-1}(\iota)$ to obtain the path $\alpha_{l}(\iota)$. Clearly, then also $\tau_{l}=\sigma_{l}(\iota)^{N}$ can be shuffled with $\beta_{l-1}(\iota)^{N}$ to obtain $\beta_{l}=\alpha_{l}(\iota)^{N}$. ∎

We now set $\gamma_{l}=\beta_{0}^{k}\beta_{1}^{k}\cdots\beta_{l}^{k}$ for all $l\geq 0$, where $k$ is the constant from Step II. The main property of the paths $\gamma_{l}$ is stated in the next lemma:

Lemma 21

For every $l\geq 0$, $\gamma_{l}$ can be obtained by shuffling the pre-paths $\rho_{0},\rho_{1},\ldots,\rho_{l}$.

Proof

The proof is by induction on $l\geq 0$. We first consider $l=0$. Then, we have $\rho_{0}=\gamma_{0}=C(\eta)^{kN}$ and the claim trivially holds.

We assume $l\geq 1$. By induction assumption we can obtain $\gamma_{l-1}$ by shuffling $\rho_{0},\rho_{1},\ldots,\rho_{l-1}$. We will now argue that we can obtain $\gamma_{l}=\beta_{0}^{k}\beta_{1}^{k}\cdots\beta_{l}^{k}$ by shuffling $\rho_{l}$ with $\gamma_{l-1}=\beta_{0}^{k}\beta_{1}^{k}\cdots\beta_{l-1}^{k}$ By definition we have $\rho_{l}=\tau_{0}^{k}\tau_{1}^{k}\cdots\tau_{l}^{k}$. By Lemma 20, $\tau_{i}$ can be shuffled with $\beta_{i-1}$ to obtain $\beta_{i}$ for every $0<i\leq l$. But then we can also shuffle $\tau_{i}^{k}$ with $\beta_{i-1}^{k}$ to obtain $\beta_{i}^{k}$ for every $0<i\leq l$. Because $\tau_{i}^{k}$ and $\beta_{i-1}^{k}$ appear in the same order in $\tau_{1}^{k}\tau_{2}^{k}\cdots\tau_{l}^{k}$ and $\beta_{0}^{k}\beta_{1}^{k}\cdots\beta_{l-1}^{k}$, we can shuffle these two (pre-)paths and obtain $\beta_{1}^{k}\cdots\beta_{l}^{k}$. The claim then follows because of $\beta_{0}=\tau_{0}=C(\eta)^{N}$. ∎

We finally state the proof of Theorem 6.1:

Proof

Let $l_{\max}$ be the maximal layer of $T$. We will now argue that the path $\gamma_{l_{\max}}$ gives rise to traces with the desired properties. By Lemma 19, each pre-path $\rho_{i}$, for $0\leq i\leq l_{\max}$, can be executed from a valuation $\nu$ with $\left\lVert\nu\right\rVert\in O(N)$, and $\rho_{l_{\max}}$ reaches a valuation $\nu^{\prime}$ with $\nu^{\prime}(x)\geq N^{\mathtt{vExp}(x)}$ for all $x\in\mathit{Var}$. From Proposition 4 we get that the path $\gamma_{l_{\max}}$, which can be obtained by shuffling $\rho_{0},\rho_{1},\ldots,\rho_{l_{\max}}$, can be executed from a valuation $\nu$ with $\left\lVert\nu\right\rVert\in O(N)$ and reaches a valuation $\nu^{\prime}$ with $\nu^{\prime}(x)\geq N^{\mathtt{vExp}(x)}$ for all $x\in\mathit{Var}$. We consider a transition $t$ with $\mathtt{tExp}(t)=i$ for some $1\leq i\leq{l_{\max}}$. There is a node $\eta\in\mathtt{layer}(i-1)$ such that $t\in\mathit{Trns}(\mathtt{VASS}(\eta))$. By Property 1) of Lemma 17 we have that $\tau_{i-1}$ contains at least $N^{i}$ instances of $t$. Hence, $\rho_{i-1}=\tau_{0}^{k}\tau_{1}^{k}\tau_{2}^{k}\cdots\tau_{i-1}^{k}$ also contains at least $N^{i}$ instances of $t$. Thus, $\gamma_{l_{\max}}$, which has been obtained from shuffling $\rho_{0},\rho_{1},\ldots,\rho_{l_{\max}}$, also contains at least $N^{i}$ instances of $t$. ∎

Appendix 0.L Proof of Proposition 3

Proof

Let $L$ be a lower triangular matrix with $\mathtt{pot}(Z)=\sum_{\text{column }r\text{ of }L}\mathtt{pot}(r)$. Because $L$ is a lower triangular matrix, we have that for every variable $x\in\mathit{Var}$ there is at most one column vector $r$ such that $r(x)\neq 0$ and $r(x^{\prime})=0$ for all variables $x^{\prime}$ such the row associated to variable $x^{\prime}$ is above the row associated to variable $x$. Now the claim follows because we have $\mathtt{pot}(r)=\mathtt{vExp}(x)$ for every column vector $r$ of $L$ and every variable $x$ such that $r(x)\neq 0$ and $r(x^{\prime})=0$ for all variables $x^{\prime}$ such the row associated to variable $x^{\prime}$ is above the row associated to variable $x$. ∎

Appendix 0.M Proof of Lemma 9

Proof

The proof proceeds by induction on the layer $l$ of $\eta\in\mathtt{layer}(l)$. Clearly, the claim holds for the root $\iota\in\mathtt{layer}(0)$.

We now assume that the claim holds for $l\geq 0$ and prove the claim for $l+1$. We fix some node $\eta\in\mathtt{layer}(l+1)$. Let $\eta_{p}\in\mathtt{layer}(l)$ be the parent of $\eta$. We will apply the Bound Proof Principle from Section 5 in order to show that every trace $\zeta$ with $\mathtt{init}(\zeta)\leq N$ enters $\mathtt{VASS}(\eta)$ at most $O(N^{\mathtt{pot}(\eta)})$ times.

We first need to prepare for the definition of the witness function. By Property 1) of Proposition 2 we have $r_{\eta_{p}}^{T}d+z_{l}(s_{2})-z_{l}(s_{1})\leq 0$ for all $s_{1}\xrightarrow{d}s_{2}\in\mathit{Trns}(\mathtt{VASS}(\eta_{p}))$ (). Further, by Property 2) of Proposition 2 we have for every strict ancestor $\eta^{\prime}\in\mathtt{layer}(i)$ of $\eta_{p}$ that $r_{\eta^{\prime}}^{T}d+z_{i}(s_{2})-z_{i}(s_{1})=0$ for all $s_{1}\xrightarrow{d}s_{2}\in\mathit{Trns}(\mathtt{VASS}(\eta_{p}))$ (#). Now we can choose coefficients $\lambda_{\eta^{\prime}}\in\mathbb{Z}$, for every strict ancestor $\eta^{\prime}$ of $\eta_{p}$, and a coefficient $\lambda_{\eta_{p}}\in\mathbb{Z}$ with $\lambda_{\eta_{p}}>0$ such that the vector $r^{\circ}=\lambda_{\eta_{p}}r_{\eta_{p}}+\sum_{\text{strict ancestor }\eta^{\prime}\text{ of }\eta_{p}}\lambda_{\eta^{\prime}}r_{\eta^{\prime}}$ satisfies the equation $\mathtt{pot}(r^{\circ})+\mathtt{pot}(\eta_{p})=\mathtt{pot}(\eta)$ (the coefficients $\lambda_{\eta^{\prime}}$ and $\lambda_{\eta_{p}}$ can be chosen according to the elementary column operations in the definition of $\mathtt{pot}(\eta)$). Because of Property 6 of Proposition 2 we can in fact choose the coefficients $\lambda_{\eta^{\prime}}$ such that $r^{\circ}=\lambda_{\eta_{p}}r_{\eta_{p}}+\sum_{\text{strict ancestor }\eta^{\prime}\text{ of }\eta_{p}}\lambda_{\eta^{\prime}}r_{\eta^{\prime}}\geq 0$. We now consider the vector $z^{\circ}=\lambda_{\eta_{p}}z_{\eta_{p}}+\sum_{0\leq i<l}\lambda_{\eta^{\prime}}z_{i}$. By () and (#) we get that ${r^{\circ}}^{T}d+z^{\circ}(s_{2})-z^{\circ}(s_{1})\leq 0$ for all $s_{1}\xrightarrow{d}s_{2}\in\mathit{Trns}(\mathtt{VASS}(\eta_{p}))$ (+); we note that this inequality is strict for all transitions $t$ for which inequality (*) is strict, i.e., for all $t\in\mathit{Trns}(\mathtt{VASS}(\eta_{p}))$ with $\mathtt{tExp}(t)=l+1$. Further, the inequality (+) remains valid, if we add the vector $c\cdot\mathbf{1}$ to $z^{\circ}$ for any $c\in\mathbb{Z}$; hence, we can assume $z^{\circ}\geq 0$.

We now define the witness function $w:\mathit{Cfg}(\mathcal{V})\rightarrow\mathbb{N}$ by setting $w(s,\nu)={r^{\circ}}^{T}\nu+z^{\circ}(s)$, for $s\in\mathit{St}(\mathtt{VASS}(\eta_{p}))$, and $w(s,\nu)=0$, otherwise. We note that $w$ is well-defined, i.e., $w(s,\nu)\geq 0$ for all $(s,\nu)\in\mathit{Cfg}(\mathcal{V})$, because we have shown above that $r^{\circ}\geq 0$ and $z^{\circ}\geq 0$. By (+) we have already established condition 1) of the Bound Proof Principle. It remains to establish condition 2).

We observe that only transitions that enter $\mathtt{VASS}(\eta_{p})$ can increase the value of $w$. Let $t=s_{1}\xrightarrow{d}s_{2}$ be such a transition and let $(s_{1},\nu_{1})\xrightarrow{d}(s_{2},\nu_{2})$ be some step in a trace $\zeta$ of $\mathcal{V}$ with $\mathtt{init}(\zeta)\leq N$. Then, $p(s_{2},\nu_{2})-p(s_{1},\nu_{1})=p(s_{2},\nu_{2})={r^{\circ}}^{T}\nu_{2}+z^{\circ}(s)\in O(N^{\mathtt{pot}(r^{\circ})})$. Hence, there is an increase certificate $\mathtt{inc}_{t}$ with $\mathtt{inc}_{t}(N)\in O(N^{\mathtt{pot}(r^{\circ})})$. We further note that by induction assumption we have that $\zeta$ enters $\mathtt{VASS}(\eta_{p})$ at most $O(N^{\mathtt{pot}(\eta_{p})})$ times. Hence, we have $\mathtt{tbound}_{t}(N)\cdot\mathtt{inc}_{t}(N)=O(N^{\mathtt{pot}(\eta_{p})})\cdot O(N^{\mathtt{pot}(r^{\circ})})=O(N^{\mathtt{pot}(\eta_{p})+\mathtt{pot}(r^{\circ})})=O(N^{\mathtt{pot}(\eta)})$.

We are now ready to apply the Bound Proof Principle from Proposition 1. We observe that $\max_{(s,\nu)\in\mathit{Cfg}(\mathcal{V}),\left\lVert\nu\right\rVert\leq N}w(s,\nu)\in O(N)$ because $w(s,\nu)$ is a linear expression for all $s\in\mathit{St}(\mathcal{V})$, and we consider valuations $\nu$ with $\left\lVert\nu\right\rVert\leq N$. From the Bound Proof Principle we now get that $\mathtt{tbound}_{t}(N)\in O(N^{\mathtt{pot}(\eta)})$ for all transitions $t\in\mathit{Trns}(\mathtt{VASS}(\eta_{p}))$ with $\mathtt{tExp}(t)=l+1$. Finally, we observe that every transition $t$ that enters $\mathtt{VASS}(\eta)$ either also enters $\mathtt{VASS}(\eta_{p})$ or belongs to $\mathtt{VASS}(\eta_{p})$ and we have $\mathtt{tExp}(t)=l+1$. This concludes the proof. ∎

Appendix 0.N Proof of Lemma 10

Proof

We observe that $\mathtt{vExp}(x)=1$ resp. $\mathtt{tExp}(t)=1$ for the bounds discovered in the first iteration and $\mathtt{vExp}(x)>1$ resp. $\mathtt{tExp}(t)>1$ for variable and transition bounds discovered in later iterations of Algorithm 1. We prove the claim by induction on $l$. The claim holds for $l=1$ because we have $\{\mathtt{vExp}(x)\mid x\in\mathit{Var},\mathtt{vExp}(x)<1\}=\emptyset$ and thus $\mathtt{varsum}(1)=1$.

We consider some $l\geq 1$ and prove the claim for $l+1$. We will apply the Bound Proof Principle from Section 5 in order to show that $\mathtt{vExp}(x)=l+1$ resp. $\mathtt{tExp}(t)=l+1$ implies $\mathtt{vExp}(x)\leq\mathtt{varsum}(l+1)$ resp. $\mathtt{tExp}(t)\leq\mathtt{varsum}(l+1)$. Concretely, we will show $\mathtt{vbound}_{x}(N)\in O(N^{\mathtt{varsum}(l+1)})$ resp. $\mathtt{tbound}_{t}(N)\in O(N^{\mathtt{varsum}(l+1)})$ for all variables $x$ with $\mathtt{vExp}(x)=l+1$ and transitions $t$ with $\mathtt{tExp}(t)=l+1$, and then get $\mathtt{vExp}(x)\leq\mathtt{varsum}(l+1)$ and $\mathtt{tExp}(t)\leq\mathtt{varsum}(l+1)$ from $\mathtt{vbound}_{N}(x)\in\Omega(N^{\mathtt{vExp}(x)})$ and $\mathtt{tbound}_{N}(t)\in\Omega(N^{\mathtt{tExp}(t)})$ (Corollary 2) .

We first need to prepare for the definition of the witness function. We define a vector $q\in\mathbb{Z}^{\mathit{Var}}$ by setting $q(x)=0$ for variables $x$ with $\mathtt{vExp}(x)\neq l+1$, and $q(x)=r_{\eta}(x)$ for variables $x$ with $\mathtt{vExp}(x)=l+1$, where $\eta\in\mathtt{layer}(l)$ is arbitrarily chosen. We now argue that for every $\eta\in\mathtt{layer}(l)$ there are vectors $r_{\eta}^{\circ}\in\mathbb{Z}^{\mathit{Var}}$, $z_{\eta}^{\circ}\in\mathbb{Z}^{\mathit{St}(\mathcal{V})}$ and a coefficient $\lambda_{\eta}>0$ such that $\mathtt{pot}(r_{\eta}^{\circ})+\mathtt{pot}(\eta)\leq\mathtt{varsum}(l+1)$, $r_{\eta}^{\circ}\geq 0$, $z_{\eta}^{\circ}\geq 0$, and $(r_{\eta}^{\circ}+\lambda_{\eta}q)^{T}d+z_{\eta}^{\circ}(s_{2})-z_{\eta}^{\circ}(s_{1})\leq 0$ for all $s_{1}\xrightarrow{d}s_{2}\in\mathit{Trns}(\mathtt{VASS}(\eta))$ (+). This is done as follows: We fix some $\eta\in\mathtt{layer}(l)$. By Property 1) of Proposition 2 we have $r_{\eta}^{T}d+z_{l}(s_{2})-z_{l}(s_{1})\leq 0$ for all $s_{1}\xrightarrow{d}s_{2}\in\mathit{Trns}(\mathtt{VASS}(\eta))$ (); we note that this inequality is strict for all transitions $t\in\mathit{Trns}(\mathtt{VASS}(\eta))$ with $\mathtt{tExp}(t)=l+1$. Further, by Property 2) of Proposition 2 we have for every strict ancestor $\eta^{\prime}\in\mathtt{layer}(i)$ of $\eta_{p}$ that $r_{\eta^{\prime}}^{T}d+z_{i}(s_{2})-z_{i}(s_{1})=0$ for all $s_{1}\xrightarrow{d}s_{2}\in\mathit{Trns}(\mathtt{VASS}(\eta))$ (#). Now we can choose coefficients $\lambda_{\eta^{\prime}}\in\mathbb{Z}$, for every strict ancestor $\eta^{\prime}$ of $\eta_{p}$, and a coefficient $\lambda_{\eta}\in\mathbb{Z}$ with $\lambda_{\eta}>0$ such that the vector $r_{\eta}^{\circ}=\lambda_{\eta}(r_{\eta}-q)+\sum_{\text{strict ancestor }\eta^{\prime}\text{ of }\eta_{p}}\lambda_{\eta^{\prime}}r_{\eta^{\prime}}$ satisfies the equation $\mathtt{pot}(r^{\circ})+\mathtt{pot}(\eta)=\mathtt{pot}(\{r_{\eta^{\prime}}\mid\eta^{\prime}\text{ is a strict ancestor }\text{ of }\eta\}\cup\{r_{\eta}-q\})$. By Property 4 of Proposition 2 we have that the vector $r_{\eta}-q$ has non-zero coefficients only for variables $x$ with $\mathtt{vExp}(x)\leq l$. Thus, we obtain $\mathtt{pot}(r^{\circ})+\mathtt{pot}(\eta)=\mathtt{pot}(\{r_{\eta^{\prime}}\mid\eta^{\prime}\text{ is a strict ancestor }\text{ of }\eta\}\cup\{r_{\eta}-q\})\leq\mathtt{varsum}(l+1)$ from Proposition 3. Because of Property 6 of Proposition 2 we can in fact choose the coefficients $\lambda_{\eta^{\prime}}$ such that $r_{\eta}^{\circ}=\lambda_{\eta}(r_{\eta}-q)+\sum_{\text{strict ancestor }\eta^{\prime}\text{ of }\eta_{p}}\lambda_{\eta^{\prime}}r_{\eta^{\prime}}\geq 0$. We now consider the vector $z_{\eta}^{\circ}=\lambda_{\eta}z_{\eta}+\sum_{0\leq i<l}\lambda_{\eta^{\prime}}z_{i}$. By () and (#) we get that $(r_{\eta}^{\circ}+\lambda_{\eta}q)^{T}d+z_{\eta}^{\circ}(s_{2})-z_{\eta}^{\circ}(s_{1})\leq 0$ for all $s_{1}\xrightarrow{d}s_{2}\in\mathit{Trns}(\mathtt{VASS}(\eta))$; we note that this inequality is strict for all transitions $t$ for which inequality (*) is strict, i.e., for all $t\in\mathit{Trns}(\mathtt{VASS}(\eta))$ with $\mathtt{tExp}(t)=l+1$. Further, the inequality remains valid, if we add the vector $c\cdot\mathbf{1}$ to $z_{\eta}^{\circ}$ for any $c\in\mathbb{Z}$; hence, we can assume $z_{\eta}^{\circ}\geq 0$.

We are now ready to define the witness function $w:\mathit{Cfg}(\mathcal{V})\rightarrow\mathbb{N}$. Let $\lambda>0$ be the least common multiple of the coefficients $\lambda_{\eta}$ for $\eta\in\mathtt{layer}(l)$. We define $w$ by setting $w(s,\nu)=(\frac{\lambda}{\lambda_{\eta}}r_{\eta}^{\circ}+\lambda q)^{T}\nu+\frac{\lambda}{\lambda_{\eta}}z_{\eta}^{\circ}(s)$, if there is a node $\eta\in\mathtt{layer}(l)$ with $s\in\mathit{St}(\mathtt{VASS}(\eta))$, and $w(s,\nu)=\lambda q^{T}\nu$, otherwise. We note that $w$ is well-defined, i.e., $w(s,\nu)\geq 0$ for all $(s,\nu)\in\mathit{Cfg}(\mathcal{V})$, because of $\lambda>0$, $q\geq 0$ and because of $r_{\eta}^{\circ}\geq 0$, $z_{\eta}^{\circ}\geq 0$ for all $\eta\in\mathtt{layer}(l)$. Let $U=\bigcup_{\eta\in\mathtt{layer}(l)}\mathit{Trns}(\mathtt{VASS}(\eta))$ be the transitions associated to the nodes in layer $l$ of the tree. By (+) we have already established condition 1) of the Bound Proof Principle for all $t\in U$. It remains to establish condition 2). We will argue that for every $t\in\mathit{Trns}(\mathcal{V})\setminus U$ we can define increase certificates $\mathtt{inc}_{t}(N)$ such that $\mathtt{tbound}_{t}(N)\cdot\mathtt{inc}_{t}(N)\leq O(N^{\mathtt{varsum}(l+1)})$.

Let $s_{1}\xrightarrow{d}s_{2}=t\in\mathit{Trns}(\mathcal{V})\setminus U$ be a transition and let $(s_{1},\nu_{1})\xrightarrow{d}(s_{2},\nu_{2})$ be a step in a trace $\zeta$ of $\mathcal{V}$ with $\mathtt{init}(\zeta)\leq N$. We note that $\nu_{2}=\nu_{1}+d$. We proceed by a case distinction on whether $t$ enters some $\mathtt{VASS}(\eta)$ for $\eta\in\mathtt{layer}(l)$.

In case $t$ does not enter $\mathtt{VASS}(\eta)$ for any $\eta\in\mathtt{layer}(l)$, we have that there is no node $\eta\in\mathtt{layer}(l)$ with $s_{2}\in\mathit{St}(\mathtt{VASS}(\eta))$. Hence, we have $w(s_{2},\nu_{2})=q^{T}\nu_{2}$. We get that $w(s_{2},\nu_{2})-w(s_{1},\nu_{1})\leq\lambda q^{T}\nu_{2}-\lambda q^{T}\nu_{1}=\lambda q^{T}d\in O(1)$ and we can set $\mathtt{inc}_{t}(N)$ to a constant function. Because of $t\in\mathit{Trns}(\mathcal{V})\setminus U$, we have $\mathtt{tExp}(t)=l^{\prime}$ for some layer $l^{\prime}\leq l$. By induction assumption we have $\mathtt{tExp}(t)\leq\mathtt{varsum}(l^{\prime})$. Because $\mathtt{varsum}$ is a monotone function, we have $\mathtt{varsum}(l^{\prime})\leq\mathtt{varsum}(l)\leq\mathtt{varsum}(l+1)$. Hence, we get $\mathtt{tExp}(t)\leq\mathtt{varsum}(l+1)$. With $\mathtt{tbound}_{t}(N)\in O(N^{\mathtt{tExp}(t)})$ (by Theorem 5.1) we now get that $\mathtt{tbound}_{t}(N)\cdot\mathtt{inc}_{t}(N)\leq O(N^{\mathtt{tExp}(t)})\cdot O(1)=O(N^{\mathtt{varsum}(l+1)})$.

In case $t$ does enter some $\mathtt{VASS}(\eta)$ with $\eta\in\mathtt{layer}(l)$, we have $w(s_{2},\nu_{2})-w(s_{1},\nu_{1})\leq(\frac{\lambda}{\lambda_{\eta}}r_{\eta}^{\circ}+\lambda q)^{T}\nu_{2}+\frac{\lambda}{\lambda_{\eta}}z_{\eta}^{\circ}(s_{2})-\lambda q^{T}\nu_{1}=\frac{\lambda}{\lambda_{\eta}}{r_{\eta}^{\circ}}^{T}\nu_{2}+\lambda q^{T}d+\frac{\lambda}{\lambda_{\eta}}z_{\eta}^{\circ}(s_{2})\in O(N^{\mathtt{pot}(r_{\eta}^{\circ})})$. With $\mathtt{tbound}_{t}(N)\leq O(N^{\mathtt{pot}(\eta)})$ (by Lemma 9) we get $\mathtt{tbound}_{t}(N)\cdot\mathtt{inc}_{t}(N)\leq O(N^{\mathtt{pot}(\eta)})\cdot O(N^{\mathtt{pot}(r_{\eta}^{\circ})})=O(N^{\mathtt{pot}(\eta)+\mathtt{pot}(r_{\eta}^{\circ})})\leq O(N^{\mathtt{varsum}(l+1)})$.

We are now ready to apply the Bound Proof Principle from Proposition 1. We observe that $\max_{(s,\nu)\in\mathit{Cfg}(\mathcal{V}),\left\lVert\nu\right\rVert\leq N}w(s,\nu)\in O(N)$ because $w(s,\nu)$ is a linear expression for all $s\in\mathit{St}(\mathcal{V})$, and we consider valuations $\nu$ with $\left\lVert\nu\right\rVert\leq N$. From the Bound Proof Principle we now get that $\mathtt{tbound}_{t}(N)\in O(N^{\mathtt{varsum}(l+1)})$ for all transitions $t\in\mathit{Trns}(\mathtt{VASS}(\eta))$ with $\mathtt{tExp}(t)=l+1$. Next, we argue that we can also deduce the desired variable bounds. We consider a variable $x\in\mathit{Var}$ with $\mathtt{vExp}(x)=l+1$. For all $(s,\nu)\in\mathit{Cfg}(\mathcal{V})$ we have $w(s,\nu)\geq q^{T}\nu\geq q(x)\cdot\nu(x)\geq\nu(x)$ . Hence, we get from the Bound Proof Principle that $\mathtt{vbound}_{N}(x)\in O(N^{\mathtt{varsum}(l+1)})$ for all variables $x$ with $\mathtt{vExp}(x)=l+1$. ∎

Appendix 0.O Proof of Lemma 11

Proof

We prove the claim by induction on $l$.

For $l=0$, we have $\{\mathtt{vExp}(x)\mid x\in\mathit{Var},\mathtt{vExp}(x)<0\}=\emptyset$ and $\mathtt{varsum}(l)=1=2^{0}$. Thus, the claim holds.

We assume the claim holds for some $l\geq 0$ and show the claim for some $l+1$. Let $m$ be the number of variables $x\in\mathit{Var}$ such that $\mathtt{vExp}(x)<l$. By induction assumption we have $\mathtt{varsum}(l)\leq 2^{m}$.

We now consider a variable $x$ with $\mathtt{vExp}(x)=l$. From Lemma 10 we have that $\mathtt{vExp}(x)\leq\mathtt{varsum}(l)\leq 2^{m}$.

There are $(k-m)$ variables $x$ such that $\mathtt{vExp}(x)=l$. Hence, we have

$\mathtt{varsum}(l+1)=\sum_{x\in\mathit{Var},\mathtt{vExp}(x)<l+1}\mathtt{vExp}(x)=$

$\sum_{x\in\mathit{Var},\mathtt{vExp}(x)<l}\mathtt{vExp}(x)+\sum_{x\in\mathit{Var},\mathtt{vExp}(x)=l}\mathtt{vExp}(x)=$

$\mathtt{varsum}(l)+(k-m)\mathtt{vExp}(x)\leq$

$2^{m}+(k-m)2^{m}=(k-m+1)2^{m}\leq 2^{k-m}2^{m}=2^{k}$. ∎

Appendix 0.P Proof of Theorem 4.1

Proof

By assumption there are no $t\in\mathit{Trns}(\mathcal{V})$, $x\in\mathit{Var}$ with $l<\mathtt{tExp}(t)+\mathtt{vExp}(x)<\infty$ (*).

We now will argue that the cycles $C(\eta)$ and sets $U=\{x\in\mathit{Var}\mid\mathtt{vExp}(x)\leq l\}$, $W=\{x\in\mathit{Var}\mid\mathtt{vExp}(x)>l\}$ satisfy the requirements of Lemma 12. The claim then directly follows from the application of Lemma 12.

By Lemma 16 we have $\sum_{\eta\in\mathtt{layer}(l)}\mathit{val}(C(\eta))(x)\geq 1$ for variables $x\in\mathit{Var}$ with $\mathtt{vExp}(x)>l$. It remains to show $\mathit{val}(C(\eta))(x)\geq 0$ for variables $x\in\mathit{Var}$ with $\mathtt{vExp}(x)\leq l$ and nodes $\eta\in\mathtt{layer}(l)$.

Let $\eta\in\mathtt{layer}(l)$ be a node in layer $l$ and let $x\in\mathit{Var}$ be a variable with $\mathtt{vExp}(x)\leq l$. Let $\eta^{\prime}\in\mathtt{layer}(l-\mathtt{vExp}(x))$ be the unique ancestor of $\eta$ in layer $l-\mathtt{vExp}(x)$. We show that $\mathtt{VASS}(\eta)=\mathtt{VASS}(\eta^{\prime})$. Assume otherwise. Then there is a transition $t\in\mathit{Trns}(\mathtt{VASS}(\eta^{\prime}))\setminus\mathit{Trns}(\mathtt{VASS}(\eta))$ with $l-\mathtt{vExp}(x)<\mathtt{tExp}(t)$. However, this contradicts the assumption (*). Hence we get that $\mathtt{VASS}(\eta)=\mathtt{VASS}(\eta^{\prime})$. Thus, $\eta$ is the sole descendant of $\eta^{\prime}$ in layer $l$. We can then deduce $\mathit{val}(C(\eta))(x)\geq 0$ from Lemma 15. ∎