Long-Run Average Behavior of Vector Addition Systems with States

TL;DR

This paper investigates the long-run average behavior of vector addition systems with states (VASS), providing complexity results and decidability for various cases, and establishing a connection to quadratic Diophantine inequalities.

Contribution

It offers the first polynomial-time decidability result for uniform cost functions on integer-valued VASS and explores the complexity of the problem for natural-valued and general cost functions.

Findings

Polynomial-time decidability for uniform cost functions on integer-valued VASS

NP-completeness for general cost functions on integer-valued VASS

Undecidability results for natural-valued VASS with general cost functions

Abstract

A vector addition system with states (VASS) consists of a finite set of states and counters. A configuration is a state and a value for each counter; a transition changes the state and each counter is incremented, decremented, or left unchanged. While qualitative properties such as state and configuration reachability have been studied for VASS, we consider the long-run average cost of infinite computations of VASS. The cost of a configuration is for each state, a linear combination of the counter values. In the special case of uniform cost functions, the linear combination is the same for all states. The (regular) long-run emptiness problem is, given a VASS, a cost function, and a threshold value, if there is a (lasso-shaped) computation such that the long-run average value of the cost function does not exceed the threshold. For uniform cost functions, we show that the regular long-run emptiness problem is (a)~decidable in polynomial time for integer-valued VASS, and (b)~decidable but nonelementarily hard for natural-valued VASS (i.e., nonnegative counters). For general cost functions, we show that the problem is (c)~NP-complete for integer-valued VASS, and (d)~undecidable for natural-valued VASS. Our most interesting result is for (c) integer-valued VASS with general cost functions, where we establish a connection between the regular long-run emptiness problem and quadratic Diophantine inequalities. The general (nonregular) long-run emptiness problem is equally hard as the regular problem in all cases except (c), where it remains open.

Equations

$$\text{textsc}LimAvg(w)=\underset{k\to \infty }{\mathrm{liminf}}\frac{1}{k+1}\sum _{i=0}^{k}w[i].$$

$$\ldots(B,\bigl{(}\begin{smallmatrix}-i\\ 2i\end{smallmatrix}\bigr{)})(A,\bigl{(}\begin{smallmatrix}-i+1\\ 2i\end{smallmatrix}\bigr{)})(B,\bigl{(}\begin{smallmatrix}-i+1\\ 2i-1\end{smallmatrix}\bigr{)})(C,\bigl{(}\begin{smallmatrix}-i+1\\ 2i+2\end{smallmatrix}\bigr{)})\ldots$$

$$\dots i-4i+4i2i+2\dots$$

$$\text{textsc}Gain({\rho }_1{\rho }_2)=\text{textsc}Gain({\rho }_1)+\text{textsc}Gain({\rho }_2).$$

$$\text{textsc}Vals({\rho }_1{\rho }_2)=\text{textsc}Vals({\rho }_1)+\text{textsc}Vals({\rho }_2).$$

$$\frac{1}{n+1}\Big{(}\vec{0}\cdot\textsc{Vals}(\rho_{2})+\textsc{Gain}(\rho_{2})\cdot\textsc{Vals}(\rho_{2})+\ldots+n\textsc{Gain}(\rho_{2})\cdot\textsc{Vals}(\rho_{2})\Big{)}=\frac{n}{2}\textsc{Gain}(\rho_{2})\cdot\textsc{Vals}(\rho_{2}).$$

$$\begin{split}\textsc{Gain}(e_{1}e_{2}e_{3}e_{4})&=\bigl{(}\begin{smallmatrix}1\\ 0\end{smallmatrix}\bigr{)}+\bigl{(}\begin{smallmatrix}0\\ -1\end{smallmatrix}\bigr{)}+\bigl{(}\begin{smallmatrix}0\\ 3\end{smallmatrix}\bigr{)}+\bigl{(}\begin{smallmatrix}-2\\ 0\end{smallmatrix}\bigr{)}=\bigl{(}\begin{smallmatrix}-1\\ 2\end{smallmatrix}\bigr{)}\\ \textsc{Vals}(e_{1}e_{2}e_{3}e_{4})&=\bigl{(}\begin{smallmatrix}1\\ 1\end{smallmatrix}\bigr{)}+\bigl{(}\begin{smallmatrix}4\\ 0\end{smallmatrix}\bigr{)}+\bigl{(}\begin{smallmatrix}1\\ 1\end{smallmatrix}\bigr{)}+\bigl{(}\begin{smallmatrix}0\\ 1\end{smallmatrix}\bigr{)}=\bigl{(}\begin{smallmatrix}6\\ 3\end{smallmatrix}\bigr{)}\end{split}$$

$$\begin{array}{rl}{\vec{x}}^T\mathbf{A}\vec{x}+\vec{a}\vec{x}+d& \le 0\\ \mathbf{B}\vec{x}& \le \vec{c}\end{array}$$

$$\text{textsc}Gain(\rho )\cdot \text{textsc}Vals(\rho )=\sum _{1\le i,j\le m}x[i]x[j]\text{textsc}Gain(e_i)\cdot \text{textsc}Vals(e_j)$$

$$2\cdot \text{textsc}Gain(\rho )\cdot \text{textsc}Vals(\rho )={\vec{x}}^T\mathbf{A}\vec{x}$$

$$\mathbf{A}[i,j]=\text{textsc}Gain(e_i)\cdot \text{textsc}Vals(e_j)+\text{textsc}Gain(e_j)\cdot \text{textsc}Vals(e_i).$$

$$\mathbf{A}=\left[\begin{array}{cccc}[r]2& 3& 4& -2\\ 3& 0& -1& -9\\ 4& -1& 6& 1\\ -2& -9& 1& 0\end{array}\right]$$

$${\mathbf{A}}^{\prime }=\left[\begin{array}{cc}[r]8& -8\\ -8& 8\end{array}\right]$$

$$({\vec{x}}^{\prime }{)}^T{\mathbf{A}}^{\prime }\vec{x}=(x_1-x_3{)}^2$$

$$\mathsf{Sum}_{\vec{g}}(\rho)=\sum_{i=1}^{m}\Big{(}\vec{g}+\sum_{j=1}^{i-1}\vec{y}_{j}\Big{)}\cdot l(q_{i})$$

$${\alpha }_0{\beta }_1^{n[1]}{\alpha }_1{\beta }_2^{n[2]}\dots {\beta }_p^{n[p]}{\alpha }_p,$$

$${\mathsf{Sum}}_{\text{textsc}Gain({\rho }_1)}({\rho }_2)={\vec{n}}^T\mathbf{B}\vec{n}+\vec{c}\cdot \vec{n}+e$$

$${\vec{n}}^T{\mathbf{B}}_{\text{textsc}Tpl}\vec{n}={\vec{d}}_{\text{textsc}Tpl}\cdot \vec{n}+h_{\text{textsc}Tpl}.$$

$$({\vec{c}}_{\text{textsc}Tpl}+{\vec{d}}_{\text{textsc}Tpl})\cdot \vec{n}+(e_{\text{textsc}Tpl}+h_{\text{textsc}Tpl})\le 0.$$

$${\alpha }_0{\beta }_1^{n[1]}{\alpha }_1{\beta }_2^{n[2]}\dots {\beta }_p^{n[p]}{\alpha }_p.$$

$${\mathsf{Sum}}_{\vec{g}}({\alpha }_0{\beta }^2{\alpha }_1{\alpha }_2)\le {\mathsf{Sum}}_{\vec{g}}({\alpha }_0\beta {\alpha }_1\beta {\alpha }_2)$$

$${\mathsf{Sum}}_{\vec{g}}({\alpha }_0{\alpha }_1{\beta }^2{\alpha }_2)\le {\mathsf{Sum}}_{\vec{g}}({\alpha }_0\beta {\alpha }_1\beta {\alpha }_2)$$

$$\begin{split}\mathsf{Sum}_{\vec{g}}(\alpha_{0}\beta\alpha_{1}\beta\alpha_{2})=\frac{1}{2}\big{(}&\mathsf{Sum}_{\vec{g}}(\alpha_{0}\beta^{2}\alpha_{1}\alpha_{2})+\\ &\mathsf{Sum}_{\vec{g}}(\alpha_{0}\alpha_{1}\beta^{2}\alpha_{2})\big{)}\end{split}$$

$${\mathsf{Sum}}_{\vec{g}}(\text{textsc}Tpl(\vec{n}))={\mathsf{Sum}}_{\vec{0}}(\text{textsc}Tpl(\vec{n}))+\vec{g}\cdot \text{textsc}Vals(\text{textsc}Tpl(\vec{n})).$$

$$2\cdot {\mathsf{Sum}}_{\vec{0}}(\text{textsc}Tpl(\vec{n}))={\vec{n}}^T{\mathbf{B}}_{\text{textsc}Tpl}\vec{n}+{\vec{c}}_{\text{textsc}Tpl}\vec{n}+e_{\text{textsc}Tpl}$$

$${\mathbf{B}}_{\text{textsc}Tpl}[i,j]=\text{textsc}Gain({\beta }_{min(i,j)})\cdot \text{textsc}Vals({\beta }_{max(i,j)}).$$

$${\mathsf{Sum}}_{\vec{0}}(\text{textsc}Tpl(\vec{n}))+\vec{g}\cdot \text{textsc}Vals(\text{textsc}Tpl(\vec{n}))\le 0$$

$$\text{textsc}Gain(\text{textsc}Tpl(t{\vec{n}}_1+{\vec{n}}_2))\cdot \text{textsc}Vals(\text{textsc}Tpl(t{\vec{n}}_1+{\vec{n}}_2))=0.$$

$${\mathbf{B}}_{\text{textsc}{Tpl}_1}=\left[\begin{array}{cc}[r]4& -1\\ -1& 4\end{array}\right]{\mathbf{B}}_{\text{textsc}{Tpl}_2}=\left[\begin{array}{cc}[r]4& -7\\ -7& 4\end{array}\right]$$

$$\mathbf{A}[i,j]=\text{textsc}Gain({\beta }_i)\cdot \text{textsc}Vals({\beta }_j)+\text{textsc}Gain({\beta }_j)\cdot \text{textsc}Vals({\beta }_i).$$

$${\mathbf{B}}_{\text{textsc}Tpl}[i,j]=\text{textsc}Gain({\beta }_{min(i,j)})\cdot \text{textsc}Vals({\beta }_{max(i,j)})$$

Full text

1 Introduction

*Vector Addition System with States (VASS). * Vector Addition Systems (VASs) [22] are equivalent to Petri Nets, and they provide a fundamental framework for formal analysis of parallel processes [16]. The extension of VASs with a finite-state transition structure gives Vector Addition Systems with States (VASS). Informally, a VASS consists of a finite set of control states and transitions between them, and a set of $k$ counters, where at every transition between the control states each counter is either incremented, decremented, or remains unchanged. A configuration consists of a control state and a valuation of each counter, and the transitions of the VASS describe the transitions between the configurations. Thus a VASS represents a finite description of an infinite-state transition system between the configurations. If the counters can hold all possible integer values, then we call them integer-valued VASS; and if the counters can hold only non-negative values, then we call them natural-valued VASS.

Modelling power. VASS are a fundamental model for concurrent processes [16], and often used in performance analysis of concurrent processes [14, 18, 20, 21]. Moreover, VASS have been used (a) in analysis of parametrized systems [2], (b) as abstract models for programs for bounds and amortized analysis [31], (c) in interactions between components of an API in component-based synthesis [17]. Thus they provide a rich framework for a variety of problems in verification as well as program analysis.

Previous results for VASS. A computation (or a run) in a VASS is a sequence of configurations. The well-studied problems for VASS are as follows: (a) control-state reachability where given a set of target control states a computation is successful if one of the target states is reached; (b) configuration reachability where given a set of target configurations a computation is successful if one of the target configurations is reached. For natural-valued VASS, (a) the control-state reachability problem is ExpSpace-complete: the ExpSpace-hardness is shown in [27, 15] and the upper bound follows from [30]; and (b) the configuration reachability problem is decidable [28, 23, 24, 25], and a recent breakthrough result shows that the problem is non-elementary hard [12]. For integer-valued VASS, (a) the control-state reachability problem is NLogSpace-complete: the counters can be abstracted away and we have to solve the reachability problem for graphs; and (b) the configuration reachability problem is NP-complete: this is a folklore result obtained via reduction to linear Diophantine inequalities.

Long-run average property. The classical problems for VASS are qualitative (or Boolean) properties where each computation is either successful or not. In this work we consider long-run average property that assigns a real value to each computation. A cost is associated to each configuration and the value of a computation is the long-run average of the costs of the configurations of the computation. For cost assignment to configuration we consider linear combination with natural coefficients of the values of the counters. In general the linear combination for the cost depends on the control state of the configuration, and in the special case of uniform cost functions the linear combination is the same across all states.

Motivating examples. We present some motivating examples for the problems we consider. First, consider a VASS where the counters represent different queue lengths, and each queue consumes resource (e.g., energy) proportional to its length, however, for different queues the constant of the proportionality might differ. The computation of the long-run average resource consumption is modeled as a uniform cost function, where the linear combination for the cost function is obtained from the constants of proportionality. Second, consider a system that uses two different batteries, and the counters represent the charge levels. At different states, different batteries are used, and we are interested in the long-run average charge of the used battery. This is modeled as a general cost function, where depending on the control state the cost function is the value of the counter representing the battery used in the state.

Our contributions. We consider the following decision problem: given a VASS and a cost function decide whether there is a regular (or periodic) computation such that the long-run average value is at most a given threshold. Our main contributions are as follows:

For uniform cost functions, we show that the problem is (a) decidable in polynomial time for integer-valued VASS, and (b) decidable but non-elementary hard for natural-valued VASS. In (b) we assume that the cost function depends on all counters. 2. 2.

For general cost functions, we show that the problem is (a) NP-complete for integer-valued VASS, and (b) undecidable for natural-valued VASS.

Our most interesting result is for general cost functions and integer-valued VASS, where we establish an interesting connection between the problem we consider and quadratic Diophantine inequalities. Finally, instead of regular computations, if we consider existence of an arbitrary computation, then all the above results hold, other than the NP-completeness result for general cost functions and integer-valued VASS (which remains open).

Related works. Long-run average behavior have been considered for probabilistic VASS [6], and other infinite-state models such as pushdown automata and games [10, 11, 1]. In these works the costs are associated with transitions of the underlying finite-state representation. In contrast, in our work the costs depend on the counter values and thus on the configurations. Costs based on configurations, specifically the content of the stack in pushdown automata, have been considered in [29]. Quantitative asymptotic bounds for polynomial-time termination in VASS have also been studied [4, 26], however, these works do not consider long-run average property. Finally, a related model of automata with monitor counters with long-run average property have been considered in [9, 8]. However, there are some crucial differences: in automata with monitor counters, the cost always depends on one counter, and counters are reset once the value is used. Moreover, the complexity results for automata with monitor counters are quite different from the results we establish.

The full proofs of presented theorems and lemmas have been relegated to the appendix.

2 Preliminaries

For a sequence $w$, we define $w[i]$ as the $(i+1)$-th element of $w$ (we start with [math]) and $w[i,j]$ as the subsequence $w[i]w[i+1]\ldots w[j]$. We allow $j$ to be $\infty$ for infinite sequences. For a finite sequence $w$, we denote by $|w|$ its length; and for an infinite sequence the length is $\infty$.

We use the same notation for vectors. For a vector $\vec{x}\in\mathbb{R}^{k}$ (resp., $\mathbb{Q}^{k}$, $\mathbb{Z}^{k}$ or $\mathbb{N}^{k}$), we define $x[i]$ as the $i$-th component of $\vec{x}$. We define the support of $\vec{x}$, denoted by $supp(\vec{x})$ as the set of components of $\vec{x}$ with non-zero values. For vectors $\vec{x},\vec{y}$ of equal dimension, we denote by $\vec{x}\cdot\vec{y}$, the dot-product of $\vec{x}$ and $\vec{y}$.

2.1 Vector addition systems with states (VASS)

A $k$-dimensional vector addition system with states (VASS) over $\mathbb{Z}$ (resp., over $\mathbb{N}$), referred to as $\textsc{VASS}(\mathbb{Z},k)$ (resp., $\textsc{VASS}(\mathbb{N},k)$), is a tuple $\mathcal{A}=\langle Q,Q_{0},\delta\rangle$, where (1) $Q$ is a finite set of states, (2) $Q_{0}\subseteq Q$ is a set of initial states, and (3) $\delta\subseteq Q\times Q\times\mathbb{Z}^{k}$. We denote by $\textbf{VASS}(\mathbb{Z},k)$ (resp., $\textbf{VASS}(\mathbb{N},k)$) the class of $k$-dimensional VASS over $\mathbb{Z}$ (resp., $\mathbb{N}$). We often omit the dimension in VASS and write $\textsc{VASS}(\mathbb{Z}),\textsc{VASS}(\mathbb{N}),\textbf{VASS}(\mathbb{N}),\textbf{VASS}(\mathbb{Z})$ if a definition or an argument is uniform w.r.t. the dimension.

Configurations and computations. A configuration of a $\textsc{VASS}(\mathbb{Z},k)$ $\mathcal{A}$ is a pair from $Q\times\mathbb{Z}^{k}$, which consists of a state and a valuation of the counters. A computation of $\mathcal{A}$ is an infinite sequence $\pi$ of configurations such that (a) $\pi[0]\in Q_{0}\times\{\vec{0}\}$111Without loss of generality, we assume that the initial counter valuation is $\vec{0}$. We can encode any initial configuration in the VASS itself., and (b) for every $i\geq 0$, there exists $(q,q^{\prime},\vec{y})\in\delta$ such that $\pi[i]=(q,\vec{x})$ and $\pi[i+1]=(q^{\prime},\vec{x}+\vec{y})$. A computation of a $\textsc{VASS}(\mathbb{N},k)$ $\mathcal{A}$ is a computation $\pi$ of $\mathcal{A}$ considered as a $\textsc{VASS}(\mathbb{Z},k)$ such that the values of all counters are natural, i.e., for all $i>0$ we have $\pi[i]\in Q\times\mathbb{N}^{k}$.

Paths and cycles. A path $\rho=(q_{0},q^{\prime}_{0},\vec{y}_{0}),(q_{1},q_{1}^{\prime},\vec{y}_{1}),\ldots$ in a $\textsc{VASS}(\mathbb{Z})$ (resp., $\textsc{VASS}(\mathbb{N})$) $\mathcal{A}$ is a (finite or infinite) sequence of transitions (from $\delta$) such that for all $0\leq i\leq|\rho|$ we have $q^{\prime}_{i}=q_{i+1}$. A finite path $\rho$ is a cycle if $\rho=(q_{0},q^{\prime}_{0},\vec{y}_{0}),\ldots,(q_{m},q^{\prime}_{m},\vec{y}_{m})$ and $q_{0}=q^{\prime}_{m}$. Every computation in a $\textsc{VASS}(\mathbb{Z})$ (resp., $\textsc{VASS}(\mathbb{N})$) defines a unique infinite path. Conversely, every infinite path in a $\textsc{VASS}(\mathbb{Z})$ $\mathcal{A}$ starting with $q_{0}\in Q_{0}$ defines a computation in $\mathcal{A}$. However, if $\mathcal{A}$ is a $\textsc{VASS}(\mathbb{N},k)$, some paths do not have corresponding computations due to non-negativity restriction posed on the counters.

Regular computations. We say that a computation $\pi$ of a $\textsc{VASS}(\mathbb{Z})$ (resp., $\textsc{VASS}(\mathbb{N})$) is regular if it corresponds to a path which is ultimately periodic, i.e., it is of the form $\alpha\beta^{\omega}$ where $\alpha,\beta$ are finite paths.

2.2 Decision problems

We present the decision problems that we study in the paper.

Cost functions. Consider a $\textsc{VASS}(\mathbb{Z},k)$ (resp., $\textsc{VASS}(\mathbb{N},k)$) $\mathcal{A}=(Q,Q_{0},\delta)$. A cost function $f$ for $\mathcal{A}$ is a function $f\colon Q\times\mathbb{Z}^{k}\to\mathbb{Z}$, which is linear with natural coefficients, i.e., for every $q$ there exists $\vec{a}\in\mathbb{N}^{k}$ such that $f(q,\vec{z})=\vec{a}\cdot\vec{z}$ for all $\vec{z}\in\mathbb{Z}^{k}$. We extend cost functions to computations as follows. For a computation $\pi$ of $\mathcal{A}$, we define $f(\pi)$ as the sequence $f(\pi[0]),f(\pi[1]),\ldots$. Every cost function $f$ is given by a labeling $l\colon Q\to\mathbb{N}^{k}$ by $f(q,\vec{z})=l(q)\cdot\vec{z}$. We define the size of $f$, denoted by $|f|$, as the size of binary representation of $l$ considered as a sequence of natural numbers of the length $|Q|\cdot k$.

Uniform cost functions. We say that a cost function $f$ is uniform, if it is given by a constant function $l$, i.e., for all states $q,q^{\prime}$ and $\vec{z}\in\mathbb{Z}^{k}$ we have $f(q,\vec{z})=f(q^{\prime},\vec{z})$. Uniform cost functions are given by a single vector $\vec{a}\in\mathbb{N}^{k}$.

The long-run average. We are interested in the long-run average of the values returned by the cost function, which is formalized as follows. Consider an infinite sequence of real numbers $w$. We define

[TABLE]

Definition 1** (The average-value problems).**

Given a $\textsc{VASS}(\mathbb{Z},k)$ (resp., $\textsc{VASS}(\mathbb{N},k)$) $\mathcal{A}$, a cost function $f$ for $\mathcal{A}$, and a threshold $\lambda\in\mathbb{Q}$,

• •

the average-value problem (resp., the regular average-value problem) asks whether $\mathcal{A}$ has a computation (resp., a regular computation) $\pi$ such that $\textsc{LimAvg}(f(\pi))\leq\lambda$, and

• •

the finite-value problem (resp., the regular finite-value problem) asks whether $\mathcal{A}$ has a computation (resp., a regular computation) $\pi$ such that $\textsc{LimAvg}(f(\pi))<\infty$.

The following example illustrates the regular average-value problem for $\textbf{VASS}(\mathbb{Z})$.

Example 2**.**

Consider the $\textsc{VASS}(\mathbb{Z},2)$ $\mathcal{A}_{e}=\langle\{A,B,C\},\{B\},\{e_{1},e_{2},e_{3},e_{4}\}\rangle$ depicted in Figure 1 and a (non-uniform) cost function $f$ is given by the labeling from Figure 1. A\mapsto\bigl{(}\begin{smallmatrix}4\\ 0\end{smallmatrix}\bigr{)},

Consider an infinite path $(e_{1}e_{2}e_{3}e_{4})^{\omega}$ that defines the regular computation $\pi_{0}$. This computation can be divided into blocks of 4 consecutive configurations. The $(i+1)$-th block has the following form

[TABLE]

and the corresponding values of $f(\pi)$ are:

[TABLE]

Therefore, the sum of values over each block is $6$ and hence $\textsc{LimAvg}(f(\pi_{0}))=\frac{3}{2}$.

The answer to the (regular) average-value problem with any threshold is YES. Consider $j\in\mathbb{N}$ and a path $(e_{1}e_{2})^{j}(e_{1}e_{2}e_{3}e_{4})^{\omega}$. Observe that it defines a regular computation $\pi_{j}$, which after the block $(e_{1}e_{2})^{j}$ coincides with $\pi_{0}$ with all counter values shifted by \bigl{(}\begin{smallmatrix}-2j\\ 3j\end{smallmatrix}\bigr{)}. Note that in each block $e_{1}e_{2}e_{3}e_{4}$, the value $f$ on the vector \bigl{(}\begin{smallmatrix}-2j\\ 3j\end{smallmatrix}\bigr{)} are $j,-8j,j,3j$. Therefore, $\textsc{LimAvg}(f(\pi_{j}))=\textsc{LimAvg}(f(\pi_{0}))+\frac{-3j}{4}=\frac{-3j-6}{4}$. It follows that for every threshold $\lambda\in\mathbb{Q}$, there exists a regular computation $\pi_{j}$ with $\textsc{LimAvg}(f(\pi_{j}))\leq\lambda$.

Organization. In this paper, we study the (regular) average-value problem for $\textbf{VASS}(\mathbb{Z},k)$ and $\textbf{VASS}(\mathbb{N},k)$. First, we study the average-value problem for uniform cost functions (Section 3). Next, we consider the non-uniform case, where we focus on $\textbf{VASS}(\mathbb{Z})$ (Section 4). We start with solving the (regular) finite-value problem, and then we move to the regular average-value problem. We show that both problems are NP-complete. Next, we discuss the non-uniform case for $\textbf{VASS}(\mathbb{N})$ and we show that the regular finite-value problem is decidable (and non-elementary), while the (regular) average-value problem is undecidable.

3 Uniform cost functions

In this section we study the average-value problem for $\textbf{VASS}(\mathbb{Z})$ and $\textbf{VASS}(\mathbb{N})$ for the uniform cost functions.

3.1 Integer-valued VASS: $\textbf{VASS}(\mathbb{Z})$

Consider a $\textsc{VASS}(\mathbb{Z},k)$ $\mathcal{A}$ and a uniform cost function $f$ for $\mathcal{A}$. This function is defined by a single vector of coefficients $\vec{a}\in\mathbb{N}^{k}$. First, observe that we can reduce the number of the counters to one, which tracks the current cost. This counter $c$ stores the value of $f(\pi[i])=\vec{a}\cdot\vec{z}$, where $\vec{z}$ are the values of counters. Initially, the counter $c$ is $0=\vec{a}\cdot\vec{0}$. Next, in each step $i>0$, counters $\vec{z}$ are updated with some values $\vec{y}$ and we update $c$ with $\vec{a}\cdot\vec{y}$. Note that the value of $f(\pi[i+1])=\vec{a}\cdot(\vec{z}+\vec{y})$ equals $f(\pi[i])+\vec{a}\cdot\vec{y}$.

Second, observe that the average-value problem for $\textbf{VASS}(\mathbb{Z},1)$ and uniform cost functions is equivalent to single-player average energy games (with no bounds on energy levels), which are solvable in polynomial time [3]. Moreover, average-energy games (with no bounds on energy levels) admit memoryless winning strategies and hence the average-value and the regular average-value problems coincide. In consequence we have:

Theorem 3**.**

The average-value and the regular average-value problems for $\textbf{VASS}(\mathbb{Z})$ and uniform cost functions are decidable in polynomial time.

3.2 Natural-valued VASS: $\textbf{VASS}(\mathbb{N})$

For natural-valued VASS, we cannot reduce the number of counters to one; we need to track all counters to make sure that all of them have non-negative values. Moreover, we show that the average-value problem for (single counter) $\textbf{VASS}(\mathbb{N},1)$ is in PSpace while the average-value problem for $\textbf{VASS}(\mathbb{N})$ is nonelementary.

First, the average-value problem for (single counter) $\textbf{VASS}(\mathbb{N},1)$ in the uniform case is equivalent to single-player average energy games with non-negativity constraint on the energy values. The latter problem is in PSpace and it is NP-hard [3].

In the multi-counter case, we show that the average-value problem is mutually reducible to the configuration reachability problem for VASS, which has recently been shown nonelementary hard [12]. We additionally assume that the cost function depends on all its arguments, i.e., all coefficients are non-negative. This assumption allows us show that if there is a computation of the average value below some $\lambda$, then there is one, which is lasso-shaped and the cycle in the lasso has exponential size in the size of the VASS and $\lambda$. Therefore, we can non-deterministically pick such a cycle and check whether it is reachable from the initial configuration.

Theorem 4**.**

The average-value and the regular average-value problems for $\textbf{VASS}(\mathbb{N})$ and uniform cost functions with non-zero coefficients are decidable and mutually reducible to the configuration reachability problem for $\textbf{VASS}(\mathbb{N})$.

Proof.

We present both directions of the reduction.

Hardness. Consider a $\mathcal{A}_{0}\in\textbf{VASS}(\mathbb{N},k)$ and two configurations $(q,\vec{v}),(q^{\prime},\vec{v}^{\prime})$. Without loss of generality, we assume that $\vec{v}=\vec{v}^{\prime}=\vec{0}$. We construct a $\textsc{VASS}(\mathbb{N},k+1)$ $\mathcal{A}_{1}$ build as an extension of $\mathcal{A}_{0}$ with two additional states $q_{S},q_{F}$ and an additional counter $c_{k+1}$. The state $q_{S}$ is the only initial state with a single outgoing transition, which goes to $q$, where only the counter $c_{k+1}$ is incremented, and other counters are unchanged. Then, the counter $c_{k+1}$ is not changed except for the state $q_{F}$. The state $q_{F}$ is a sink with an incoming transition $(q^{\prime},q_{F},\vec{0})$ and two loops over $q_{F}$. One loop does not change the counters and the other that decrements $c_{k+1}$ (and does not change the other counters). The cost function returns the sum of counters. Observe that every computation of the average-value [math] has to reach $q_{F}$ with first $k$ counters being [math]. Such a computation exists if and only if $(q^{\prime},\vec{0})$ is reachable in $\mathcal{A}_{0}$ from $(q,\vec{0})$.

Decidability. We can solve the average-value problem for $\textbf{VASS}(\mathbb{N})$ and uniform cost functions with non-zero coefficients in non-deterministic exponential time with a single query to the VASS-reachability oracle.

Consider a $\textsc{VASS}(\mathbb{N},k)$ $\mathcal{A}$ and assume it has a computation $\pi$ of the average-value not exceeding $\lambda$. Then, for every $\epsilon>0$, the computation $\pi$ contains a cyclic computation (a cycle w.r.t. the state and the valuation of counters) of the average value $M=\lambda+\epsilon$. Let $\pi^{C}$ be a cyclic computation of the minimal length among computations of the average value $M$. Consider three sets of positions in $\pi^{C}$:

1. (a)

$N_{0}$, where the value of $f$ is less than $M$, 2. (b)

$N_{1}$, where the value of $f$ belongs to $[M,2M]$, and 3. (c)

$N_{2}$, where the value of $f$ exceeds $2M$.

Note that $|N_{2}|\leq|N_{0}|$, as otherwise the average value exceeds $M$. Since $\pi^{C}$ has the minimal-length, it does not contain a subcycle computation. A subcycle computation has either the average less-or-equal $M$, and hence it is shorter than $\pi^{C}$, or it has the average greater than $M$, and hence it can be removed. Therefore, all positions in $\pi^{C}$ are distinct. Finally, since all coefficients are non-zero, the value of each counter is bounded by $M$, and hence $|N_{0}|,|N_{1}|\leq|Q|\cdot(2M)^{k}$. In consequence, the length of $\pi^{C}$ is bounded by $3|Q|\cdot(2M)^{k}$.

This has two consequences. First, there are finitely many such cyclic computations and hence there exists a cyclic computation of the value at most $\lambda$ and length $3|Q|\cdot(2\lambda)^{k}$. Second, to decide the average-value problem for an $\textsc{VASS}(\mathbb{N},k)$, we can non-deterministically generate a cyclic computation of length bounded by $3|Q|\cdot(2\lambda)^{k}$, verify that (a) its average does not exceed $\lambda$, and (b) it is reachable from some initial configuration.

Observe that the above procedure implies that the average-value and the regular average-value problems coincide for $\textbf{VASS}(\mathbb{N})$ under uniform cost functions with non-zero coefficients. ∎

We have used in the proof the fact that $f$ depends on all counters. We conjecture that this assumption can be lifted:

Open question 5**.**

Is the average-value problem for $\textbf{VASS}(\mathbb{N})$ and uniform cost functions decidable?

4 General cost functions and $\textbf{VASS}(\mathbb{Z})$

First, we consider (an extension of) the regular finite-value problem for $\textbf{VASS}(\mathbb{Z})$ (Section 4.1). We show that one can decide in non-deterministic polynomial time whether a given VASS has a regular computation (a) of the value $-\infty$, or (b) of some finite value. To achieve this, we introduce path summarizations, which allow us to state conditions that entail (a) and respectively (b). We show that these conditions can be checked in NP.

We apply the results from Section 4.1 to solve the regular average-value problem (Section 4.2). We consider only VASS that have some computation of a finite value, and no computation of the value $-\infty$, i.e., the answer to (a) is NO and the answer to (b) is YES. In other cases we can easily answer to the regular average-value problem. If the answer to (a) is YES, then for any threshold we answer YES. If the answers to (a) and (b) are NO, then for any threshold we answer NO. Finally, we show NP-hardness of the regular finite-value and the regular average-value problems (Section 4.3).

The main result of this section is the following theorem:

Theorem 6**.**

The regular finite-value and the regular average-value problems for $\textbf{VASS}(\mathbb{Z})$ with (general) cost functions are NP-complete.

We fix a $\textsc{VASS}(\mathbb{Z},k)$ $\mathcal{A}=\langle Q,Q_{0},\delta\rangle$, with the set of states $Q$ and the set of transitions $\delta$, and a cost function $f$, which we refer to throughout this section. We exclude the complexity statements, where the asymptotic behavior applies to all $\mathcal{A}$ and $f$.

4.1 The finite-value problem

For a path $\rho$, we define characteristics $\textsc{Gain}(\rho),\textsc{Vals}(\rho)$, which summarize the impact of $\rho$ on the values of counters (Gain) and the value of the (partial) average of costs (Vals).

Let $\rho$ be of the form $(q_{1},q_{2},\vec{y}_{1})\ldots(q_{m},q_{m+1},\vec{y}_{m})$. We define $\textsc{Gain}(\rho)$ as the sum of updates along $\rho$, i.e., $\textsc{Gain}(\rho)=\sum_{i=1}^{m}\vec{y}_{i}$. The vector $\textsc{Gain}(\rho)$ is the update of counters upon the whole path $\rho$. Observe that

[TABLE]

Let $l\colon Q\to\mathbb{N}^{k}$ be the function representing $f$, i.e., for every $\vec{z}\in\mathbb{Z}^{k}$ we have $f(q,\vec{z})=l(q)\cdot\vec{z}$. We define $\textsc{Vals}(\rho)$ as the sum of vectors $l(q_{i})$ along $\rho$, i.e., $\textsc{Vals}(\rho)=\sum_{i=1}^{m}l(q_{i})$. Note that we exclude the last state $q_{m+1}$, and hence we have

[TABLE]

The vector $\textsc{Vals}(\rho)$ describes the coefficients with which each counter contributes to the average along the path $\rho$.

Consider a regular computation $\pi$ and a path $\rho_{1}(\rho_{2})^{\omega}$ that corresponds to it. Let $\pi^{\prime}$ be the (regular) computation obtained from $\pi$ by contracting $|\rho_{2}|$ to a single transition $(q_{f},q_{f},\textsc{Gain}(\rho_{2}))$, which is a loop over a fresh state $q_{f}$. The counters over this transition are updated by $\textsc{Gain}(\rho_{2})$ and the cost function in $q_{f}$ is defined as $f(q_{f},\vec{z})=\frac{1}{|\rho_{2}|}\textsc{Vals}(\rho_{2})\cdot\vec{z}$.

The values of $\pi$ and $\pi^{\prime}$ may be different, but they differ only by some finite value. Indeed, the difference over a single iteration of $\rho_{2}$ updates and computation of the partial averages are interleaved along $\rho_{2}$, while in $(q_{f},q_{f},\textsc{Gain}(\rho_{2}))$ we first compute the partial average and then update the counters. Therefore, that difference is a finite value $N$ that does not depend on the initial values of counters. It follows that the difference between the average values of (the computations corresponding to) $\rho_{2}$ and $(q_{f},q_{f},\textsc{Gain}(\rho_{2}))$ is bounded by $N$.

Finally, observe that the value of $\pi^{\prime}$ can be easily estimated. Observe that the partial average of the first $n+1$ values of $f$ in $\pi^{\prime}$ equals

[TABLE]

In consequence, we have the following:

Lemma 7**.**

Let $\pi$ be a regular computation corresponding to a path $\rho_{1}(\rho_{2})^{\omega}$. Then, one of the following holds:

$\textsc{Gain}(\rho_{2})\cdot\textsc{Vals}(\rho_{2})<0$* and $\textsc{LimAvg}(f(\pi))=-\infty$, or* 2. 2.

$\textsc{Gain}(\rho_{2})\cdot\textsc{Vals}(\rho_{2})=0$* and $\textsc{LimAvg}(f(\pi))$ is finite, or* 3. 3.

$\textsc{Gain}(\rho_{2})\cdot\textsc{Vals}(\rho_{2})>0$* and $\textsc{LimAvg}(f(\pi))=\infty$.*

Example 8**.**

Consider the VASS $\mathcal{A}_{e}$ and the cost function $f$ from Example 2. We have shown that the computation defined by the path $(e_{1}e_{2}e_{3}e_{4})^{\omega}$ has finite average value. This can be algorithmically computed using Lemma 7. We compute

[TABLE]

Therefore, $\textsc{Gain}(e_{1}e_{2}e_{3}e_{4})\cdot\textsc{Vals}(e_{1}e_{2}e_{3}e_{4})=0$.

Reduction to integer quadratic programming. Lemma 7 reduces the regular finite-value problem to finding a cycle with $\textsc{Gain}(\rho)\cdot\textsc{Vals}(\rho)<0$ (resp., $\textsc{Gain}(\rho)\cdot\textsc{Vals}(\rho)=0$). We show that existence of such a cycle can be stated as a polynomial-size instance of integer quadratic programming, which can be decided in NP [13]. An instance of integer quadratic programming consists of a symmetric matrix $\mathbf{A}\in\mathbb{Q}^{n\times n},\vec{a}\in\mathbb{Q}^{n},d\in\mathbb{Q},\mathbf{B}\in\mathbb{Q}^{n\times m},\vec{c}\in\mathbb{Q}^{m}$ and it asks whether there exists a vector $\vec{x}\in\mathbb{Z}^{n}$ satisfying the following system:

[TABLE]

Let $\rho$ be a cycle. Observe that both $\textsc{Gain}(\rho),\textsc{Vals}(\rho)$ depend only on the multiplicity of transitions occurring in $\rho$; the order of transitions is irrelevant. Consider a vector $\vec{x}=(x[1],\ldots,x[m])$ of multiplicities of transitions $e_{1},\ldots,e_{m}$ in $\rho$. Then,

[TABLE]

Therefore, we have

[TABLE]

for a symmetric matrix $\mathbf{A}\in\mathbb{Z}^{m\times m}$ defined for all $i,j$ as

[TABLE]

The left hand side of (1) is multiplied by $2$ to avoid division by $2$. It follows that if $\textsc{Gain}(\rho)\cdot\textsc{Vals}(\rho)<0$ (resp., $\textsc{Gain}(\rho)\cdot\textsc{Vals}(\rho)=0$), then the inequality $\vec{x}^{T}\mathbf{A}\vec{x}-1\leq 0$ (resp., $\vec{x}^{T}\mathbf{A}\vec{x}\leq 0$) has a solution.

Note that the above inequality can have a solution, which does not correspond to a cycle. We can encode with a system of linear inequalities that $\vec{x}$ corresponds to a cycle. Consider $S\subseteq Q$, which corresponds to all states visited by $\rho$. It suffices to ensure that (a) for all $s\in S$, the number of incoming transitions to $s$, which is the sum of multiplicities of transitions leading to $s$, equals the number of transitions outgoing from $s$, (b) for every $s\in S$, the number of outgoing transitions is greater or equal to $1$, and (c) for $s\in Q\setminus S$, the number of incoming and outgoing transitions is [math]. Finally, we state that all multiplicities are non-negative. We can encode such equations and inequalities as $\mathbf{B}_{S}\vec{x}\leq\vec{c}_{S}$. Observe that every vector of multiplicities $\vec{x}\in\mathbb{Z}$ satisfies $\vec{x}^{T}\mathbf{A}\vec{x}-1\leq 0$ (resp., $\vec{x}^{T}\mathbf{A}\vec{x}\leq 0$) and $\mathbf{B}_{S}\vec{x}\leq\vec{c}_{S}$ defines a cycle $\rho$ with $\textsc{Gain}(\rho),\textsc{Vals}(\rho)<0$ (resp., $\textsc{Gain}(\rho),\textsc{Vals}(\rho)=0$). The matrices $\mathbf{A},\mathbf{B}_{S}$ and the vector $\vec{c}_{S}$ are polynomial in $|\mathcal{A}|$. The set $S$ can be picked non-deterministically. In consequence, we have the following:

Lemma 9**.**

The problem: given a $\textsc{VASS}(\mathbb{Z},k)$ $\mathcal{A}$ and a cost function $f$, decide whether $\mathcal{A}$ has a regular computation of the value $-\infty$ (resp., less than $+\infty$) is in NP.

Example 10**.**

Consider the VASS $\mathcal{A}_{e}$ and the cost function $f$ from Example 2. We consider some cycle $\rho$ starting in $B$ over all states of $\mathcal{A}_{e}$. Let $\vec{x}\in\mathbb{N}^{4}$ be the multiplicities of transitions $e_{1},e_{2},e_{3},e_{4}$ respectively in $\rho$ Then, we have

[TABLE]

Since $\rho$ is a cycle starting from $B$, we have $x_{1}=x_{2}$ and $x_{3}=x_{4}$. Therefore, we can eliminate $x_{2},x_{4}$ and the matrix $\mathbf{A}$ can be simplified to $\mathbf{A}^{\prime}\in\mathbb{Z}^{2\times 2}$ defined as

[TABLE]

where $x_{1}$ (resp., $x_{3}$) is the multiplicity of the cycle $e_{1}e_{2}$ (resp., $e_{3}e_{4}$). Let $\vec{x}^{\prime}=(x_{1},x_{3})$. Note that

[TABLE]

It follows that a cycle $\rho$ defines the computation of some finite value if and only if it contains the multiplicities of transitions $e_{1},e_{2},e_{3},e_{4}$ are equal.

4.2 The regular average-value problem

In this section, we study the regular average-value problem for $\textbf{VASS}(\mathbb{Z})$. We assume that $\mathcal{A}$ has a regular computation of finite value and does not have a regular computation of the value $-\infty$. Finally, we consider the case of the threshold $\lambda=0$. The case of an arbitrary threshold $\lambda\in\mathbb{Q}$ can be easily reduced to the case $\lambda=0$ (see [9, 8] for intuitions and techniques in mean-payoff games a.k.a. limit-average games).

Consider a regular computation $\pi$ and let $\rho_{1}(\rho_{2})^{\omega}$ be a path corresponding to $\pi$. We derive the necessary and sufficient conditions on $\rho_{1},\rho_{2}$ to have $\textsc{LimAvg}(f(\pi))\leq 0$.

Assume that $\textsc{LimAvg}(f(\pi))\leq 0$. Due to Lemma 7, we have $\textsc{Gain}(\rho_{2})\cdot\textsc{Vals}(\rho_{2})=0$, which implies that every iteration of $\rho_{2}$ has the same average. Therefore, $\textsc{LimAvg}(f(\pi))$ is the average value of $\rho_{2}$ (starting with counter values defined by $\rho_{1}$). The latter value is at most [math] if and only if the sum of values along $\rho_{2}$ is at most [math]. We define this sum below.

The sum of values $\mathsf{Sum}_{\vec{g}}(\rho)$. Let $l$ be the labeling defining the cost function $f$. Consider a path $\rho$ of length $m$ such that $\rho=(q_{1},q_{2},\vec{y}_{1})\ldots(q_{m},q_{m+1},\vec{y}_{m})$. Let $\pi$ be the computation corresponding to $\rho$ with the initial counter values being $\vec{g}$. Then, the value of counters at the position $i$ in $\pi$ is $\vec{g}+\sum_{j=1}^{i-1}\vec{y}_{j}$. Therefore, the sum of values over $\rho$ starting with counter values $\vec{g}\in\mathbb{Z}^{k}$, denoted by $\mathsf{Sum}_{\vec{g}}(\rho)$, is given by the following formula:

[TABLE]

We have the following:

Lemma 11**.**

There exists a regular computation $\pi$ with $\textsc{LimAvg}(f(\pi))\leq 0$ if and only if there exist paths $\rho_{1},\rho_{2}$ such that

1. (C1)

$\rho_{1}(\rho_{2})^{\omega}$* is an infinite path and $\rho_{2}$ is a cycle,* 2. (C2)

$\textsc{Gain}(\rho_{2})\cdot\textsc{Vals}(\rho_{2})=0$, and 3. (C3)

$\mathsf{Sum}_{\textsc{Gain}(\rho_{1})}(\rho_{2})\leq 0$.

The proof of Lemma 11 has been relegated to the appendix.

Due to results from the previous section, we can check in NP the existence of $\rho_{1},\rho_{2}$ satisfying (C1) and (C2). We call a cycle $\rho_{2}$ balanced if $\textsc{Gain}(\rho_{2})\cdot\textsc{Vals}(\rho_{2})=0$. In the remaining part we focus on condition (C3), while keeping in mind (C1) and (C2).

The plan of the proof. The proof has three key ingredients which are as follows: factorizations, quadratic factor elimination, and the linear case.

• •

Factorizations. We show that we can consider only paths $\rho_{2}$ of the form

[TABLE]

where $|\alpha_{i}|,|\beta_{i}|\leq|\mathcal{A}|$ and each $\beta_{i}$ is a distinct simple cycle (Lemma 13). It follows that $p$ is exponentially bounded in $|\mathcal{A}|$. Next, we show that for $\rho_{2}$ in such a form we have

[TABLE]

where $\mathbf{B}\in\mathbb{Z}^{p\times p},\vec{c}\in\mathbb{Z}^{p}$ (Lemma 14). Therefore, $\mathsf{Sum}_{\textsc{Gain}(\rho_{1})}(\rho_{2})\leq 0$ can be presented as an instance of integer quadratic programming, where the variables correspond to multiplicities of simple cycles.

However, there are two problems to overcome. First, $\rho_{2}$ has to be balanced, i.e., it has to satisfy $\textsc{Gain}(\rho_{2})\cdot\textsc{Vals}(\rho_{2})=0$, which introduces another quadratic equation. Solving a system of two quadratic equations over integers is considerably more difficult (see [13] for references). Second, $p$ is (bounded by) the number of distinct simple cycles and hence it can be exponential in $|\mathcal{A}|$. Therefore, $\mathbf{B}$ and $\vec{c}$ may have exponential size (of the binary representation) in $|\mathcal{A}|$.

• •

Quadratic factor elimination. To solve these problems, we fix a sequence $\textsc{Tpl}=(\alpha_{0},\beta_{1},\alpha_{1},\ldots,\beta_{p},\alpha_{p})$ and consider $\mathbf{B}_{\textsc{Tpl}},\vec{c}_{\textsc{Tpl}},e_{\textsc{Tpl}}$ for Tpl. We show that one of the following holds (Lemma 15 and Lemma 17):

• –

$\vec{n}^{T}\mathbf{B}_{\textsc{Tpl}}\vec{n}+\vec{c}_{\textsc{Tpl}}\cdot\vec{n}+e_{\textsc{Tpl}}\leq 0$ has a simple solution, or

• –

there exist $\vec{d}_{\textsc{Tpl}}\in\mathbb{Z}^{p},h_{\textsc{Tpl}}\in\mathbb{Z}$ such that for all vectors $\vec{n}$, if the cycle $\rho_{2}=\alpha_{0}\beta_{1}^{n[1]}\ldots\beta_{p}^{n[p]}\alpha_{p}$ is balanced (C2), then

[TABLE]

We can decide in non-deterministic polynomial time whether the first condition holds (Lemma 22).

• •

The linear case. Assuming that the second condition holds, we reduce the problem of solving the quadratic inequality $\vec{n}^{T}\mathbf{B}_{\textsc{Tpl}}\vec{n}+\vec{c}_{\textsc{Tpl}}\cdot\vec{n}+e_{\textsc{Tpl}}\leq 0$ to solving the linear inequality

[TABLE]

Moreover, we can compute $\vec{d}_{\textsc{Tpl}},h_{\textsc{Tpl}}$ from the sequence Tpl. At this point, we can solve the problem in non-deterministic exponential time. Next, we argue that we do not have to compute the whole system.

We show that if $(\vec{c}_{\textsc{Tpl}}+\vec{d}_{\textsc{Tpl}})\cdot\vec{n}+e_{\textsc{Tpl}}+h_{\textsc{Tpl}}\leq 0$ has a solution, then it has a solution for a vector $\vec{n}_{0}$ with $m=O(|\mathcal{A}|)$ non-zero components. Therefore, we can remove cycles corresponding to [math] coefficients of $\vec{n}_{0}$. Still, $\sum_{i=0}^{p}|\alpha_{i}|$ can be exponential in $|\mathcal{A}|$, but this operation shortens the size of the template, i.e., the value $\sum_{i=0}^{p}|\alpha_{i}|+\sum_{i=1}^{p}|\beta_{i}|$, and hence by iterating it we get a polynomial size template, which yields a polynomial-size system of inequalities. These inequalities can be solved in NP.

We now present the details of each ingredient.

4.2.1 Factorizations

The regular finite-value problem has been solved via reduction to solving (quadratic and linear) inequalities. In this section, we show a reduction of the regular average-value problem to linear and quadratic inequalities as well. First, we establish that we can consider only cycles $\rho$, which have a compact representation using templates parametrized by multiplicities of cycles. The value $\mathsf{Sum}_{\vec{g}}(\rho)$ for a cycle represented by a template is given by a quadratic function in the multiplicities of cycles.

Templates and multiplicities. A template Tpl is a sequence of paths $(\alpha_{0},\beta_{1},\alpha_{1},\ldots,\beta_{p},\alpha_{p})$ such that all $\beta_{1},\ldots,\beta_{p}$ are cycles and $\alpha_{0}\beta_{1}\alpha_{1}\ldots\beta_{p}\alpha_{p}$ is a cycle. A template is minimal if for all $i\in\{0,\ldots,p\}$ we have $|\alpha_{i}|<|Q|$ and all $\beta_{i}$ are pairwise distinct simple cycles. For every vector $\vec{n}\in\mathbb{N}^{p}$, called multiplicities, we define $\textsc{Tpl}(\vec{n})$ as a cycle

[TABLE]

A cycle $\rho$ has a (minimal) factorization if there exists a (minimal) template and multiplicities $\vec{n}$ such that $\rho=\textsc{Tpl}(\vec{n})$.

Observe that every cycle $\rho$ has a factorization such that for all $i$ we have $|\alpha_{i}|<|Q|$ and each $\beta_{i}$ is a simple cycle. However, the sequence $\beta_{i}$’s can have repetitions. The following lemma states that if a cycle $\beta$ occurs twice in $\rho$, then we can group them together.

Lemma 12** (Cycle grouping).**

Consider $\vec{g}\in\mathbb{Z}^{k}$ and a cycle $\alpha_{0}\beta\alpha_{1}\beta\alpha_{2}$. Then, one of the following holds:

[TABLE]

Proof sketch.

To show the lemma observe that

[TABLE]

∎

Careful repeated application of Lemma 12 implies that we can look for a cycle $\rho$ satisfying (C1), (C2) and (C3) among cycles that have a minimal factorization:

Lemma 13**.**

For every cycle $\rho$ and $\vec{g}\in\mathbb{Z}^{k}$, there exists a cycle $\rho^{\prime}$ that has a minimal factorization (4.2.1) such that $\textsc{Gain}(\rho)=\textsc{Gain}(\rho^{\prime})$, $\textsc{Vals}(\rho)=\textsc{Vals}(\rho^{\prime})$ and $\mathsf{Sum}_{\vec{g}}(\rho)\geq\mathsf{Sum}_{\vec{g}}(\rho^{\prime})$.

Proof sketch.

Note that repeated application of Lemma 12 allows us to group simple cycles together but it may create connecting paths of length greater than $|Q|$. In such a case, we extract simple cycles from long connecting paths and group them together again using Lemma 12. Such process terminates as in each iteration it either decreases the sum of lengths’ of connecting paths or does not change this sum but decreases the number of (non-grouped) cycles. Note that the initial cycle $\rho$ and the resulting cycle $\rho^{\prime}$ have the same multisets of transitions and hence $\textsc{Gain}(\rho)=\textsc{Gain}(\rho^{\prime})$ and $\textsc{Vals}(\rho)=\textsc{Vals}(\rho^{\prime})$. It follows that this process preserves condition (C2). ∎

Consider a template $\textsc{Tpl}=(\alpha_{0},\beta_{1},\alpha_{1},\ldots,\beta_{p},\alpha_{p})$. We present $\mathsf{Sum}_{\vec{g}}(\textsc{Tpl}(\vec{n}))$ as a function from multiplicities of simple cycles $\vec{n}\in\mathbb{N}$ into $\mathbb{Z}$. First, observe that

[TABLE]

The expression $\textsc{Vals}(\textsc{Tpl}(\vec{n}))$ is a linear expression in $\vec{n}$ with natural coefficients, and the expression $\mathsf{Sum}_{\vec{0}}(\textsc{Tpl}(\vec{n}))$ is a quadratic function in each of its arguments $\vec{n}$.

Lemma 14**.**

Given a template Tpl we can compute in polynomial time in $|\textsc{Tpl}|+|\mathcal{A}|+|f|$, a symmetric matrix $\mathbf{B}_{\textsc{Tpl}}\in\mathbb{Z}^{p\times p},\vec{c}_{\textsc{Tpl}}\in\mathbb{Z}^{p}$ and $e_{\textsc{Tpl}}\in\mathbb{Z}$ such that the following holds:

[TABLE]

Moreover, for all $i,j\in\{1,\ldots,p\}$ we have

[TABLE]

The proof of Lemma 14 has been relegated to the appendix.

Observe that $\mathbf{B}_{\textsc{Tpl}}$ is similar to the matrix $\mathbf{A}$ from (1). We exploit this similarity in the following section to eliminate the term $\vec{n}^{T}\mathbf{B}_{\textsc{Tpl}}\vec{n}$ if possible.

4.2.2 Elimination of the quadratic factor

We show how to simplify the expression (1) of Lemma 14 for $\mathsf{Sum}_{\vec{0}}(\textsc{Tpl}(\vec{n}))$. We show that either the inequality

[TABLE]

has a simple solution for every $\vec{g}$, or the quadratic term in (1) of Lemma 14 can be substituted with a linear term.

Negative and linear templates. Consider a template Tpl. A template Tpl is positive (resp., negative) if there exist multiplicities $\vec{n}_{1},\vec{n}_{2}\in\mathbb{N}^{p}$ such that

$\vec{n}_{1}^{T}\mathbf{B}_{\textsc{Tpl}}\vec{n}_{1}>0$ (resp., $\vec{n}_{1}^{T}\mathbf{B}_{\textsc{Tpl}}\vec{n}_{1}<0$), and 2. 2.

for every $t\in\mathbb{N}^{+}$, we have

[TABLE]

A template Tpl is linear if there exist $\vec{d}_{\textsc{Tpl}}\in\mathbb{Z}^{p}$ and $h_{\textsc{Tpl}}\in\mathbb{Z}$ such that for all $\vec{n}$, if $\textsc{Gain}(\textsc{Tpl}(\vec{n}))\cdot\textsc{Vals}(\textsc{Tpl}(\vec{n}))=0$, then $\vec{n}^{T}\mathbf{B}_{\textsc{Tpl}}\vec{n}=\vec{d}_{\textsc{Tpl}}\cdot\vec{n}+h_{\textsc{Tpl}}$.

We observe that the existence of a negative cycle Tpl implies that $\mathsf{Sum}_{\vec{g}}(\textsc{Tpl}(\vec{n}))\leq 0$ has a solution for every $\vec{g}\in\mathbb{N}^{k}$, which in turn implies that the answer to the average-value problem is YES. Basically, for $\rho^{t}$ defined as $\textsc{Tpl}(t\vec{n}_{1}+\vec{n}_{2})$ and $t$ big enough we can make $\mathsf{Sum}_{\vec{g}}(\rho^{t})$ arbitrarily small.

Lemma 15**.**

If there exist a negative template, whose any state is reachable from some initial state, then the answer to the regular average-value problem with threshold [math] is YES.

Proof sketch.

Assume that Tpl is negative and consider $\rho^{t}$ defined as $\textsc{Tpl}(t\vec{n}_{1}+\vec{n}_{2})$. Note that $2\cdot\mathsf{Sum}_{\vec{0}}(\rho^{t})=(t\vec{n}_{1}+\vec{n}_{2})^{T}\mathbf{B}_{\textsc{Tpl}}(t\vec{n}_{1}+\vec{n}_{2})+\vec{c}_{\textsc{Tpl}}(t\vec{n}_{1}+\vec{n}_{2})+e_{\textsc{Tpl}}$ is a quadratic polynomial in $t$ with the leading coefficient $\vec{n}_{1}^{T}\mathbf{B}_{\rho_{1}}\vec{n_{1}}$ negative, whereas $\vec{g}\cdot\textsc{Vals}(\rho^{t})$ is linear in $t$. Therefore, for $t$ big enough (which depends on $\vec{g}$) $\mathsf{Sum}_{\vec{g}}(\rho^{t})=\mathsf{Sum}_{\vec{0}}(\rho^{t})+\vec{g}\cdot\textsc{Vals}(\rho^{t})$ is negative and $\rho^{t}$ is balanced. It follows that $\rho_{1}$ leading from an initial state to the first state of Tpl and $\rho_{2}=\rho^{t}$ for $t$ big enough satisfy conditions (C1), (C2), (C3) of Lemma 11 and hence the answer to the average-value problem is YES. ∎

We show that either there is a template, which is negative or all templates are linear (Lemma 17). Next, we show that we can check in non-deterministic polynomial time whether there exists a negative template (Lemma 22). We start with an example presenting one of the main ideas.

Example 16**.**

Consider the VASS $\mathcal{A}_{e}$ and the cost function $f$ from Example 2. We consider balanced cycles $\rho$ starting in $B$. We know from Example 10 that in balanced cycles all transitions have the same number of occurrences. Therefore, $\rho$ is factorized into one of two minimal templates: $\textsc{Tpl}_{1}=(\epsilon,e_{1}e_{2},\epsilon,e_{3}e_{4},\epsilon)$ or $\textsc{Tpl}_{2}=(\epsilon,e_{3}e_{4},\epsilon,e_{1}e_{2},\epsilon)$.

[TABLE]

Since transitions have the same number of occurrences, the multiplicities of $e_{1}e_{2}$ and $e_{3}e_{4}$ are equal and hence we consider $\vec{n}$ such that $n[1]=n[2]$. For such vectors $\vec{n}$ we have $\vec{n}\mathbf{B}_{\textsc{Tpl}_{1}}\vec{n}=6(n[1])^{2}$ and $\vec{n}\mathbf{B}_{\textsc{Tpl}_{2}}\vec{n}=-6(n[1])^{2}$. Therefore, $\textsc{Tpl}_{1}$ is positive and $\textsc{Tpl}_{2}$ is negative.

Interestingly, $\vec{n}^{T}\mathbf{B}_{\textsc{Tpl}_{1}}\vec{n}=-\vec{n}^{T}\mathbf{B}_{\textsc{Tpl}_{2}}\vec{n}$. This is not a coincidence. Recall the matrix $\mathbf{A}^{\prime}$ from Example 10 and observe that $\mathbf{A}^{\prime}=\mathbf{B}_{\textsc{Tpl}_{1}}+\mathbf{B}_{\textsc{Tpl}_{2}}$. As we consider $\vec{v}$ such that $\vec{n}^{T}\mathbf{A}^{\prime}\vec{n}=0$ and hence the above equality follows.

Lemma 17**.**

(1) There exists a negative template or all templates are linear. (2) If there exists a positive template Tpl, then there exists a negative one of the size bounded by $|\textsc{Tpl}|^{2}$. (3) If a template Tpl is linear, we can compute $\vec{d}_{\textsc{Tpl}},h_{\textsc{Tpl}}$ in polynomial time in $|\textsc{Tpl}|+|\mathcal{A}|+|f|$.

Proof ideas.

Consider a template Tpl with all connecting paths being empty, i.e., $\textsc{Tpl}=(\epsilon,\beta_{1},\ldots,\beta_{p},\epsilon)$. Let $\vec{n}$ be a vector of multiplicities such that a cycle $\textsc{Tpl}(\vec{n})$ is balanced, i.e., $\textsc{Gain}(\textsc{Tpl}(\vec{n}))\cdot\textsc{Vals}(\textsc{Tpl}(\vec{n}))=0$. Then, $\textsc{Tpl}(t\vec{n})$ is balanced for all $t\in\mathbb{N}$. We consider three cases:

The case $\vec{n}^{T}\mathbf{B}_{\textsc{Tpl}}\vec{n}<0$. Then, Tpl is negative. Vectors $\vec{n}_{1}=\vec{n}$ and $\vec{n}_{2}=\vec{0}$ witness negativity.

The case $\vec{n}^{T}\mathbf{B}_{\textsc{Tpl}}\vec{n}>0$. Then, Tpl is positive and we show that the template with reversed cycles $\textsc{Tpl}^{R}=(\epsilon,\beta_{p},\ldots,\beta_{1},\epsilon)$ is negative.

First, observe that $\textsc{Gain}(\textsc{Tpl}(\vec{n}))\cdot\textsc{Vals}(\textsc{Tpl}(\vec{n}))=0$ can be stated as a matrix equation $\vec{n}^{T}\mathbf{A}\vec{n}=0$, where for all $i,j$ we have

[TABLE]

This can be derived in virtually the same way as in Section 4.1. Next, recall from Lemma 14 that $\mathbf{B}_{\textsc{Tpl}}$ is similar to $\mathbf{A}$. For all $i,j$ we have

[TABLE]

A similar identity holds for $\textsc{Tpl}^{R}$, but $i,j$ are substituted by respectively $p-i+1$ and $p-j+1$ and $\min$ is swapped with $\max$. In consequence, we have

[TABLE]

Therefore, for all $i,j$ we have

[TABLE]

It follows that

[TABLE]

where $\vec{n}_{R}$ is the reversed vector $\vec{n}$. Note that $\textsc{Tpl}^{R}(\vec{n}_{R})$ has the same multiset of transitions as $\textsc{Tpl}^{R}(\vec{n}_{R})$, and hence $\textsc{Tpl}^{R}(\vec{n}_{R})$ is balanced, and $\textsc{Tpl}^{R}(t\vec{n}_{R})$ is balanced for all $t\in\mathbb{N}$. It follows that $\textsc{Tpl}^{R}$ is negative.

The above two cases fail. Then for all $\vec{n}$, if $\textsc{Gain}(\textsc{Tpl}(\vec{n}))\cdot\textsc{Vals}(\textsc{Tpl}(\vec{n}))=0$, then $\vec{n}^{T}\mathbf{B}_{\textsc{Tpl}}\vec{n}=0$. Therefore, Tpl is linear with $\vec{d}_{\textsc{Tpl}},h_{\textsc{Tpl}}$ being $\vec{0}$ and [math] respectively. In the general case, if the connecting paths are non-empty, then $\vec{d}_{\textsc{Tpl}},h_{\textsc{Tpl}}$ need not be [math]. Intuitively, $\textsc{Gain}(\textsc{Tpl}(\vec{n}))\cdot\textsc{Vals}(\textsc{Tpl}(\vec{n}))$ depends on the whole template whereas $\mathbf{B}_{\textsc{Tpl}}$ depends only on the cycles of Tpl. The expression $\vec{d}_{\textsc{Tpl}}\cdot\vec{n}+h_{\textsc{Tpl}}$ accounts for that difference.

Essentially the same line of reasoning can be applied if the connecting paths in Tpl are non-empty. However, the argument becomes more technical. We present it in full detail in the appendix. ∎

Now, we discuss how to check whether there exists a negative template. One of the conditions of negativity is that $\textsc{Gain}(\textsc{Tpl}(t\vec{n}_{1}+\vec{n}_{2}))\cdot\textsc{Vals}(\textsc{Tpl}(t\vec{n}_{1}+\vec{n}_{2}))=0$. Recall that Gain and Vals depend on the multiset of transitions, but not on the order of transitions. Therefore, for a given template Tpl, we define $\textsc{Trans}_{\textsc{Tpl}}(\vec{n})\in\mathbb{N}^{m}$, where $m=|\delta|$, as the vector of multiplicities of transitions in $\textsc{Tpl}(\vec{n})$. We will write $\textsc{Trans}(\vec{n})$ if Tpl is clear from the context.

Lemma 18**.**

Let Tpl be a template and let $\vec{n}\in\mathbb{N}^{p}$ be a vector of multiplicities. There exist $r_{1},\ldots,r_{\ell}\in\mathbb{Q}^{+}$ and $\vec{z}_{1},\ldots,\vec{z}_{\ell}\in\mathbb{N}^{p}$ such that

1. (1)

$supp(\vec{z}_{i})\leq m$* (the number of transitions of $|\mathcal{A}|$),* 2. (2)

there exists $t\in\mathbb{N}^{+}$ such that $\textsc{Trans}(\vec{z}_{i})=t\cdot\textsc{Trans}(\vec{n})$, and 3. (3)

$\vec{n}=\sum_{i=1}^{\ell}r_{i}\vec{z}_{i}$.

Remark. The condition $\textsc{Trans}(\vec{z}_{i})=t\cdot\textsc{Trans}(\vec{n})$ implies that if the cycle $\textsc{Tpl}(\vec{n})$ is balanced, then all the cycles $\textsc{Tpl}(\vec{z}_{1}),\ldots,\textsc{Tpl}(\vec{z}_{\ell})$ are balanced as well.

Proof ideas.

First, observe that Trans is a linear function transforming vectors from $\mathbb{N}^{p}$ into vectors from $\mathbb{N}^{m}$. The value $p$ can be exponential w.r.t. $m=|\delta|$ and hence we show that each vector from $\mathbb{N}^{p}$ can be presented as a linear combination over $\mathbb{Q}^{+}$ of vectors with polynomially-bounded supports.

The full proof has been relegated to the appendix. ∎

Next, we show that if there exists a negative template, then there exists one of polynomial size.

Lemma 19**.**

If there exists a negative template, then there exists one of polynomial size in $|\textsc{Tpl}|+|\mathcal{A}|+|f|$.

Proof ideas.

Assume that a template Tpl is positive (resp., negative). Let $\vec{n}_{1},\vec{n}_{2}\in\mathbb{N}^{p}$ be the vectors witnessing positivity (resp., negativity). Then, using Lemma 18, we show that there exist $\vec{n}_{1}^{0},\vec{n}_{2}^{0}$ that witness template Tpl being positive or negative and the support of both $\vec{n}_{1}^{0},\vec{n}_{2}^{0}$ is bounded by $|\delta|$. We remove from Tpl cycles corresponding to coefficient [math] in both $\vec{n}_{1}^{0}$ and $\vec{n}_{2}^{0}$. We get a template with polynomially many cycles. If all connecting paths are still bounded by $|Q|$ we terminate with Tpl of polynomial size. However, as we remove some cycles, some connecting path are concatenated and in the result we get connecting paths longer than $|Q|$. For such connecting path, we extract simple cycles and group them (as in Lemma 13). We get another minimal template $\textsc{Tpl}^{\prime}$ shorter than Tpl, which is positive or negative. By iterating this process, we get a polynomial-size template $\textsc{Tpl}^{\neq 0}$, which is positive or negative. Then, by Lemma 17 there exists a negative template of polynomial size.

The full proof has been relegated to the appendix. ∎

Still, to check whether there exists a negative template we have to solve a system consisting of a quadratic inequality $\vec{n}_{1}^{T}\mathbf{B}_{\textsc{Tpl}}\vec{n}_{1}<0$ and a quadratic equation, which corresponds to $\textsc{Gain}(\textsc{Tpl}(t\vec{n}_{1}+\vec{n}_{2}))\cdot\textsc{Vals}(\textsc{Tpl}(t\vec{n}_{1}+\vec{n}_{2}))=0$. We show that this quadratic equation can be transformed into a system of linear inequalities.

Lemma 20**.**

Let Tpl be a template. There exist systems of linear equations and inequalities $S_{1},\ldots,S_{l}$ such that (1) each $S_{i}$ has polynomial size in $|\textsc{Tpl}|+|\mathcal{A}|+|f|$, (2) for all $\vec{n}\in\mathbb{N}^{p}$ we have $\textsc{Gain}(\textsc{Tpl}(\vec{n}))\cdot\textsc{Vals}(\textsc{Tpl}(\vec{n}))=0$ if and only if for some $i$ the vector $\vec{n}$ satisfies $S_{i}$.

Proof ideas.

We construct a matrix $\mathbf{A}\in\mathbb{Z}^{(p+1)\times(p+1)}$ such that for every $\vec{n}\in\mathbb{N}^{p}$ we have $\textsc{Gain}(\textsc{Tpl}(\vec{n}))\cdot\textsc{Vals}(\textsc{Tpl}(\vec{n}))=0$ if and only if for $\vec{n}_{1}=(n[1],\ldots,n[p],1)$ we have $\vec{n}_{1}^{T}\mathbf{A}\vec{n}_{=}0$. Moreover, we know that for all $\vec{n}_{1}\in\mathbb{N}^{p+1}$ we have $\vec{n}_{1}^{T}\mathbf{A}\vec{n}_{1}\geq 0$. We carry out standard elimination of quadratic terms using the quadratic formula on the successive variables in $\vec{n}_{1}^{T}\mathbf{A}\vec{n}_{1}$. Such a procedure involves computing squares in each step ($\Delta=b^{2}-4ac$) and hence it can lead to coefficients of double-exponential order in $p+1$ (the number of dimensions). However, due to condition $\vec{n}_{1}^{T}\mathbf{A}\vec{n_{1}}\geq 0$ for all $\vec{n}_{1}\in\mathbb{N}^{p+1}$, we can show that for every $i$ either $x[i]=0$ or $x[i]$ has to be a double root ($\Delta=0$) and hence it can be described with a simple equation, which is of polynomial size.

The full proof has been relegated to the appendix. ∎

Finally, Lemma 19 and Lemma 20 imply that existence of a negative template can be solved in NP via reduction to integer quadratic programming.

Lemma 21**.**

We can verify in NP whether a given $\textsc{VASS}(\mathbb{Z},k)$ $\mathcal{A}$ has a negative template.

Proof sketch.

We non-deterministically pick a template Tpl of polynomial size (Lemma 19). Then, we non-deterministically pick a system $S_{i}$ for template (Lemma 20). We make two copies of $S_{i}$: $S_{i}^{1}$ and $S_{i}^{2}$; in one we substitute $\vec{n}$ with $\vec{n}_{2}$ and in the other with $\vec{n}_{1}+\vec{n}_{2}$. It follows that for all $t\in\mathbb{R}$ the vector $t\vec{n}_{1}+\vec{n}_{2}$ satisfies $S_{i}$ (substituted for $\vec{n}$). Finally, we solve an instance of integer quadratic programming consisting of $\vec{n}_{1}\mathbf{B}_{\textsc{Tpl}}\vec{n}_{1}-1\leq 0$ and linear equations and inequalities $S_{i}^{1}$ and $S_{i}^{2}$, which is an instance of integer quadratic programming and hence can be solved in NP [13]. ∎

4.2.3 The linear case

We consider the final case, where all templates are linear. The decision procedure described in the following lemma answers YES (in at least one of non-deterministic computations) whenever the answer to the regular average-value problem with threshold [math] is YES and all templates are linear. Thus, it is complete.

Our main algorithm assumes that all templates are linear if it fails to find a negative template. The failure can be due to a wrong non-deterministic pick. Having that in mind, we make sure that the decision procedure from the following lemma is sound regardless of the linearity of templates, i.e., if it answers YES, then the answer to the regular average-value problem with threshold [math] is YES.

Lemma 22**.**

Assume that all templates are linear. Then, we can solve the regular average-value problem with threshold [math] in non-deterministic polynomial time. Moreover, the procedure is sound irrespectively of the linearity assumption.

Proof sketch.

First, we show that using Lemma 18, if there is a cycle $\rho$ with (a) $\textsc{Gain}(\rho)\cdot\textsc{Vals}(\rho)=0$ and (b) $\mathsf{Sum}_{\vec{g}}(\rho)\leq 0$, then there is a cycle $\rho^{\prime}$ defined by a template of polynomial size satisfying both conditions (a) and (b).

Assume that for some $\vec{g}\in\mathbb{Z}^{k}$ we have

$\mathsf{Sum}_{\vec{g}}(\rho)\leq 0$ and 2. 2.

$\textsc{Gain}(\rho)\cdot\textsc{Vals}(\rho)=0$.

Then, there exists a minimal template Tpl and a vector of multiplicities $\vec{n}$ such that $\textsc{Tpl}(\vec{n})=\rho$ (Lemma 13). As Tpl is linear, then we can compute in polynomial time $\vec{d}_{\textsc{Tpl}}\in\mathbb{Z}^{p},h_{\textsc{Tpl}}\in\mathbb{Z}$, which are polynomial in $|\textsc{Tpl}|+|\mathcal{A}|+|f|$ such that

[TABLE]

We apply Lemma 18 to vector $\vec{n}$ and get $\vec{n}=\sum_{i=1}^{\ell}r_{i}\vec{z}_{i}$, with $\vec{z}_{i},r_{i}$ satisfying the statement of Lemma 18. Observe that for some $i$, we have $\mathsf{Sum}_{\vec{g}}(\textsc{Tpl}(\vec{z}_{i}))\leq 0$. As $\textsc{Trans}(\vec{z}_{i})=t\cdot\textsc{Trans}(\vec{n})$, we have

[TABLE]

Therefore, $\textsc{Tpl}(\vec{z}_{i})$ is a balanced cycle with $\mathsf{Sum}_{\vec{g}}(\textsc{Tpl}(\vec{z}_{i}))\leq 0$. As $supp(\vec{z}_{i})\leq|\delta|$, we remove from Tpl cycles that correspond to [math] components in $\vec{z}_{i}$. Again, Tpl may not be minimal so, as in the proof of Lemma 13, we extract simple cycles and iterate the process until we get $\textsc{Tpl}^{\prime}$ of polynomial size such that $\textsc{Tpl}^{\prime}$ with some multiplicities defines a cycle $\rho^{\prime}$, which satisfies $\mathsf{Sum}_{\vec{g}}(\rho^{\prime})\leq 0$ and $\textsc{Gain}(\rho^{\prime})\cdot\textsc{Vals}(\rho^{\prime})=0$.

Second, consider a template Tpl of polynomial size. We nondeterministically pick a subset of states $Q$ and write a system of equations $S_{\textsc{Gain}}^{Q}$ over variables $\vec{x},\vec{y}$ such that $\vec{x},\vec{y}$ is a solution of $S_{\textsc{Gain}}^{Q}$ if and only if there exists a path $\rho_{1}$ satisfying (a) $\vec{x}$ are multiplicities of transitions along $\rho_{1}$ (b) $\rho_{1}$ is from some initial state of $\mathcal{A}$ to the first state of Tpl, (c) $\rho_{1}$ visits all states from $Q$, (d) $\vec{y}=\textsc{Gain}(\rho_{1})$. To write $S_{\textsc{Gain}}^{Q}$ we specify that all states from $Q$ have equal in-degree and out-degree except for the initial state of $\mathcal{A}$ , in which out-degree is greater than in-degree by $1$, and the first state of Tpl, where in-degree is greater than out-degree by $1$.

In summary, if all templates are linear, then there exist $\rho_{1},\rho_{2}$ defining a regular computation of the average value at most [math] if and only if the following holds: there is a subset of states $Q$ and a template Tpl of polynomial size such that the system of inequalities consisting of $S^{Q}_{\textsc{Gain}}$ and the inequality

[TABLE]

has a solution over natural numbers. Note that all the components except for $\vec{y}\cdot\textsc{Vals}(\textsc{Tpl}(\vec{n}))$ are linear. Since $\vec{y}$ and $\vec{n}$ are variables, the component $\vec{y}\cdot\textsc{Vals}(\textsc{Tpl}(\vec{n}))$ is quadratic. Still, $S^{Q}_{\textsc{Gain}}$ with $\eqref{eq:linear-case}$ is an instance of integer quadratic programming, which can be solved in NP [13].

We have assumed that Tpl is linear. However, we cannot check that deterministically in polynomial time. Still, linearity of Tpl is necessary only for the completeness of the above procedure. We can make sure that the answer is sound irrespectively of that assumption. Having a solution of the system, we can compute in polynomial time $\textsc{Gain}(\rho_{1})$ and $\mathsf{Sum}_{\textsc{Gain}(\rho_{1})}(\textsc{Tpl}(\vec{n}))$ and then verify $\mathsf{Sum}_{\textsc{Gain}(\rho_{1})}(\textsc{Tpl}(\vec{n}))\leq 0$. ∎

4.2.4 Summary

We present a short summary of the non-deterministic procedure deciding whether a given $\textsc{VASS}(\mathbb{Z},k)$ $\mathcal{A}$ has a regular computation of the value at most [math]. We assume that all states in $\mathcal{A}$ are reachable from initial states.

• •

Step 1. We check whether there is a cycle $\rho$ with $\textsc{Gain}(\rho)\cdot\textsc{Vals}(\rho)<0$. We can do it in non-deterministic polynomial time (Lemma 9). If the answer is YES, then the answer to the average-value problem is YES (Lemma 7). Otherwise, we proceed.

• •

Step 2. We check whether there exists a negative template in $\mathcal{A}$. We can do it in non-deterministic polynomial time (Lemma 21). If the answer is YES, then the answer to the regular average-value problem is YES (Lemma 15). Otherwise, we proceed.

• •

Step 3. Assuming that the previous steps failed, all templates are linear. Then, we can solve the regular average-value problem in non-deterministic polynomial time (Lemma 22). Note that Step 2, could have failed due to unfortunate non-deterministic pick. However, the procedure from Lemma 22 is sound regardless of the linearity assumption.

In consequence, we have the main result of this section:

Lemma 23**.**

The regular average-value problem for $\textbf{VASS}(\mathbb{Z})$ with (general) cost functions is in NP.

4.3 Hardness

We show that the regular finite-value and the regular average-value problems are NP-hard. The proof is via reduction from the 3-SAT problem. Given a 3-CNF formula $\varphi$ over $n$ variables, we construct a VASS of dimension $2n$, where dimensions correspond to literals in $\varphi$. Each simple cycle $\rho$ in the VASS consists of two parts: The first part corresponds to picking a substitution $\sigma$, which is stored in the vector $\textsc{Gain}(\rho)$. The second part ensures that $\textsc{Gain}(\rho)\cdot\textsc{Vals}(\rho)=0$ if $\sigma$ satisfies $\varphi$ and it is strictly positive otherwise. Therefore, if $\varphi$ is satisfiable, the VASS has a regular run of the average cost [math], and otherwise all its regular runs have infinite average cost. In consequence, we have the following:

Lemma 24**.**

The regular finite-value and the regular average-value problems for $\textbf{VASS}(\mathbb{Z})$ with (general) cost functions are NP-hard.

Proof.

Let $\varphi$ be a propositional formula in $3$-CNF with $n$ variables and $l$ clauses. We construct a $\textsc{VASS}(\mathbb{Z},2n)$ $\mathcal{A}_{\varphi}$ such that (1) if $\varphi$ is satisfiable, then $\mathcal{A}_{\varphi}$ has a regular computation of value [math], and (2) otherwise, all regular computations of $\mathcal{A}_{\varphi}$ have infinite value.

The VASS $\mathcal{A}_{\varphi}$, presented in Figure 2, consists of two parts. The first part consists of the states $q_{0},\ldots,q_{n}$, where $q_{0}$ is initial in $\mathcal{A}_{\varphi}$. It corresponds to picking a variable substitution. For every $i\in\{0,\ldots,n-1\}$, there are two transitions $(q_{i-1},q_{i},\mathbf{1}_{i})$ and $(q_{i-1},q_{i},\mathbf{1}_{i+n})$, i.e., transitions from $q_{i-1}$ to $q_{i}$ incrementing the $i$-th or $(i+n)$-th counter. Upon reaching $q_{n}$, the vector of counter values $\vec{g}$ has exactly $n$ components with value $1$ while other have value [math]. The vector $\vec{g}$ defines variable valuation $\sigma_{\vec{g}}$ defined as follows. A variable $p_{j}$ is valuated to true, if $g[j]=1$, and it is false if $g[j+n]=1$. The cost function $f$ in the first part is [math] for all states.

In the second part the values of counters do not change, but the cost function $f$ is non-zero. We use this part to ensure that the average value is [math] if and only if $\sigma_{\vec{g}}$ satisfies $\varphi$. This part consists of $l$ layers, each consisting of $3$ states. At the $j$-th layer, corresponding to the clause $c_{j}=l_{1}\vee l_{2}\vee l_{3}$, we define the cost function $f$ on states $q_{j,1},q_{j,2},q_{j,3}$ such that $f(q_{j,i},\vec{g})$ returns the value of the component of $\vec{g}$ corresponding to $\neg l_{i}$. It follows that $\sigma_{\vec{g}}$ satisfies $c_{j}$ if and only if for one of these $3$ states we have $f(q_{j,i},\vec{g})=0$. Therefore, a single cycle over $\mathcal{A}$ has the average [math] if and only if $\sigma_{\vec{g}}$ satisfies $\varphi$.

It follows that if $\varphi$ has a satisfying valuation, then $\mathcal{A}_{\varphi}$ has a regular computation of the average value [math]. Conversely, if $\varphi$ is unsatisfiable, then for every simple cycle $\rho$ we have $\textsc{Gain}(\rho)\cdot\textsc{Vals}(\rho)>0$. Since all weights are non-negative, it follows that for all cycles $\rho$ we have $\textsc{Gain}(\rho)\cdot\textsc{Vals}(\rho)>0$ and hence all regular computations of $\mathcal{A}_{\varphi}$ have the value $+\infty$.

∎

The main results of this section (Lemma 9, Lemma 23 and Lemma 24) summarize to Theorem 6. We leave the case of non-regular runs as an open question.

Open question 25**.**

What is the complexity of the average-value and finite-value problems for $\textbf{VASS}(\mathbb{Z})$?

5 General cost functions and $\textbf{VASS}(\mathbb{N})$

We show that the average-value and the regular average-value problems are undecidable.

The proofs are via reduction from the halting problem for Minsky machines [19], which are automata with two natural-valued registers $r_{1},r_{2}$. There are two main differences between Minsky machines and $\textbf{VASS}(\mathbb{N})$. First, the former can perform zero- and nonzero-tests on their registers, while the latter can take any transition as long as the counters’ values remain non-negative. Second, the halting problem for Minsky machines is qualitative, i.e., the answer is YES or NO. We consider quantitative problems for VASS, where we are interested in the values assigned to computations. We exploit the quantitative features of our problems to simulate zero- and nonzero-tests.

Theorem 26**.**

The average-value and the regular average-value problems for $\textbf{VASS}(\mathbb{N})$ with (general) cost functions are undecidable.

Proof sketch.

We first sketch the reduction from the halting problem for Minsky machines to the regular average-value problem for $\textbf{VASS}(\mathbb{N})$. To ease the presentation, we use Büchi conditions, which can be eliminated.

Consider a Minsky machine $\mathcal{M}$ and let $I$ be its set of instructions. We construct a $\textsc{VASS}(\mathbb{N})$ $\mathcal{A}$, which for presentation purposes has transitions labeled with the alphabet $I\cup\{\#\}$, that satisfies the following. Every regular computation labeled by $vu^{\omega}\in(I\cup\{\#\})^{\omega}$ has the average value [math] if and only if $u$ is of the form $u_{1}\#\ldots u_{k}\#$ and all words $u_{1},\ldots,u_{k}$ encode terminating computations of $\mathcal{M}$. First, we can construct an automaton without counters, which verifies that for every subword of the form $\#v\#$, with $v\in I^{*}$, $v$ encodes a terminating computations provided that all zero and non-zero test are correct. We can ensure that the cycle contains at least one transition labeled by $\#$ using a Büchi condition. This condition can be also enforced with additional counters. Such an automaton can be then encoded in the states of $\mathcal{A}$.

Second, to verify correctness of instructions w.r.t. the registers, we use counters $c_{1},c_{2}$ in $\mathcal{A}$, which track the values of the registers minus $1$, i.e., the value of $c_{i}$ in $\mathcal{A}$ is the maximum of [math] and the value of the $i$-th register $r_{i}$ in $\mathcal{M}$. The VASS $\mathcal{A}$ stores in its state whether the value of $r_{i}$ is [math], $1$ or the value of $c_{i}$ plus $1$. With that information, the VASS $\mathcal{A}$ can verify correctness of the instructions of $\mathcal{M}$.

However, transitions of $\mathcal{A}$ do not depend on the values of counters and hence it can be in a state denoting that the value of $r_{i}$ is [math] or $1$, while the value of $c_{i}$ is greater than [math]. To ensure that this is not the case, the cost function $f$ returns the value of $c_{i}$ whenever $r_{i}$ is supposed to be [math] or $1$. This suffices to prove the correctness in the regular average-value case.

Consider a regular computation $\pi$ of the average [math] labeled with $v(u_{1}\#\ldots u_{k}\#)^{\omega}$. The values returned by the cost function are natural and hence for the average to by [math], the values at all positions need to be [math]. It follows that whenever $\mathcal{A}$ stipulates that the value of $r_{i}$ is [math] or $1$, then the value of $c_{i}$ is [math]. Thus, all zero- and non-zero tests in $u_{1},\ldots,u_{k}$ are correct and hence these words encode terminating computations of $\mathcal{M}$. This concludes the reduction the the regular average-value problem for $\textbf{VASS}(\mathbb{N})$.

In the average-value problem however, a computation of the value [math] may be labeled with a word of the form $u_{1}\#u_{2}\#\ldots$, where the lengths of $u_{i}$’s grow fast. In that case we cannot infer that there exists $i$ such that all values of $f$ along $u_{i}$ are [math]. However, using two additional counters, we can ensure that all words $u_{i}$ have length bounded by $|u_{0}|$. The first counter computes the value $|u_{1}|-|u_{2}|+|u_{3}|-\ldots$, while the second computes $|u_{2}|-|u_{3}|+|u_{4}|-\ldots$. Note that both counters are non-negative only if $|u_{2}|\leq|u_{1}|$, $|u_{3}|\leq|u_{2}|$, $|u_{4}|\leq|u_{1}|-|u_{2}|+|u_{3}|$. The first three inequalities imply $|u_{4}|\leq|u_{1}|$. We can show by induction that for all $i$ we have $|u_{i}|\leq|u_{0}|$. Therefore, the average-value is [math] only if there exists (exists infinitely many) words $u_{i}$ such that all values along this word are [math]. Then again, this word corresponds to a terminating computation of $\mathcal{M}$. Conversely, if $\mathcal{M}$ has a terminating computation and $u$ is its encoding, then $\mathcal{A}$ has a computation of the average value [math] that is labeled with $(\#u)^{\omega}$. ∎

Even though, the problems with an exact threshold are undecidable, we can decide existence of a regular computation of some finite value via reduction to reachability in VASS.

Theorem 27**.**

The regular finite-value problem for $\textbf{VASS}(\mathbb{N})$ with (general) cost functions is decidable.

Proof sketch.

Note that a $\textsc{VASS}(\mathbb{N},k)$ $\mathcal{A}$ has a regular computation of some finite value if and only if there exist finite paths $\rho_{1},\rho_{2}$ such that $\rho_{1}(\rho_{2})^{\omega}$ corresponds to a computation and for all counters which influence the average in $\rho_{2}$, the values of this counters do not change in a full iteration over $\rho_{2}$.

Assume that all counters influence $\rho_{2}$. We reduce the finite-value problem to the configuration reachability problem for $\textsc{VASS}(\mathbb{N},2k)$. Such a VASS $\mathcal{A}_{2k}$ first simulates $\mathcal{A}$ maintaining two copies $r_{i,1},r_{i,2}$ of each counter $c_{i}$. This phase of the $\mathcal{A}_{2k}$ computation corresponds to $\rho_{1}$. Then, $\mathcal{A}_{2k}$ nondeterministically picks a position, at it stores the current state of $\mathcal{A}$ and switches to the mode where it modifies only counters $r_{i,1}$. This phase corresponds to $\rho_{2}$. Again, $\mathcal{A}_{2k}$ non-deterministically picks the end of that phase and verifies that the last state is the same as the first of this phase. It remains to be verified that for all $i$ we have $r_{i,1}=r_{i,2}$. This is done by allowing to decrement $r_{i,1},r_{i,2}$ simultaneously. Then, the final value is $\vec{0}$ if and only if for all $i$, at the end of the second phase we have $r_{i,1}=r_{i,2}$. ∎

The above argument relies on regularity of computations. We leave the general case as an open question.

Open question 28**.**

Is the finite-value problem for $\textbf{VASS}(\mathbb{N})$ decidable?

6 VASS games

The problems we studied correspond to finding a suitable path is a configuration-graph of a VASS, which can be considered as a single-player game on a VASS. We briefly discuss a natural extension of our problems to two-player games on VASS, which are defined in a similar way to mean-payoff games on pushdown systems [10]. We consider infinite game arenas, in which the positions are the configurations of a VASS and moves correspond to transitions between configurations. The states of the VASS are partitioned into Player-1 and Player-2 states and it gives rise to the partition of configurations into Player-1 and Player-2 configurations. On such an arena we define the cost of each position as the cost of the configuration defined using the cost function. Finally, we consider two-player games with mean-payoff (cost) objectives; As consequences of our results we have the following:

As shown in Theorem 4, configuration reachability reduces to the average-value problem, and for $\textsc{VASS}(\mathbb{N})$-games configuration reachability is undecidable [5]. Hence the average-value problem is undecidable for $\textsc{VASS}(\mathbb{N})$-games. 2. 2.

Finite-state multidimensional total-payoff games straightforwardly reduce to the average-value problem for $\textsc{VASS}(\mathbb{Z})$-games; basically the counters track the total payoff and the general cost function specifies the multi-dimensional requirement. Finite-state multidimensional total-payoff games are undecidable [7], and hence the average-value problem for $\textsc{VASS}(\mathbb{Z})$-games is undecidable.

7 Conclusion

In this work we consider VASS with long-run average properties where the cost depends linearly on the values of the counters. For state-dependent and state-independent linear combinations we establish decidability and complexity results for VASS with integer-valued and natural-valued counters. We leave open some questions (see Open questions 5, 25, and 28) which are interesting directions for future work.

Acknowledgment

We would like to thank Petr Novotný for discussion on literature on VASS and the long-run average property.

8 Full proofs of selected lemmas

We prove Lemma 7 as a consequence of the proof of Lemma 11, and hence we show this after the proof of Lemma 11.

See 11

Proof.

Consider a regular computation $\pi$ let $\rho_{1}(\rho_{2})^{\omega}$ be the path corresponding to $\pi$. Assume that $\textsc{LimAvg}(f(\pi))\leq 0$. Then, there is a sequence of positions $n$ such that $\frac{1}{n}\sum_{i=1}^{n}f(\pi[i])$ converges to [math]. Without loss of generality, we assume these positions are aligned with full occurrences of $\rho_{2}$, i.e., $n=|\rho_{1}|+\ell\cdot|\rho_{2}|$. To see that, consider $r\in\{0,\ldots,|\rho_{2}|-1\}$ such that the infinite sequence of $n$’s has an infinite subsequence with the same remainder $r$ modulo $|\rho_{2}|$. Then, we can extend $\rho_{1}$ to $\rho_{1}^{\prime}$ so that $|\rho_{1}^{\prime}|$ modulo $|\rho_{2}|$ is $r$ and rotate the cycle $\rho_{2}$.

Therefore, we consider the sequence of partial averages

[TABLE]

where $n=|\rho_{1}|+\ell\cdot|\rho_{2}|$. First, observe that as $n$ tends to infinity, $\frac{1}{n}(\sum_{i=1}^{|\rho_{1}|}f(\pi[i])$ converges to [math]. Therefore, $\frac{1}{n}\sum_{i=|\rho_{1}|+1}^{n}f(\pi[i])$ converges to [math], and we study this term.

Let $m=|\rho_{2}|$ and $\rho_{2}=(q_{1},q_{2},\vec{y}_{1})\ldots(q_{m},q_{1},\vec{y}_{m})$. Observe that the value of the counters at the position $|\rho_{1}|+\ell\cdot|\rho_{2}|+i$ in $\pi$ equals

[TABLE]

and the state at this position is $q_{i}$. Let $l:Q\to\mathbb{N}^{k}$ be the labeling defining $f$. Then, we have

[TABLE]

Note that

[TABLE]

and hence

[TABLE]

Since $\textsc{Gain}(\rho_{2})\cdot\textsc{Vals}(\rho_{2})=0$ (Lemma 7) we have

[TABLE]

Since $\sum_{i=1}^{\ell m}f(\pi[|\rho_{1}|+i])$ tends to [math] as $\ell\to\infty$ we have $\mathsf{Sum}_{\textsc{Gain}(\rho_{1})}(\rho_{2})\leq 0$.

Therefore, $\textsc{LimAvg}(f(\pi))\leq 0$ implies that $\mathsf{Sum}_{\textsc{Gain}(\rho_{1})}(\rho_{2})\leq 0$. Observe that the converse implication holds as well. ∎

As the consequence of the above proof we have the following:

See 7

Proof.

This follows directly from the equation (4):

if $\textsc{Gain}(\rho_{2})\cdot\textsc{Vals}(\rho_{2})<0$, then $\lim_{\ell\to\infty}\sum_{i=1}^{m}f(\pi[|\rho_{1}|+(\ell m)+i])=-\infty$ and hence $\textsc{LimAvg}(f(\pi))=-\infty$, 2. 2.

if $\textsc{Gain}(\rho_{2})\cdot\textsc{Vals}(\rho_{2})=0$, then $\sum_{i=1}^{m}f(\pi[|\rho_{1}|+(\ell m)+i])$ is independent of $\ell$, and hence $\textsc{LimAvg}(f(\pi))=\sum_{i=1}^{m}f(\pi[|\rho_{1}|+i])$, which is finite, and 3. 3.

if $\textsc{Gain}(\rho_{2})\cdot\textsc{Vals}(\rho_{2})>0$ $\lim_{\ell\to\infty}\sum_{i=1}^{m}f(\pi[|\rho_{1}|+(\ell m)+i])=\infty$ and hence $\textsc{LimAvg}(f(\pi))=\infty$.

∎

See 14

Proof.

First, observe that for all $\vec{g},\vec{h}\in\mathbb{Z}^{k}$ we have

[TABLE]

Therefore,

[TABLE]

We repeatedly apply ($**$ ‣ 8) to $\mathsf{Sum}_{\vec{0}}(\textsc{Tpl}(\vec{n}))$, where

[TABLE]

and get

[TABLE]

Observe that

[TABLE]

Therefore, by applying (6) to (5) we get:

[TABLE]

[TABLE]

[TABLE]

It follows that $2\mathsf{Sum}_{\vec{0}}(\textsc{Tpl}(\vec{n}))$ can be presented as a quadratic function of the form

[TABLE]

Finally, the quadratic terms occur in (7) and (9). All quadratic terms in (7) are of the form $n[i]^{2}\textsc{Gain}(\beta_{i})\cdot\textsc{Vals}(\beta_{i})$ and all quadratic terms in (9) are of the form $n[i]n[j]\textsc{Gain}(\beta_{j})\cdot\textsc{Vals}(\beta_{i})$, where $j<i$. Therefore, the matrix $\mathbf{B}_{\textsc{Tpl}}$ is as in the statement. ∎

See 17

Proof.

Consider a template Tpl of the form

[TABLE]

and a vector $\vec{n}$ such that $\textsc{Tpl}(\vec{n})$ is balanced ($\textsc{Gain}(\textsc{Tpl}(\vec{n}))\cdot\textsc{Vals}(\textsc{Tpl}(\vec{n}))=0$.) We define $\beta_{p+1}$ as

[TABLE]

and we define $\vec{m}\in\mathbb{Z}^{p+1}$ as ${n}[i]={m}[i]$ for $i\in\{1,\ldots p\}$ and $m[p+1]=1$. We define an extended template $\textsc{Tpl}_{1}$ such that

[TABLE]

We distinguish three cases.

The case $\vec{m}^{T}\mathbf{B}_{\textsc{Tpl}_{1}}\vec{m}<0$. We show that $\textsc{Tpl}_{1}$ is negative. Consider vectors $\vec{n}_{2},\vec{n}_{2}$ such that

[TABLE]

Then, $\vec{n}_{1}^{T}\mathbf{B}_{\textsc{Tpl}_{1}}\vec{n_{1}}<0$ and $\textsc{Tpl}_{1}(t\vec{n}_{1}+\vec{n}_{2})$ has the same multiset of edges as $\textsc{Tpl}(\vec{n})$ repeated $t+1$ times. Therefore,

[TABLE]

and hence $\textsc{Tpl}_{1}$ is negative.

The case $\vec{m}^{T}\mathbf{B}_{\textsc{Tpl}_{1}}\vec{m}>0$. Similarly to the previous case, we can show that $\textsc{Tpl}_{1}$ is positive. However, we show that there exists a template $\textsc{Tpl}_{2}$, which is negative. To show that, we exhibit the connection between the equation $\textsc{Gain}(\textsc{Tpl}(\vec{n}))\cdot\textsc{Vals}(\textsc{Tpl}(\vec{n}))=0$ and $\vec{n}^{T}\mathbf{B}_{\textsc{Tpl}_{1}}\vec{n}$.

Since $\beta_{p+1}=\textsc{Tpl}(\vec{0})$ and $m[p+1]=1$ we have

[TABLE]

Therefore,

[TABLE]

Observe that the last equation can be presented as a quadratic form, i.e., consider a matrix $\mathbf{C}\in\mathbb{Z}^{(p+1)\times(p+1)}$ defined as for $i,j\in\{1,\ldots,p+1\}$ as

[TABLE]

Then,

[TABLE]

Recall, that for all $1\leq i,j\leq p+1$ we have

[TABLE]

Consider any template $\textsc{Tpl}_{2}$ with the same cycles as $\textsc{Tpl}_{1}$ but in the reverse order. Then, for all $1\leq i,j\leq p+1$ we have

[TABLE]

and hence

[TABLE]

It follows that $\mathbf{B}_{\textsc{Tpl}_{2}}$ equals $\mathbf{C}-\mathbf{B}_{\textsc{Tpl}_{1}}$ transposed along anti-diagonal, i.e., for all $1\leq i,j\leq p+1$ we have

[TABLE]

Therefore, $\vec{m}^{T}(\mathbf{C}-\mathbf{B}_{\textsc{Tpl}_{1}})\vec{m}$, which is less than [math], equals $\vec{m}_{R}^{T}\mathbf{B}_{\textsc{Tpl}_{2}}\vec{m}_{R}$, where $\vec{m}_{R}$ is the reversed vector $\vec{m}$.

It remains to show that there exists such $\textsc{Tpl}_{2}$ of the size bounded by $|\textsc{Tpl}_{1}|^{2}$. We define $\textsc{Tpl}_{2}$ as $\beta_{p+1}$ followed by $p$ iterations of $\textsc{Tpl}(\vec{0})=\alpha_{0}\ldots\alpha_{p}$ each with a signle occrrence of a cycle $\beta_{i}$ in the order $\beta_{p},\beta_{p},\ldots,\beta_{1}$. Formally, for $1\leq i\leq j\leq p+1$ we define

[TABLE]

We define $\textsc{Tpl}_{2}$ as follows:

[TABLE]

Observe that the path $\textsc{Tpl}_{2}(\vec{0})=\beta_{p+1}^{p}$, i.e., it is the same as $\textsc{Tpl}_{1}(\vec{0})^{p}=\textsc{Tpl}(\vec{0})^{p}$. Therefore, the size of $\textsc{Tpl}_{2}$ is bounded by $|\textsc{Tpl}_{1}|^{2}$. The template $\textsc{Tpl}_{2}$ is not minimal, but it has not been a requirement.

The vectors

[TABLE]

witness $\textsc{Tpl}_{2}$ being negative. Indeed, first

[TABLE]

Second, $\textsc{Tpl}_{2}(t\vec{k}_{1}+\vec{k}_{2})$ has the same multiset of edges as $\textsc{Tpl}(\vec{n})$ repeated $p(t+1)$ times. Therefore, as in the previous case, we have

[TABLE]

It follows that $\textsc{Tpl}_{2}$ is negative.

The case $\vec{m}^{T}\mathbf{B}_{\textsc{Tpl}_{1}}\vec{m}=0$. We show that Tpl is linear. Observe that $\mathbf{B}_{\textsc{Tpl}}$ is obtained from $\mathbf{B}_{\textsc{Tpl}_{1}}$ by deletion of the $(p+1)$-th row and the $(p+1)$-th column. Therefore,

[TABLE]

Therefore, we define $\vec{d}_{\textsc{Tpl}}$ for $1\leq i\leq p$ as

[TABLE]

and we define $h_{\textsc{Tpl}}=-\textsc{Gain}(\beta_{p+1})\cdot\textsc{Vals}(\beta_{p+1})$. Since $\vec{m}^{T}\mathbf{B}_{\textsc{Tpl}_{1}}\vec{m}=0$, we get

[TABLE]

Therefore, Tpl is linear.

Finally, if no template is negative, then all templates are linear. ∎

The following lemma is a vital part of the proof of Lemma 18. Recall that for a given template Tpl, we define $\textsc{Trans}_{\textsc{Tpl}}(\vec{n})\in\mathbb{N}^{m}$, where $m=|\delta|$, as the vector of multiplicities of transitions in $\textsc{Tpl}(\vec{n})$. The function $\textsc{Trans}_{\textsc{Tpl}}$ is linear. We write $\textsc{Trans}(\vec{n})$ if Tpl is clear from the context.

Lemma 29**.**

Let Tpl be a template. For every vector $\vec{n}\in\mathbb{N}^{p}$, there exists $\vec{n}_{0}\in\mathbb{N}^{p}$ such that

1. (1)

$supp(\vec{n}_{0})\leq m$, 2. (2)

$supp(\vec{n}_{0})\subseteq supp(\vec{n})$, and 3. (3)

there exists $t\in\mathbb{N}^{+}$ such that $\textsc{Trans}(\vec{n}_{0})=t\textsc{Trans}(\vec{n})$.

Proof.

We define $\textsc{Trans}^{*}\colon\mathbb{Q}^{p}\to\mathbb{Q}^{m}$ as the unique linear extension of Trans. Assume that $supp(\vec{n})>m$. Then, there are $m+1$ components $i_{1},\ldots,i_{m+1}$ of $\vec{n}$ such that $n[i_{1}],\ldots,n[i_{m+1}]$ are non-zero and $\textsc{Trans}^{*}(\mathbf{1}_{i_{1}}),\ldots,\textsc{Trans}^{*}(\mathbf{1}_{i_{m+1}})$ are linearly dependent. It follows that $\{i_{1},\ldots,i_{m+1}\}$ can be partitioned into $I_{1},I_{2}$ and there exist non-zero vectors $\vec{y}_{1},\vec{y}_{2}\in\mathbb{Q}^{p}$ with the support included in $I_{1}$ and $I_{2}$ respectively. such that $\textsc{Trans}^{*}(\vec{y}_{1})=\textsc{Trans}^{*}(\vec{y}_{2})$. Consider the maximal $c\in\mathbb{Q}^{+}$ such that all components of $\vec{x}=\vec{n}-c\vec{y}_{1}+c\vec{y}_{2}$ are non-negative, i.e., $\vec{x}\in(\mathbb{Q}^{\geq 0})^{p}$. Observe that $\textsc{Trans}^{*}(\vec{x})=\textsc{Trans}^{*}(\vec{n})$, $supp(\vec{x})\subseteq supp(\vec{n})$ and at least one component of $\vec{n}$ becomes [math] in $\vec{x}$.

We iterate this process until we get a vector $\vec{x}_{0}\in(\mathbb{Q}^{\geq 0})^{p}$ such that

1. (1)

$supp(\vec{x}_{0})\leq m$, 2. (2)

$supp(\vec{x}_{0})\subseteq supp(\vec{n})$, and 3. (3)

$\textsc{Trans}^{*}(\vec{x}_{0})=\textsc{Trans}^{*}(\vec{n})$.

Finally, let $t\in\mathbb{N}$ be such that $t\vec{x}_{0}\in\mathbb{N}^{p}$. Observe that $\vec{n}_{0}=t\vec{x}_{0}$ satisfies the statement. ∎

See 18

Proof.

We show the lemma by induction on $|supp(\vec{n})|$. Clearly, if $|supp(\vec{n})|\leq m$ the statement holds.

Consider $\vec{n}\in\mathbb{N}^{p}$ and assume that for all $\vec{n}^{\prime}\in\mathbb{N}^{p}$ with $|supp(\vec{n}^{\prime})|<|supp(\vec{n})|$ the lemma holds. Let $\vec{n}_{0}$ be the vector from Lemma 29. Consider the maximal $r\in\mathbb{Q}^{+}$ such that $\vec{n}-r\vec{n}_{0}$ has all the components non-negative. Let $r=\frac{p}{q}$ and consider $\vec{k}=q\vec{n}-p\vec{n}_{0}$. Observe that $\vec{k}\in\mathbb{N}^{p}$ and $|supp(\vec{k})|<|supp(\vec{n})|$ and hence there exist $s_{1},\ldots,s_{\ell}\in\mathbb{Q}^{+}$ and $\vec{y}_{1},\ldots,\vec{y}_{\ell}\in\mathbb{N}^{p}$ such that for all $1\leq i\leq\ell$

1. (1)

$supp(\vec{y}_{i})\leq m$ (the number of transitions of $|\mathcal{A}|$), 2. (2)

there exist $t\in\mathbb{N}^{+}$ such that $\textsc{Trans}(\vec{y}_{i})=t\cdot\textsc{Trans}(\vec{k})$, and 3. (3)

$\vec{k}=\sum_{j=1}^{\ell}s_{j}\vec{y}_{j}$.

Recall that there is $t_{0}\in\mathbb{N}^{+}$ such that $\textsc{Trans}(\vec{n}_{0})=t_{0}\textsc{Trans}(\vec{n})$. It follows that

[TABLE]

Therefore,

[TABLE]

and

[TABLE]

satisfy the statement of this lemma. ∎

See 19

Proof.

Assume that a template $\textsc{Tpl}_{1}$ is positive (resp., negative). First, we show that positivity (resp., negativity) of $\textsc{Tpl}_{1}$ is witnessed by vectors $\vec{k}_{1},\vec{k}_{2}$ with at most $m$ non-zero components.

Let $\vec{n}_{1},\vec{n}_{2}\in\mathbb{N}^{p}$ be the vectors witnessing positivity (resp., negativity). Let $r_{1},\ldots,r_{\ell}\in\mathbb{Q}^{+}$ and $\vec{z}_{1},\ldots,\vec{z}_{\ell}$ be coefficients and vectors for $\vec{n}_{1}$ satisfying Lemma 18. Then, either for some $i$ we have $\vec{z}_{i}\mathbf{B}_{\textsc{Tpl}}\vec{z}_{i}\neq 0$, and we define $\vec{p}_{1}$ as $\vec{z}_{1}^{i}$ or for some pair $i\neq j$

[TABLE]

and we define $\vec{p}_{1}=a(r_{i}\vec{z}_{i}+r_{j}\vec{z}_{j})$, where $a$ is a natural number such that $ar_{i},ar_{j}\in\mathbb{N}$. Note that one of these conditions holds; if they both fail, then due to $\vec{n}_{1}=\sum_{i=1}^{\ell}r_{i}\vec{z}_{i}$, we have $\vec{n}_{1}\mathbf{B}_{\textsc{Tpl}}\vec{n}_{1}=0$ contrary to the assumptions.

Let $\vec{p}_{2}$ be a vector with $supp(\vec{m}_{2})\leq|\delta|$ and $\textsc{Trans}(\vec{p}_{2})=t\textsc{Trans}(\vec{n}_{2})$ (which exists by Lemma 18). Finally, we define $\vec{k}_{1}=a\vec{p}_{1}$ and $\vec{k}_{1}=b\vec{p}_{2}$ for $a,b\in\mathbb{N}^{+}$ such that for some $t\in\mathbb{N}$ we have

[TABLE]

Observe that $\vec{k}_{1},\vec{k}_{2}$ also witness template $\textsc{Tpl}_{1}$ being positive or negative, but $|supp(\vec{k}_{1})|,|supp(\vec{k}_{2})|\leq m$.

We remove from $\textsc{Tpl}_{1}$ cycles corresponding to coefficient [math] in both $\vec{k}_{1}$ and $\vec{k}_{2}$. We get a template with polynomially many cycles. If all connecting paths are still bounded by $|Q|$ we terminate with $\textsc{Tpl}_{1}$, of polynomial size. However, as we remove some cycles, some connecting path are concatenated and in the result we get connecting paths longer than $|Q|$. For such connecting path, we extract simple cycles and group them (as in Lemma 13). We get another minimal template $\textsc{Tpl}_{2}$ shorter than $\textsc{Tpl}_{1}$, which is positive or negative. By iterating this process, we get a polynomial-size template $\textsc{Tpl}^{\neq}$, which is positive or negative. Then, by Lemma 17 that there exists a negative template of polynomial size. ∎

See 20

Proof.

Recall the construction of $\textsc{Tpl}_{1}$ from the proof of Lemma 17. We repeat this construction and define a symmetric matrix $\mathbf{A}\in\mathbb{Z}^{(p+1)\times(p+1)}$ such that for all $\vec{n}\in\mathbb{N}^{p}$ we have

[TABLE]

where $\vec{n}_{1}=(n[1],n[2],\ldots,n[p],1)$. We define $\beta_{p+1}=\alpha_{0}\alpha_{1}\ldots\alpha_{p}$ and the $\mathbf{A}$ is defined for all $1\leq i,j\leq p+1$ as

[TABLE]

We have assumed that $\mathcal{A}$ does not have a regular run of the value $-\infty$ and hence for all $\vec{m}\in\mathbb{N}^{p+1}$ we have $\vec{m}^{T}\mathbf{A}\vec{m}\geq 0$. We eliminate variables using the standard quadratic formula. We start with $m[1]$ and observe that

[TABLE]

where $A_{1}=\mathbf{A}[1,1]$, $B_{1}=2\sum_{i=2}^{p+1}\mathbf{A}[1,i]$, and $C_{1}=\vec{n}_{0}^{T}\mathbf{A}\vec{n}_{0}$ where $\vec{m}_{0}=(0,m[2],m[3],\ldots,m[p+1])$.

We compute $\Delta=(B_{1})^{2}-4A_{1}C_{1}$ and assume that $\Delta\geq 0$. Observe that there are four cases:

• •

The case: $A_{1}=B_{1}=0$. We observe that this is possible only if for all $i$ we have $\mathbf{A}[1,i]=\mathbf{A}[i,1]=0$.

Suppose that there is $i$ such that $\mathbf{A}[1,i]\neq 0$. Then, since $B_{1}=0$ there is $j$ such that $\mathbf{A}[1,j]\leq-1$. Consider $\vec{m}_{0}\in\mathbb{N}^{p+1}$ such that $m_{0}[1]=\mathbf{A}[1,j]^{2}$, $m_{0}[j]=1$ and all the other components are [math]. Then, $\vec{m}_{0}^{T}\mathbf{A}\vec{m}_{0}<0$, which contradicts the assumptions.

• •

The case: $A_{1}=0$ and $B_{1}\neq 0$. In this case, we argue that $m[1]=0$. Indeed, we have $C_{1}\geq 0$. Now, if $B_{1}<0$, then for $\vec{m}_{t}=(t,m[2],\ldots,m[p+1])$ and $t\in\mathbb{N}^{+}$ big enough, we get $\vec{m}_{t}^{T}\mathbf{A}\vec{m}_{t}<0$ contrary to the assumptions. Therefore, $B_{1}>0$. It follows that $B_{1}m[1]+C_{1}=0$ if and only if $m[1]=0$ and $C_{1}=0$.

• •

The case $A_{1}\neq 0$ and $\Delta>0$. Then, we argue that $m[1]=0$. Indeed, if $\vec{x}\in(\mathbb{R}^{\geq 0})^{p+1}$ is such that $x[1]>0$, then for some small $\epsilon\in(-\frac{x[1]}{2},\frac{x[1]}{2})$ and the vector $\vec{x}_{1}=(m[1]+\epsilon,m[2],\ldots,m[p+1])$ we have $\vec{x}_{1}^{T}\mathbf{A}\vec{x}_{1}<0$. It follows that there exists $\vec{y}\in(\mathbb{Q}^{\geq 0})^{p+1}$ close to $\vec{x}_{1}$ such that $\vec{y}^{T}\mathbf{A}\vec{y}<0$. Finally, for some $t\in\mathbb{N}$ we have $t\vec{y}\in\mathbb{N}^{p+1}$ and

[TABLE]

which contradicts the assumption $\vec{m}^{T}\mathbf{A}\vec{m}\geq 0$.

• •

The case: $A\neq 0$ and $\Delta=0$. Then, $m[1]=\frac{-B_{1}}{2A_{1}}$.

We have the same identities for all components of $\vec{m}$. Now, we construct linear inequalities $S_{i}$ for $\vec{n}$.

First, without loss of generality we assume that $\mathbf{A}$ does not have $\vec{0}$ rows or columns. Such rows and columns in the symmetric $\mathbf{A}$ correspond to variables, which occur only with the [math] coefficient. Second, recall that we assumed that for $1\leq i\leq p$ we have $m[i]=n[i]$ and $m[p+1]=1$. We substitute $m[p+1]$ with $1$ in all the equations on $\vec{n}$. Third, for every subset $P\subseteq\{1,\ldots,p\}$, we define $S_{P}$ such that $P=\{i\colon n[i]=0\}$.

Consider $P\subseteq\{1,\ldots,p\}$. We define $S_{P}$ as

[TABLE]

We assume that $i,j\in\{1,\ldots,p\}$ which is omitted for readability.

First, note that for every solution $\vec{n}\in\mathbb{N}$ to $S_{P}$ we have $\vec{n}_{1}=(n[1],n[2],\ldots,n[p],1)$ satisfies $\vec{n}_{1}^{T}\mathbf{A}\vec{n}_{1}=0$. We can remove all rows and columns with indexes from $P$ as their contribution to $\vec{n}_{1}^{T}\mathbf{A}\vec{n}_{1}$ is [math]. Let $\mathbf{A}^{\prime}$ be the matrix and $\vec{k}$ be the vector resulting from removal of components from $P$. Then, we observe that $\mathbf{A}^{\prime}\vec{k}$ is the $\vec{0}$ vector. Indeed, for every $i$ the equation

[TABLE]

implies that the $i$-th component of $\mathbf{A}\vec{n}_{1}$ is [math]. Thus, all components of the minor $\mathbf{A}^{\prime}$ with $\vec{k}$ are [math].

Finally, we argue that for every $\vec{m}$ satisfying $\vec{m}^{T}\mathbf{A}\vec{m}=0$ with $m[p+1]=1$, the vector $\vec{n}=(m[1],\ldots,m[p])$ solves some $S_{P}$. Indeed, we consider $P=\{i\colon n[i]=0\}$ and observe that due to the above considerations for all $i\in\{1,\ldots,p\}\setminus P$ we need to have $2A_{i}n[i]={-B_{i}}$ as it is stated in $S_{P}$. ∎