Masaryk University, Czechia and https://www.muni.cz/lide/422654-michal-ajdarow Masaryk University, Czechia and https://www.fi.muni.cz/usr/kucera/[email protected]://orcid.org/0000-0002-6602-8028 \CopyrightMichal Ajdarów and Antonín Kučera \ccsdesc[100]Theory of computation Models of computation \fundingThe work is supported by the Czech Science Foundation, Grant No. 21-24711S.\EventEditorsSerge Haddad and Daniele Varacca \EventNoEds2 \EventLongTitle32nd International Conference on Concurrency Theory (CONCUR 2021) \EventShortTitleCONCUR 2021 \EventAcronymCONCUR \EventYear2021 \EventDateAugust 23–27, 2021 \EventLocationVirtual Conference \EventLogo \SeriesVolume203 \ArticleNo24

Deciding Polynomial Termination Complexity for VASS Programs

Michal Ajdarów Antonín Kučera

Abstract

We show that for every fixed degree $k\geq 3$ , the problem whether the termination/counter complexity of a given demonic VASS is $\pazocal{O}(n^{k})$ , $\Omega(n^{k})$ , and $\Theta(n^{k})$ is $\mathbf{coNP}$ -complete, $\mathbf{NP}$ -complete, and $\mathbf{DP}$ -complete, respectively. We also classify the complexity of these problems for $k\leq 2$ . This shows that the polynomial-time algorithm designed for strongly connected demonic VASS in previous works cannot be extended to the general case. Then, we prove that the same problems for VASS games are $\mathbf{PSPACE}$ -complete. Again, we classify the complexity also for $k\leq 2$ . Tractable subclasses of demonic VASS and VASS games are obtained by bounding certain structural parameters, which opens the way to applications in program analysis despite the presented lower complexity bounds.

keywords:

Termination complexity, vector addition systems

1 Introduction

Vector addition systems with states (VASS) are a generic formalism expressively equivalent to Petri nets. In program analysis, VASS are used to model programs with unbounded integer variables, parameterized systems, etc. Thus, various problems about such systems reduce to the corresponding questions about VASS. This approach’s main bottleneck is that interesting questions about VASS tend to have high computational complexity (see, e.g., [7, 14, 15]). Surprisingly, recent results (see below) have revealed computational tractability of problems related to asymptotic complexity of VASS computations, allowing to answer questions like “Does the program terminate in time polynomial in $n$ for all inputs of size $n$ ?”, or “Is the maximal value of a given variable bounded by $\pazocal{O}(n^{4})$ for all inputs of size $n$ ?”. These results are encouraging and may enhance the existing software tools for asymptotic program analysis such as SPEED [10], COSTA [1], RAML [11], Rank [2], Loopus [17, 18], AProVE [9], CoFloCo [8], C4B [6], and others. In this paper, we give a full classification of the computational complexity of deciding polynomial termination/counter complexity for demonic VASS and VASS games, and solve open problems formulated in previous works. Furthermore, we identify structural parameters making the asymptotic VASS analysis computationally hard. Since these parameters are often small in VASS program abstractions, this opens the way to applications in program analysis despite the established lower complexity bounds.

The termination complexity of a given VASS $\pazocal{A}$ is a function $\pazocal{L}:\mathbb{N}\rightarrow\mathbb{N}_{\infty}$ assigning to every $n$ the maximal length of a computation initiated in a configuration with all counters initialized to $n$ . Similarly, the counter complexity of a given counter $c$ in $\pazocal{A}$ is a function $\pazocal{C}[c]:\mathbb{N}\rightarrow\mathbb{N}_{\infty}$ such that $\pazocal{C}[c](n)$ is the maximal value of $c$ along a computation initiated in a configuration with all counters set to $n$ . So far, three types of VASS models have been investigated in previous works.

•

Demonic VASS, where the non-determinism is resolved by an adversarial environment aiming to increase the complexity.
•

VASS Games, where every control state is declared as angelic or demonic, and the non-determinism is resolved by the controller or by the environment aiming to lower and increase the complexity, respectively.
•

VASS MDPs, where the states are either non-deterministic or stochastic. The non-determinism is usually resolved in the “demonic” way.

Let us note that the “angelic” and “demonic” non-determinism are standard concepts in program analysis [5] applicable to arbitrary computational devices including VASS. The use of VASS termination/counter complexity analysis is illustrated in the next example.

Example 1.1.

Consider the program skeleton of Fig. 1 (left). Since a VASS cannot directly model the assignment j:=i and cannot test a counter for zero, the skeleton is first transformed into an equivalent program of Fig. 1 (middle), where the assignment j:=i is implemented using an auxiliary variable Aux and two while loops. Clearly, the execution of the transformed program is only longer than the execution of the original skeleton (for all inputs). For the transformed program, an over-approximating demonic VASS model is obtained by replacing conditionals with non-determinism, see Fig. 1 (right). When all counters are initialized to $n$ , the VASS terminates after $\pazocal{O}(n^{2})$ transitions. Hence, the same upper bound is valid also for the original program skeleton. Actually, the run-time complexity of the skeleton is $\Theta(n^{2})$ where $n$ is the initial value of i, so the obtained upper bound is asymptotically optimal.

⬇ input i; while(i>0) i:=i-1; j:=i; while(j>0) j:=j-1;

⬇ input i; while(i>0) i–; j:=0; Aux:=0; while(i>0) i–; j++; Aux++; while(Aux>0) i++; Aux–; while(j>0) j–;

Figure 1: A skeleton of a simple imperative program (left) and its VASS model (right).

Existing results. In [4], it is shown that the problem whether $\pazocal{L}\in\pazocal{O}(n)$ for a given demonic VASS is solvable in polynomial time, and a complete proof method based on linear ranking functions is designed. The polynomiality of termination complexity for a given demonic VASS is also decidable in polynomial time, and if $\pazocal{L}\not\in\pazocal{O}(n^{k})$ for any $k\in\mathbb{N}$ , then $\pazocal{L}\in 2^{\Omega(n)}$ [13]. The same results hold for counter complexity. In [19], a polynomial time algorithm computing the least $k\in\mathbb{N}$ such that $\pazocal{L}\in\pazocal{O}(n^{k})$ for a given demonic VASS is presented (the algorithm first checks if such a $k$ exists). It is also shown that if $\pazocal{L}\not\in\pazocal{O}(n^{k})$ , then $\pazocal{L}\in\Omega(n^{k+1})$ . Again, the same results hold also for counter complexity. The proof is actually given only for strongly connected demonic VASS, and it is conjectured that a generalization to unrestricted demonic VASS can be obtained by extending the presented construction (see the Introduction of [19]). In [12], it was shown that the problem whether the termination/counter complexity of a given demonic VASS belongs to a given level of Grzegorczyk hierarchy is solvable in polynomial time, and the same problem for VASS games is shown $\mathbf{NP}$ -complete. The $\mathbf{NP}$ upper bound follows by observing that player Angel can safely commit to a countreless¹¹1A strategy is counterless if the decision depends just on the control state of the configuration currently visited. strategy when minimizing the complexity level in the Grzegorczyk hierarchy. Intuitively, this is because Grzegorczyk classes are closed under function composition (unlike the classes $\Theta(n^{k})$ ). Furthermore, the problem whether $\pazocal{L}\in\pazocal{O}(n^{2})$ for a given VASS game is shown $\mathbf{PSPACE}$ hard, but the decidability of this problem is left open. As for VASS MDPs, the only existing result is [3], where it is shown that the linearity of termination complexity is solvable in polynomial time for VASS MDPs with a tree-like MEC decomposition.

Our contribution. For demonic VASS, we refute the conjecture of [19] and prove that for general (not necessarily strongly connected) demonic VASS, the problem whether

•

$\pazocal{L}\in\pazocal{O}(n^{k})$ is in $\mathbf{P}$ for $k=1$ , and $\mathbf{coNP}$ -complete for $k\geq 2$ ;
•

$\pazocal{L}\in\Omega(n^{k})$ is in $\mathbf{P}$ for $k\leq 2$ , and $\mathbf{NP}$ -complete for $k\geq 3$ ;
•

$\pazocal{L}\in\Theta(n^{k})$ is in $\mathbf{P}$ for $k=1$ , $\mathbf{coNP}$ -complete for $k=2$ , and $\mathbf{DP}$ -complete for $k\geq 3$ ;
•

$\pazocal{C}[c]\in\pazocal{O}(n^{k})$ is $\mathbf{coNP}$ -complete;
•

$\pazocal{C}[c]\in\Omega(n^{k})$ is in $\mathbf{P}$ for $k=1$ , and $\mathbf{NP}$ -complete for $k\geq 2$ ;
•

$\pazocal{C}[c]\in\Theta(n^{k})$ is $\mathbf{coNP}$ -complete for $k=1$ , and $\mathbf{DP}$ -complete for $k\geq 2$ .

Since the demonic VASS constructed in our proofs are relatively complicated, we write them in a simple imperative language with a precisely defined VASS semantics. This allows to present the overall proof idea clearly and justify technical correctness by following the control flow of the VASS program, examining possible side effects of the underlying “gadgets”, and verifying that the Demon does not gain anything by deviating from the ideal execution scenario.

When proving the upper bounds, we show that every path in the DAG of strongly connected components can be associated with the (unique) vector describing the maximal simultaneous increase of the counters. Here, the counters pumpable to exponential (or even larger) values require special treatment. We show that this vector is computable in polynomial time. Hence, the complexity of a given counter $c$ is $\Omega(n^{k})$ iff there is a path in the DAG such that the associated maximal increase of $c$ is $\Omega(n^{k})$ . Thus, we obtain the $\mathbf{NP}$ upper bound, and the other upper bounds follow similarly. The crucial parameter characterizing hard-to-analyze instances is the number of different paths from a root to a leaf in the DAG decomposition, and tractable subclasses of demonic VASS are obtained by bounding this parameter. We refer to Section 3 for more details.

Then, we turn our attention to VASS games, where the problem of polynomial termination/counter complexity analysis requires completely new ideas. In [12], it was observed that the information about the “asymptotic counter increase performed so far” must be taken into account by player Angel when minimizing the complexity level in the polynomial hierarchy, and counterless strategies are therefore insufficient. However, it is not clear what information is needed to make optimal decisions, and whether this information is finitely representable. We show that player Angel can safely commit to a so-called locking strategy. A strategy for player Angel is locking if whenever a new angelic state $p$ is visited, one of its outgoing transition is chosen and “locked” so that when $p$ is revisited, the same locked transition is used. The locked transition choice may depend on the computational history and the transitions locked in previously visited angelic states. Then, we define a locking decomposition of a given VASS that plays a role similar to the DAG decomposition for demonic VASS. Using the locking decomposition, the existence of a suitable locking strategy for player Angel is decided by an alternating polynomial time algorithm (and hence in polynomial space). Thus, we obtain the following: For every VASS game and a counter $c$ , we have that $\pazocal{L},\pazocal{C}[c]$ are either in $\pazocal{O}(n^{k})$ or in $\Omega(n^{k+1})$ . Furthermore, the problem whether

•

$\pazocal{L}\in\pazocal{O}(n^{k})$ is $\mathbf{NP}$ -complete for $k{=}1$ and $\mathbf{PSPACE}$ -complete for $k{\geq}2$ ;
•

$\pazocal{L}\in\Omega(n^{k})$ is in $\mathbf{P}$ for $k{=}1$ , $\mathbf{coNP}$ -complete for $k{=}2$ , and $\mathbf{PSPACE}$ -complete for $k{\geq}3$ ;
•

$\pazocal{L}\in\Theta(n^{k})$ is $\mathbf{NP}$ -complete for $k{=}1$ and $\mathbf{PSPACE}$ -complete for $k{\geq}2$ ;
•

$\pazocal{C}[c]\in\pazocal{O}(n^{k})$ is $\mathbf{PSPACE}$ -complete;
•

$\pazocal{C}[c]\in\Omega(n^{k})$ is in $\mathbf{P}$ for $k{=}1$ , and $\mathbf{PSPACE}$ -complete for $k{\geq}2$ ;
•

$\pazocal{C}[c]\in\Theta(n^{k})$ is $\mathbf{PSPACE}$ -complete.

Similarly to demonic VASS, tractable subclasses of VASS games are obtained by bounding the number of different paths in the locking decomposition.

The VASS model constructed in Example 1.1 is purely demonic. The use of VASS games in program analysis/synthesis is illustrated in the next example.

Example 1.2.

Consider the program of Fig. 2. The condition at line 3 is resolved by the environment in a demonic way. The two branches of if-then-else execute a code modifying the variables j and k. After that, the controller can choose one of the two while-loops at lines 8, 9 with the aim of keeping the value of z small. The question is how the size of z grows with the size of input if the controller makes optimal decisions. A closer look reveals that when the variable i is assigned $n$ at line 1, then

•

the values of j and k are $\Theta(n)$ and $\Theta(n^{2})$ when the condition is evaluated to true;
•

the values of j and k are $\Theta(n^{2})$ and $\Theta(n)$ when the condition is evaluated to false.

Hence, the controller can keep z in $\Theta(n)$ if an optimal decision is taken. Constructing a VASS game model for the program of Fig. 2 is straightforward (the required gadgets are given in Fig. 3). Using the results of this paper, the above analysis can be performed fully automatically.

⬇

1input i;

2j:=0; k:=0; z:=0;

3if condition // demonic choice //

4then while (i>0) do j++; k:=k+i; i–; done

5else j:=i*i; k:=i;

6while (i>0) do j:=j+k; i–; done

7choose: // angelic choice //

8while (j>0) do j–; z++ done

9or: while (k>0) do k–; z++ done

Figure 2: A simple program with both demonic and angelic non-determinism.

2 Preliminaries

The sets of integers and non-negative integers are denoted by $\mathbb{Z}$ and $\mathbb{N}$ , respectively, and we use $\mathbb{N}_{\infty}$ to denote $\mathbb{N}\cup\{\infty\}$ . The vectors of $\mathbb{Z}^{d}$ where $d\geq 1$ are denoted by $\mathbf{v},\mathbf{u},\ldots$ , and the vector $(n,\ldots,n)$ is denoted by $\vec{n}$ .

Definition 2.1 (VASS).

Let $d\geq 1$ . A $d$ -dimensional vector addition system with states (VASS) is a pair $\pazocal{A}=\left(Q,\textit{Tran}\right)$ , where $Q\neq\emptyset$ is a finite set of states and $\textit{Tran}\subseteq Q\times\mathbb{Z}^{d}\times Q$ is a finite set of transitions such that for every $q\in Q$ there exist $p\in Q$ and $\mathbf{u}\in\mathbb{Z}^{d}$ such that $(q,\mathbf{u},p)\in\textit{Tran}$ .

The set $Q$ is split into two disjoint subsets $Q_{A}$ and $Q_{D}$ of angelic and demonic states controlled by the players Angel and Demon, respectively. A configuration of $\pazocal{A}$ is a pair $p\mathbf{v}\in Q\times\mathbb{N}^{d}$ , where $\mathbf{v}$ is the vector of counter values. We often refer to counters by their symbolic names. For example, when we say that $\pazocal{A}$ has three counters $x,y,z$ and the value of $x$ in a configuration $p\mathbf{v}$ is $8$ , we mean that $d=3$ and $\mathbf{v}_{i}=8$ where $i$ is the index associated to $x$ . When the mapping between a counter name and its index is essential, we use $c_{i}$ to denote the counter with index $i$ .

A finite path in $\pazocal{A}$ of length $m$ is a finite sequence $\varrho=p_{1},\mathbf{u}_{1},p_{2},\mathbf{u}_{2},\ldots,p_{m}$ such that $(p_{i},\mathbf{u}_{i},p_{i+1})\in Tran$ for all $1\leq i<m$ . We use $\Delta(\varrho)$ to denote the effect of $\varrho$ , defined as $\sum_{i=1}^{m}\mathbf{u}_{i}$ . An infinite path in $\pazocal{A}$ is an infinite sequence $\alpha=p_{1},\mathbf{u}_{1},p_{2},\mathbf{u}_{2},\ldots$ such that every finite prefix $p_{1},\mathbf{u}_{1},\ldots,p_{m}$ of $\alpha$ is a finite path in $\pazocal{A}$ .

A computation of $\pazocal{A}$ is a sequence of configurations $\alpha=p_{1}\mathbf{v}_{1},p_{2}\mathbf{v}_{2},\ldots$ of length $m\in\mathbb{N}_{\infty}$ such that for every $1\leq i<m$ there is a transition $(p_{i},\mathbf{u}_{i},p_{i+1})$ satisfying $\mathbf{v}_{i+1}=\mathbf{v}_{i}+\mathbf{u}_{i}$ . Note that every computation determines its associated path in the natural way.

VASS Termination Complexity. A strategy for Angel (or Demon) in $\pazocal{A}$ is a function $\eta$ assigning to every finite computation $p_{1}\mathbf{v}_{1},\ldots,p_{m}\mathbf{v}_{m}$ where $p_{m}\in Q_{A}$ (or $p_{m}\in Q_{D}$ ) a transition $(p_{m},\mathbf{u},q)$ . Every pair of strategies $(\sigma,\pi)$ for Angel/Demon and every initial configuration $p\mathbf{v}$ determine the unique maximal computation $\mathit{Comp}^{\sigma,\pi}(p\mathbf{v})$ initiated in $p\mathbf{v}$ . The maximality means that the computation cannot be prolonged without making some counter negative. For a given counter $c$ , we use $\textit{max}[c](\mathit{Comp}^{\sigma,\pi}(p\mathbf{v}))$ to denote the supremum of the $c$ ’s values in all configurations visited along $\mathit{Comp}^{\sigma,\pi}(p\mathbf{v})$ . Furthermore, we use $\textit{len}(\mathit{Comp}^{\sigma,\pi}(p\mathbf{v}))$ to denote the length of $\mathit{Comp}^{\sigma,\pi}(p\mathbf{v})$ . Note that $\textit{max}[c]$ and len can be infinite for certain computations.

For every initial configuration $p\mathbf{v}$ , consider a game where the players Angel and Demon aim at minimizing and maximizing the $\textit{max}[c]$ or len objective, respectively. By applying standard game-theoretic arguments (see Appendix A), we obtain

	$\displaystyle\sup_{\pi}\ \operatornamewithlimits{inf\vphantom{p}}_{\sigma}\ \textit{len}(\mathit{Comp}^{\sigma,\pi}(p\mathbf{v}))$	$\displaystyle=$	$\displaystyle\operatornamewithlimits{inf\vphantom{p}}_{\sigma}\ \sup_{\pi}\ \textit{len}(\mathit{Comp}^{\sigma,\pi}(p\mathbf{v}))$		(1)
	$\displaystyle\sup_{\pi}\ \operatornamewithlimits{inf\vphantom{p}}_{\sigma}\ \textit{max}[c](\mathit{Comp}^{\sigma,\pi}(p\mathbf{v}))$	$\displaystyle=$	$\displaystyle\operatornamewithlimits{inf\vphantom{p}}_{\sigma}\ \sup_{\pi}\ \textit{max}[c](\mathit{Comp}^{\sigma,\pi}(p\mathbf{v}))$		(2)

where $\sigma$ and $\pi$ range over all strategies for Angel and Demon, respectively. Hence, there exists a unique termination value of $p\mathbf{v}$ , denoted by $\mathit{Tval}(p\mathbf{v})$ , defined by (1). Similarly, for every counter $c$ there exists a unique maximal counter value, denoted by $\mathit{Cval}[c](p\mathbf{v})$ , defined by (2). Furthermore, both players have optimal positional strategies $\sigma^{*}$ and $\pi^{*}$ achieving the outcome specified by the equilibrium value or better in every configuration $p\mathbf{v}$ against every strategy of the opponent (here, a positional strategy is a strategy depending only on the currently visited configuration). We refer to Appendix A for details.

The termination complexity and $c$ -counter complexity of $\pazocal{A}$ are functions $\pazocal{L},\pazocal{C}[c]:\mathbb{N}\rightarrow\mathbb{N}_{\infty}$ where $\pazocal{L}(n)=\max\{\mathit{Tval}(p\vec{n})\mid p\in Q\}$ and $\pazocal{C}[c](n)=\max\{\mathit{Cval}[c](p\vec{n})\mid p\in Q\}$ . When the underlying VASS $\pazocal{A}$ is not clear, we write $\pazocal{L}{A}$ and $\pazocal{C}{A}[c]$ instead of $\pazocal{L}$ and $\pazocal{C}[c]$ .

Observe that the asymptotic analysis of termination complexity for a given VASS $\pazocal{A}$ is trivially reducible to the asymptotic analysis of counter complexity in a VASS $\pazocal{B}$ obtained from $\pazocal{A}$ by adding a fresh “step counter” sc incremented by every transition of $\pazocal{B}$ . Clearly, $\pazocal{L}{A}\in\Theta(\pazocal{C}{B}[\textit{sc}])$ . Therefore, the lower complexity bounds for the considered problems of asymptotic analysis are proven for $\pazocal{L}$ , while the upper bounds are proven for $\pazocal{C}[c]$ .

3 Demonic VASS

In this section, we classify the computational complexity of polynomial asymptotic analysis for demonic VASS. The following theorem holds regardless whether the counter update vectors are encoded in unary or binary (the lower bounds hold for unary encoding, the upper bounds hold for binary encoding).

Theorem 3.1.

Let $k\geq 1$ . For every demonic VASS $\pazocal{A}$ and counter $c$ we have that $\pazocal{L}$ ( $\pazocal{C}[c]$ ) is either in $\pazocal{O}(n^{k})$ or in $\Omega(n^{k+1})$ . Furthermore, the problem whether

•

$\pazocal{L}\in\pazocal{O}(n^{k})$ is in $\mathbf{P}$ for $k=1$ , and $\mathbf{coNP}$ -complete for $k\geq 2$ ;
•

$\pazocal{L}\in\Omega(n^{k})$ is in $\mathbf{P}$ for $k\leq 2$ , and $\mathbf{NP}$ -complete for $k\geq 3$ ;
•

$\pazocal{L}\in\Theta(n^{k})$ is in $\mathbf{P}$ for $k=1$ , $\mathbf{coNP}$ -complete for $k=2$ , and $\mathbf{DP}$ -complete for $k\geq 3$ ;
•

$\pazocal{C}[c]\in\pazocal{O}(n^{k})$ is $\mathbf{coNP}$ -complete;
•

$\pazocal{C}[c]\in\Omega(n^{k})$ is in $\mathbf{P}$ for $k=1$ , and $\mathbf{NP}$ -complete for $k\geq 2$ ;
•

$\pazocal{C}[c]\in\Theta(n^{k})$ is $\mathbf{coNP}$ -complete for $k=1$ , and $\mathbf{DP}$ -complete for $k\geq 2$ .

The next theorem identifies the crucial parameter influencing the complexity of polynomial asymptotic analysis for demonic VASS. Let $\pazocal{D}(\pazocal{A})$ be the standard DAG of strongly connected components of $\pazocal{A}$ . For every leaf (bottom SCC) $\eta$ of $\pazocal{D}(\pazocal{A})$ , let $\textit{Deg}(\eta)$ be the total number of all paths from a root of $\pazocal{D}(\pazocal{A})$ to $\eta$ .

Theorem 3.2.

Let $\Lambda$ be a class of demonic VASS such that for every $\pazocal{A}\in\Lambda$ and every leaf $\eta$ of $\pazocal{D}(\pazocal{A})$ we have that $\textit{Deg}(\eta)$ is bounded by a fixed constant depending only on $\Lambda$ .

Then, the problems whether $\pazocal{L}{A}\in\pazocal{O}(n^{k})$ , $\pazocal{L}{A}\in\Omega(n^{k})$ , $\pazocal{L}{A}\in\Theta(n^{k})$ for given $\pazocal{A}\in\Lambda$ and $k\in\mathbb{N}$ , are solvable in polynomial time (where the $k$ is written in binary). The same results hold also for $\pazocal{C}[c]$ (for a given counter $c$ of $\pazocal{A}$ ).

The degree of the polynomial bounding the running time of the decision algorithm for the three problems of Theorem 3.2 increases with the increasing size of the constant bounding $\textit{Deg}(\eta)$ . From the point of view of program analysis, Theorem 3.2 has a clear intuitive meaning. If $\pazocal{A}$ is an abstraction of a program $\pazocal{P}$ , then the instructions in $\pazocal{P}$ increasing the complexity of the asymptotic analysis of $\pazocal{A}$ are branching instructions such as if-then-else that are not embedded within loops. If $\pazocal{P}$ executes many such constructs in a sequence, a termination point can be reached in many ways (“zigzags” in the $\pazocal{P}$ ’s control-flow graph). This increases $\textit{Deg}(\eta)$ , where $\eta$ is a leaf of $\pazocal{D}(\pazocal{A})$ containing the control state modeling the termination point of $\pazocal{P}$ .

3.1 Lower bounds

d_{2}\texttt{\,+=\,}d_{1}*e_{1};\ \ d_{3}\texttt{\,+=\,}d_{2}*e_{2};\ \cdots\ ;\ \ d_{k}\texttt{\,+=\,}d_{k-1}*e_{k-1};

2 foreach $i=1,\ldots,v$ do

3 choose:

x_{i}\texttt{\,+=\,}d_{k}

\bar{x}_{i}\texttt{\,+=\,}d_{k};

5 end foreach

s_{0}\texttt{\,+=\,}d_{k};

7 foreach $i=1,\ldots,m$ do

8 choose:

s_{i}\texttt{\,+=\,}\min(\ell^{i}_{1},s_{i-1})

s_{i}\texttt{\,+=\,}\min(\ell^{i}_{2},s_{i-1})

s_{i}\texttt{\,+=\,}\min(\ell^{i}_{3},s_{i-1});

10 end foreach

f\texttt{\,+=\,}s_{m}*n

VASS Program 1

\pazocal{A}_{\varphi}

Figure 3: The gadgets of

\pazocal{A}_{\varphi}

Lemma 3.3.

Let $k\geq 2$ . For every propositional formula $\varphi$ in 3-CNF there exists a demonic VASS $\pazocal{A}_{\varphi}$ , with counter $c$ , constructible in time polynomial in $|\varphi|$ such that

•

if $\varphi$ is satisfiable, then $\pazocal{L}_{\pazocal{A}_{\varphi}}\in\Theta(n^{k+1})$ and $\pazocal{C}_{\pazocal{A}_{\varphi}}[c]\in\Theta(n^{k})$ ;
•

if $\varphi$ is not satisfiable, then $\pazocal{L}_{\pazocal{A}_{\varphi}}\in\Theta(n^{k})$ and $\pazocal{C}_{\pazocal{A}_{\varphi}}[c]\in\Theta(n)$ .

Proof 3.4.

Let $\varphi\ \equiv\ C_{1}\wedge\cdots\wedge C_{m}$ be a propositional formula where every $C_{i}\equiv\ell_{1}^{i}\vee\ell_{2}^{i}\vee\ell_{3}^{i}$ is a clause with three literals over propositional variables $X_{1},\ldots,X_{v}$ (a literal is a propositional variable or its negation). We construct a VASS $\pazocal{A}_{\varphi}$ with the counters

•

$x_{1},\cdots,x_{v}$ , $\bar{x}_{1},\cdots,\bar{x}_{v}$ used to encode an assignment of truth values to $X_{1},\ldots,X_{v}$ . In the following, we identify literals $\ell_{j}^{i}$ of $\varphi$ with their corresponding counters (i.e., if $\ell_{j}^{i}\equiv X_{u}$ , the corresponding counter is $x_{u}$ ; and if $\ell_{j}^{i}\equiv\neg X_{u}$ , the corresponding counter is $\bar{x}_{u}$ ).
•

$s_{0},\ldots,s_{m}=c$ used to encode the validity of clauses under the chosen assignment,
•

$f$ used to encode the (in)validity of $\varphi$ under the chosen assignment,
•

$d_{1},\ldots,d_{k}$ and $e_{1},\ldots,e_{k-1}$ used to compute $n^{k}$ ,
•

and some auxiliary counters used in gadgets.

The structure of $\pazocal{A}_{\varphi}$ is shown in VASS Program 1. The basic instructions are implemented by the gadgets of Fig. 3 (top). Counter changes associated to a given transition are indicated by the corresponding labels, where $-c$ and $+c$ mean decrementing and incrementing a given counter by one (the other counters are unchanged). Hence, the empty label represents no counter change, i.e., the associated counter update vector is $\vec{0}$ . The auxiliary counter $\alpha$ is unique for every instance of these gadgets and it is not modified anywhere else.

The constructs $\textit{ins}_{1};\,\textit{ins}_{2}$ and $\textbf{choose: }\textit{ins}_{1};\textbf{ or }\cdots\textbf{ or }\textit{ins}_{j}$ are implemented by connecting the underlying gadgets as shown in Fig. 3 (bottom). The foreach statements are just concise representations of the corresponding sequences of instructions connected by ‘;’.

Now suppose that the computation of VASS Program 1 is executed from line 1 where all counters are initialized to $n$ . One can easily verify that all gadgets implement the operations associated to their labels up to some “asymptotically irrelevant side effects”. More precisely,

•

the $z\texttt{\,+=\,}x*y$ gadget ensures that the Demon can increase the value of counter $z$ by $\textit{val}(x)+\textit{val}(y)\cdot(\textit{val}(x)+n)$ (but not more) if he plays optimally, where $\textit{val}(x)$ and $\textit{val}(y)$ are the values stored in $x$ and $y$ when initiating the gadget. Recall that the counter $\alpha$ is unique for the gadget, and its initial value is $n$ . Also note that the value of $y$ is decreased to $0$ when the Demon strives to maximally increase the value of $z$ .
•

The $x\texttt{\,+=\,}y$ gadget ensures that the Demon can add $\textit{val}(y)$ to the counter $x$ and then reset $y$ to the value $\textit{val}(y)+n$ (but not more) if he plays optimally. Again, note that $\alpha$ is a unique counter for the gadget with initial value $n$ .
•

The $s_{i}\texttt{\,+=\,}\min(\ell,s_{i-1})$ gadget allows the Demon to increase $s_{i}$ by the minimum of $\textit{val}(\ell)$ and $\textit{val}(s_{i-1})$ , and then restore $\ell$ to $\textit{val}(\ell)+n$ (but not more).

Now, the VASS Program 1 is easy to follow. We describe its execution under the assumption that the Demon plays optimally. It is easy to verify that the Demon cannot gain anything by deviating from the below described scenario where certain counters are pumped to their maximal values (in particular, the auxiliary counters are never re-used outside their gadgets, hence the Demon is not motivated to leave any positive values in them).

By executing line 1, the Demon pumps the counter $d_{k}$ to the value $\Theta(n^{k})$ . Then, the Demon determines a truth assignment for every $X_{i}$ , where $i\in\{1,\ldots,v\}$ , by pumping either the counter $x_{i}$ or the counter $\bar{x}_{i}$ to the value $\Theta(n^{k})$ . A key observation is that when the chosen assignment makes $\varphi$ true, then every clause contains a literal such that the value of its associated counter is $\Theta(n^{k})$ . Otherwise, there is a clause $C_{i}$ such that all of the three counters corresponding to $\ell_{1}^{i}$ , $\ell_{2}^{i}$ , $\ell_{3}^{i}$ have the value $n$ . The Demon continues by pumping $s_{0}$ to the value $\Theta(n^{k})$ at line 1. Then, for every $i=1,\ldots,m$ , he selects a literal $\ell_{j}^{i}$ of $C_{i}$ and pumps $s_{i}$ to the minimum of $\textit{val}(s_{i-1})$ and $\textit{val}(\ell_{j}^{i})$ . Observe that $\textit{val}(s_{i-1})$ is either $\Theta(n)$ or $\Theta(n^{k})$ , and the same holds for $\textit{val}(s_{i})$ after executing the instruction. Hence, $s_{m}$ is pumped either to $\Theta(n^{k})$ or $\Theta(n)$ , depending on whether the chosen assignment sets every clause to true or not, respectively. Note that the length of the whole computation up to line 1 is $\Theta(n^{k})$ , regardless whether the chosen assignment sets the formula $\varphi$ to true or false. If $s_{m}$ was pumped to $\Theta(n^{k})$ , then the last instruction at line 1 can pump the counter $f$ to $\Theta(n^{k+1})$ in $\Theta(n^{k+1})$ transitions. Hence, if $\varphi$ is satisfiable, the Demon can schedule a computation of length $\Theta(n^{k+1})$ and along the way pump $c=s_{m}$ to $\Theta(n^{k})$ . Otherwise, the length of the longest computation is $\Theta(n^{k})$ and counter $c=s_{m}$ is bounded by $\Theta(n)$ . Also observe that if the Demon starts executing $\pazocal{A}_{\varphi}$ in some other control state (i.e., not in the first instruction of line 1), the maximal length of a computation as well as the maximal value of $c$ is only smaller.

Recall that the class $\mathbf{DP}$ consists of problems that are intersections of one problem in $\mathbf{NP}$ and another problem in $\mathbf{coNP}$ . The class $\mathbf{DP}$ is expected to be somewhat larger than $\mathbf{NP}\cup\mathbf{coNP}$ , and it is contained in the $\mathbf{P}^{\mathbf{NP}}$ level of the polynomial hierarchy. The standard $\mathbf{DP}$ -complete problem is Sat-Unsat, where an instance is a pair $\varphi,\psi$ of propositional formulae and the question is whether $\varphi$ is satisfiable and $\psi$ is unsatisfiable [16]. Hence, the $\mathbf{DP}$ lower bounds of Theorem 3.1 follow directly from the next lemmas (a proof can be found in Appendix B).

Lemma 3.5.

Let $k\geq 3$ . For every pair $\varphi,\psi$ of propositional formulae in 3-CNF there exists a demonic VASS $\pazocal{A}_{\varphi,\psi}$ such that $\pazocal{L}_{\pazocal{A}_{\varphi,\psi}}\in\Theta(n^{k})$ iff $\varphi$ is satisfiable and $\psi$ is unsatisfiable.

Lemma 3.6.

Let $k\geq 2$ . For every pair $\varphi,\psi$ of propositional formulae in 3-CNF there exists a demonic VASS $\pazocal{A}_{\varphi,\psi}$ along with a counter $c$ such that $\pazocal{C}_{\pazocal{A}_{\varphi,\psi}}[c]\in\Theta(n^{k})$ iff $\varphi$ is satisfiable and $\psi$ is unsatisfiable.

3.2 Upper bounds

The upper complexity bounds of Theorem 3.1 are proven for $\pazocal{C}[c]$ . For the sake of clarity, we first sketch the main idea and then continue with developing a formal proof.

Intuition. For a given demonic VASS $\pazocal{A}$ , we compute its SCC decomposition and proceed by analyzing the individual SCCs in the way indicated in Fig. 4. We start in a top SCC with all counters initialized to $n$ . Here, we can directly apply the results of [19, 13] and decide in polynomial time whether $\pazocal{C}[c]\in\Theta(n^{k})$ for some $k\in\mathbb{N}$ or $\pazocal{C}[c]\in 2^{\Omega(n)}$ (in the first case, we can also determine the $k$ ). We perform this analysis for every counter $c$ and thus obtain the vector describing the maximal asymptotic growth of the counters (such as $(n^{2},n,2^{\Omega(n)})$ in Fig. 4). Observe that

•

although the asymptotic growth of $\pazocal{C}[c]$ has been analyzed for each counter independently, all counters can be pumped to their associated asymptotic values simultaneously. Intuitively, this is achieved by considering the “pumping computations” for the smaller vector $(\lfloor n/d\rfloor,\ldots,\lfloor n/d\rfloor)$ of initial counter values ( $d$ is the dimension of $\pazocal{A}$ ), and then simply “concatenating” these computations in a configuration with all counters initialized to $n$ ;
•

if the asymptotic growth of $\pazocal{C}[c]$ is $\Theta(n)$ , the computation simultaneously pumping the counters to their asymptotic values may actually decrease the value of $c$ (the computation can be arranged so that the resulting value of $c$ stays above $\lfloor n/d\rfloor$ for all sufficiently large $n$ ). For example, the top SCC of Fig. 4 achieves the simultaneous asymptotic growth of all counters from $(n,n,n)$ to $(n^{2},n,2^{\Omega(n)})$ , but this does not imply the counters can be simultaneously increased above the original value $n$ (nevertheless, the simultaneous increase in the first and the third counter above $n$ is certainly possible for all sufficiently large $n$ ).

A natural idea how to proceed with next SCCs is to perform a similar analysis for larger vectors of initial counter values. Since we are interested just in the asymptotic growth of the counters, we can safely set the initial value of a counter previously pumped to $\Theta(n^{k})$ to precisely $n^{k}$ . However, it is not immediately clear how to treat the counters previously pumped to $2^{\Omega(n)}$ . We show that the length of a computation “pumping” the counters to their new asymptotic values in the considered SCC $\pazocal{C}$ is at most exponential in $n$ . Consequently, the “pumping computation” in $\pazocal{C}$ can be constructed so that the resulting value of the “large” counters stays above one half of their original value. This means the value of “large” counters is still in $2^{\Omega(n)}$ after completing the computation in $\pazocal{C}$ . Furthermore, the large counters can be treated as if their initial value was infinite when analyzing $\pazocal{C}$ . This “infinite” initial value is implemented simply by modifying every counter update vector $\mathbf{u}$ in $\pazocal{C}$ so that $\mathbf{u}[j]=0$ for every “large” counter $c_{j}$ . This adjustment in the structure of $\pazocal{C}$ is denoted by putting “ $\infty$ ” into the corresponding component of the initial counter value vector (see Fig. 4). This procedure is continued until processing all SCCs. Note that the same SCC may be processed multiple times for different vectors of initial counter values corresponding to different paths from a top SCC. In Fig. 4, the bottom SCC is processed for the initial vectors $(n^{5},n,\infty)$ and $(n^{2},\infty,\infty)$ corresponding to the two paths from the top SCC. The number of such initial vectors can be exponential in the size of $\pazocal{A}$ , as witnessed by the VASS constructed in the proof of Lemma 3.3.

Figure 4: Analyzing

\pazocal{C}[c]

in a demonic VASS by SCC decomposition.

Now we give a formal proof. Let $\pazocal{A}$ be a demonic VASS with $d$ counters. For every counter $c$ and every $\mathbf{v}\in\mathbb{N}^{d}$ , we define the function $\pazocal{C}[c,\mathbf{v}]:\mathbb{N}\rightarrow\mathbb{N}_{\infty}$ where $\pazocal{C}[c,\mathbf{v}](n)$ is the maximum of all $\mathit{Cval}[c](p\mathbf{u})$ where $p\in Q$ and $\mathbf{u}=(n^{\mathbf{v}(1)},\ldots,n^{\mathbf{v}(d)})$ .

Proposition 3.7.

Let $\pazocal{A}$ be a strongly connected demonic VASS with $d$ counters, and let $\mathbf{v}\in\mathbb{N}^{d}$ such that $\mathbf{v}(i)\leq 2^{j\cdot d}$ for every $i\leq d$ , where $j<|Q|$ . For every counter $c$ , we have that either $\pazocal{C}[c,\mathbf{v}]\in\Theta(n^{k})$ for some $1\leq k\leq 2^{(j{+}1)\cdot d}$ , or $\pazocal{C}[c,\mathbf{v}]\in\Omega(2^{n})$ . It is decidable in polynomial time which of the two possibilities holds. In the first case, the value of $k$ is computable in polynomial time.

In [19], a special variant of Proposition 3.7 covering the subcase when $\mathbf{v}=\vec{1}$ is proven. In the introduction part of [19], it is mentioned that a generalization of this result (equivalent to Proposition 3.7) can be obtained by modifying the techniques presented in [19]. Although no explicit proof is given, the modification appears feasible. We give a simple explicit proof of Proposition 3.7, using the algorithm of [19] for the $\mathbf{v}=\vec{1}$ subcase as a “black-box procedure”. We refer to Appendix B for details.

Now we extend the function $\pazocal{C}[c,\mathbf{v}]$ so that $\mathbf{v}\in\mathbb{N}_{\infty}^{d}$ . Here, the $\infty$ components of $\mathbf{v}$ correspond to counters that have already been pumped to “very large” values and do not constrain the computations in $\pazocal{A}$ . As we shall see, “very large” actually means “at least singly exponential in $n$ ”.

Let $\mathbf{v}\in\mathbb{N}_{\infty}^{d}$ , and let $\pazocal{A}_{\mathbf{v}}$ be the VASS obtained from $\pazocal{A}$ by modifying every counter update vector $\mathbf{u}$ into $\mathbf{u}^{\prime}$ , where $\mathbf{u}^{\prime}(i)=\mathbf{u}(i)$ if $\mathbf{v}(i)\neq\infty$ , otherwise $\mathbf{u}^{\prime}(i)=0$ . Hence, the counters set to $\infty$ in $\mathbf{v}$ are never changed in $\pazocal{A}_{\mathbf{v}}$ . Furthermore, let $\mathbf{v}^{\prime}$ be the vector obtained from $\mathbf{v}$ by changing all $\infty$ components into $1$ . We put $\pazocal{C}_{\pazocal{A}}[c,\mathbf{v}]=\pazocal{C}_{\pazocal{A}_{\mathbf{v}}}[c,\mathbf{v}^{\prime}]$ .

For a given $\mathbf{v}\in\mathbb{N}_{\infty}^{d}$ , we say that $F:\mathbb{N}\rightarrow\mathbb{N}^{d}$ is $\mathbf{v}$ -consistent if for every $i\in\{1,\ldots,d\}$ we have that the projection $F_{i}:\mathbb{N}\rightarrow\mathbb{N}$ is either $\Theta(n^{k})$ if $\mathbf{v}_{i}=k$ , or $2^{\Omega(n)}$ if $\mathbf{v}_{i}=\infty$ . Intuitively, a $\mathbf{v}$ -consistent function assigns to every $n\in\mathbb{N}$ a vector $F(n)$ of initial counter values growing consistently with $\mathbf{v}$ .

Given $\mathbf{v}\in\mathbb{N}_{\infty}^{d}$ , a control state $p\in Q$ , a $\mathbf{v}$ -consistent function $F$ , an infinite family $\Pi=\pi_{1},\pi_{2},\ldots$ of Demon’s strategies in $\pazocal{A}$ , a function $S:\mathbb{N}\rightarrow\mathbb{N}$ , and $n\in\mathbb{N}$ , we use $\beta_{n}[\mathbf{v},p,F,\Pi,S]$ to denote the computation of $\pazocal{A}$ starting at $pF(n)$ obtained by applying $\pi_{n}$ until a maximal computation is produced or $S(n)$ transitions are executed.

The next lemma says that if $\pazocal{A}$ is strongly connected, then all counters can be pumped simultaneously to the values asymptotically equivalent to $\pazocal{C}_{\pazocal{A}}[c,\mathbf{v}]$ so that the counters previously pumped to exponential values stay exponential.

Lemma 3.8.

Let $\pazocal{A}$ be a strongly connected demonic VASS with $d$ counters. Let $\mathbf{v}\in\mathbb{N}_{\infty}^{d}$ , and let $F$ be a $\mathbf{v}$ -consistent function. Then for every counter $c_{i}$ such that $\mathbf{v}_{i}\neq\infty$ and $\pazocal{C}_{\pazocal{A}}[c_{i},\mathbf{v}]\in\Theta(n^{k})$ we have that $\mathit{Cval}[c_{i}](pF(n))\in\Theta(n^{k})$ for every $p\in Q$ . Furthermore, there exist $p\in Q$ , an infinite family $\Pi$ of Demon’s strategies, and a function $S\in 2^{\pazocal{O}(n)}$ such that for every $c_{i}$ , the value of $c_{i}$ in the last configuration of $\beta_{n}[\mathbf{v},p,F,\Pi,S]$ is

•

$\Theta(n^{k})$ if $\pazocal{C}_{\pazocal{A}}[c_{i},\mathbf{v}]\in\Theta(n^{k})$ ;
•

$2^{\Omega(n)}$ if $\mathbf{v}_{i}=\infty$ or $\pazocal{C}{A}[c_{i},\mathbf{v}]\in 2^{\Omega(n)}$ .

A proof of Lemma 3.8 uses the result of [13] saying that counters pumpable to exponential values can be simultaneously pumped by a computation of exponential length from a configuration where all counters are set to $n$ (the same holds for polynomially bounded counters, where the length of the computation can be bounded even by a polynomial). Using the construction of Proposition 3.7, these results are extended to our setting with $\mathbf{v}$ -consistent initial counter values. Then, the initial counter values are virtually “split into $d$ boxes” of size $\lfloor F(n)/d\rfloor$ . The computations pumping the individual counters are then run “each in its own box” for these smaller initial vectors and concatenated. As the computation of one “box” cannot affect any other “box”, no computation can undo the effects of previous computations. The details can be found in Appendix B.4

Let $\pazocal{V}_{\pazocal{A}}:\mathbb{N}_{\infty}^{d}\rightarrow\mathbb{N}_{\infty}^{d}$ be a function such that, for every $\mathbf{v}\in\mathbb{N}_{\infty}^{d}$ ,

\pazocal{V}{A}(\mathbf{v})(i)=\begin{cases}k&\mbox{if $\mathbf{v}_{i}\neq\infty$ and $\pazocal{C}_{\pazocal{A}}[c_{i},\mathbf{v}]\in\Theta(n^{k})$,}\\ \infty&\mbox{otherwise.}\end{cases}

Note that every SCC (vertex) $\eta$ of $\pazocal{D}(\pazocal{A})$ can be seen as a strongly connected demonic VASS after deleting all transitions leading from/to the states outside $\eta$ . If the counters are simultaneously pumped to $\mathbf{v}$ -consistent values before entering $\eta$ , then $\eta$ can further pump the counters to $\pazocal{V}_{\eta}(\mathbf{v})$ -consistent values (see Lemma 3.8). According to Lemma 3.7, $\pazocal{V}_{\eta}(\mathbf{v})$ is computable in polynomial time for every $\mathbf{v}\in\mathbb{N}_{\infty}^{d}$ where every finite $\mathbf{v}_{i}$ is bounded by $2^{j\cdot d}$ for some $j<|Q|$ .

Observe that all computations of $\pazocal{A}$ can be divided into finitely many pairwise disjoint classes according to their corresponding paths in $\pazocal{D}{A}$ (i.e., the sequence of visited SCCs of $\pazocal{D}{A}$ ). For each such sequence $\eta_{1},\ldots,\eta_{m}$ , the vectors $\mathbf{v}_{0},\ldots,\mathbf{v}_{m}$ where $\mathbf{v}_{0}=\vec{1}$ and $\mathbf{v}_{i}=\pazocal{V}_{\eta_{i}}(\mathbf{v}_{i-1})$ are computable in time polynomial in $|\pazocal{A}|$ (note that $m\leq|Q|$ ). The asymptotic growth of the counters achievable by computations following the path $\eta_{1},\ldots,\eta_{m}$ is then given by $\mathbf{v}_{m}$ . Hence, $\pazocal{C}{A}[c_{i}]\in\Omega(n^{k})$ iff there is a path $\eta_{1},\ldots,\eta_{m}$ in $\pazocal{D}{A}$ such that $\mathbf{v}_{m}(i)\geq k$ . Similarly, $\pazocal{C}{A}[c_{i}]\in\pazocal{O}(n^{k})$ iff for every path $\eta_{1},\ldots,\eta_{m}$ in $\pazocal{D}{A}$ we have that $\mathbf{v}_{m}(i)\leq k$ . From this we immediately obtain the upper complexity bounds of Theorem 3.1.

Furthermore, for every SCC $\eta$ of $\pazocal{D}{A}$ , we can compute the set $\textit{Vectors}{A}(\eta)$ of all $\mathbf{u}$ such that there is a path $\eta_{1},\ldots,\eta_{m}$ where $\eta_{1}$ is a root of $\pazocal{D}{A}$ , $\eta_{m}=\eta$ , and $\mathbf{u}=\mathbf{v}_{m}$ . A full description of the algorithm is given in Appendix B.5. If $\textit{Deg}(\eta)$ is bounded by a fixed constant independent of $\pazocal{A}$ for every leaf $\eta$ of $\pazocal{D}_{\pazocal{A}}$ , then the algorithm terminates in polynomial time, which proves Theorem 3.2.

4 VASS Games

The computational complexity of polynomial asymptotic analysis for VASS games is classified in our next theorem. The parameter characterizing hard instances is identified at the end of this section.

Theorem 4.1.

Let $k\geq 1$ . For every VASS game $\pazocal{A}$ and counter $c$ we have that $\pazocal{L}$ ( $\pazocal{C}[c]$ ) is either in $\pazocal{O}(n^{k})$ or in $\Omega(n^{k+1})$ . Furthermore, the problem whether

•

$\pazocal{L}\in\pazocal{O}(n^{k})$ is $\mathbf{NP}$ -complete for $k{=}1$ and $\mathbf{PSPACE}$ -complete for $k{\geq}2$ ;
•

$\pazocal{L}\in\Omega(n^{k})$ is in $\mathbf{P}$ for $k{=}1$ , $\mathbf{coNP}$ -complete for $k{=}2$ , and $\mathbf{PSPACE}$ -complete for $k{\geq}3$ ;
•

$\pazocal{L}\in\Theta(n^{k})$ is $\mathbf{NP}$ -complete for $k{=}1$ and $\mathbf{PSPACE}$ -complete for $k{\geq}2$ ;
•

$\pazocal{C}[c]\in\pazocal{O}(n^{k})$ is $\mathbf{PSPACE}$ -complete;
•

$\pazocal{C}[c]\in\Omega(n^{k})$ is in $\mathbf{P}$ for $k{=}1$ , and $\mathbf{PSPACE}$ -complete for $k{\geq}2$ ;
•

$\pazocal{C}[c]\in\Theta(n^{k})$ is $\mathbf{PSPACE}$ -complete.

Furthermore, we show that for every VASS game $\pazocal{A}$ , either $\pazocal{L}\in\pazocal{O}(n^{2^{d|Q|}})$ or $\pazocal{L}\in 2^{\Omega(n)}$ . In the first case, the $k$ such that $\pazocal{L}\in\Theta(n^{k})$ can be computed in polynomial space. The same results hold for $\pazocal{C}[c]$ .

In [12], it has been shown that the problem whether $\pazocal{L}\in\pazocal{O}(n)$ is $\mathbf{NP}$ -complete, and if $\pazocal{L}\not\in\pazocal{O}(n)$ , then $\pazocal{L}\in\Omega(n^{2})$ . This yields the $\mathbf{NP}$ and $\mathbf{coNP}$ bounds of Theorem 4.1 for $k=1,2$ . Furthermore, it has been shown that the problem whether $\pazocal{L}\in\pazocal{O}(n^{2})$ is $\mathbf{PSPACE}$ -hard, and this proof can be trivially generalized to obtain all $\mathbf{PSPACE}$ lower bounds of Theorem 4.1. For the sake of completeness, we sketch the arguments in Appendix C.

The key insight behind the proof of Theorem 4.1 is that player Angel can safely commit to a simple locking strategy when minimizing the counter complexity. We start by introducing locking strategies.

Definition 4.2.

Let $\pazocal{A}$ be a VASS game. We say that a strategy $\sigma$ for player Angel is locking if for every computation $p_{1}\mathbf{v}_{1},\dots,p_{m}\mathbf{v}_{m}$ where $p_{m}\in Q_{A}$ and for every $k<m$ such that $p_{k}=p_{m}$ we have that $\sigma(p_{1}\mathbf{v}_{1},\dots,p_{k}\mathbf{v}_{k})=\sigma(p_{1}\mathbf{v}_{1},\dots,p_{m}\mathbf{v}_{m})$ .

In other words, when an angelic control state $p$ is visited for the first time, a locking strategy selects and “locks” an outgoing transition of $p$ so that whenever $p$ is revisited, the previously locked transition is taken. Observe that the choice of a “locked” transition may depend on the whole history of a computation.

Since a “locked” control state has only one outgoing transition, it can be seen as demonic. Hence, as more and more control states are locked along a computation, the VASS game $\pazocal{A}$ becomes “more and more demonic”. We capture these changes as a finite acyclic graph $\pazocal{G}{A}$ called the locking decomposition of $\pazocal{A}$ . Then, we say that a locking strategy is simple if the choice of a locked transition after performing a given history depends only on the finite path in $\pazocal{G}{A}$ associated to the history. We show that Angel can achieve an asymptotically optimal termination/counter complexity by using only simple locking strategies. Since the height of $\pazocal{G}{A}$ is polynomial in $|\pazocal{A}|$ , the existence of an appropriate simple locking strategy for Angel can be decided by an alternating polynomial-time algorithm. As $\mathbf{AP}=\mathbf{PSPACE}$ , this proves the $\mathbf{PSPACE}$ upper bounds of Theorem 4.1. Furthermore, our construction identifies the structural parameters of $\pazocal{G}{A}$ making the polynomial asymptotic analysis of VASS games hard. When these parameters are bounded by fixed constants, the problems of Theorem 4.1 are solvable in polynomial time.

4.1 Locking sets and the locking decomposition of $\pazocal{A}$

Let $\pazocal{A}$ be a VASS game. A Demonic decomposition of $\pazocal{A}$ is a finite directed graph $\pazocal{D}{A}$ defined as follows. Let ${\sim}\subseteq Q\times Q$ be an equivalence where $p\sim q$ iff either $p=q$ , or both $p,q$ are demonic and mutually reachable from each other via a finite path leading only through demonic control states. The vertices of $\pazocal{D}{A}$ are the equivalence classes $Q/{\sim}$ , and $[p]\rightarrow[q]$ iff $[p]\neq[q]$ and $(p,\mathbf{u},q)\in\textit{Tran}$ for some $\mathbf{u}$ . For demonic VASS, $\pazocal{D}{A}$ becomes the standard DAG decomposition. For VASS games, $\pazocal{D}{A}$ is not necessarily acyclic.

A locking set of $\pazocal{A}$ is a set of transitions $L\subseteq\textit{Tran}$ such that $(p,\mathbf{u},q)\in L$ implies $p\in Q_{A}$ , and $(p,\mathbf{u},q),(p^{\prime},\mathbf{u}^{\prime},q^{\prime})\in L$ implies $p\neq p^{\prime}$ . A control state $p$ is locked by $L$ if $L$ contains an outgoing transition of $p$ . We use $\mathscr{L}$ to denote the set of all locking sets of $\pazocal{A}$ . For every $L\in\mathscr{L}$ , let $\pazocal{A}_{L}$ be the VASS game obtained from $\pazocal{A}$ by “locking” the transitions of $L$ . That is, each control state $p$ locked by $L$ becomes demonic in $\pazocal{A}_{L}$ , and the only outgoing transition of $p$ in $\pazocal{A}_{L}$ is the transition $(p,\mathbf{u},q)\in L$ .

Definition 4.3.

The locking decomposition of $\pazocal{A}$ is a finite directed graph $\pazocal{G}{A}$ where the set of vertices and the set of edges of $\pazocal{G}{A}$ are the least sets $V$ and $\rightarrow$ satisfying the following conditions:

•

All elements of $V$ are pairs $([p],L)$ where $L\in\mathscr{L}$ and $[p]$ is a vertex of $\pazocal{D}_{\pazocal{A}_{L}}$ . When $p$ is demonic/angelic in $\pazocal{A}_{L}$ , we say that $([p],L)$ is demonic/angelic.
•

$V$ contains all pairs of the form $([p],\emptyset)$ .
•

If $([p],L)\in V$ where $p$ is demonic in $\pazocal{A}_{L}$ and $[p]\rightarrow[q]$ is an edge of $\pazocal{D}_{\pazocal{A}_{L}}$ , then $([q],L)\in V$ and $([p],L)\rightarrow([q],L)$ .
•

If $([p],L)\in V$ where $p$ is angelic in $\pazocal{A}_{L}$ , then for every $(p,\mathbf{u},q)\in\textit{Tran}$ we have that $([q],L^{\prime})\in V$ and $([p],L)\rightarrow([q],L^{\prime})$ , where $L^{\prime}=L\cup\{(p,\mathbf{u},q)\}$ .

It is easy to see that $\pazocal{G}{A}$ is acyclic and the length of every path in $\pazocal{G}{A}$ is bounded by $|Q|+|Q_{A}|$ , where at most $|Q|$ vertices in the path are demonic. Note that every computation of $\pazocal{A}$ obtained by applying a locking strategy determines its associated path in $\pazocal{G}{A}$ in the natural way. A locking strategy $\sigma$ is simple if the choice of a locked transition depends only on the path in $\pazocal{G}{A}$ associated to the performed history. (i.e., if two histories determine the same path in $\pazocal{G}{A}$ , then the strategy makes the same choice for both histories).

4.2 Upper bounds

Let $\pazocal{A}$ be a VASS game with $d$ counters. For every $p\in Q$ and $\mathbf{v}\in\mathbb{N}^{d}$ , let $\pazocal{C}{A}^{p}[c,\mathbf{v}](n)=\mathit{Cval}[c](p\mathbf{u})$ where $\mathbf{u}=(n^{\mathbf{v}(1)},\ldots,n^{\mathbf{v}(d)})$ . We extend this notation to the vectors $\mathbf{v}\in\mathbb{N}_{\infty}^{d}$ in the same way as in Section 3.2, i.e., for a given $\mathbf{v}\in\mathbb{N}_{\infty}^{d}$ , we put $\pazocal{C}_{\pazocal{A}}^{p}[c,\mathbf{v}]=\pazocal{C}_{\pazocal{A}_{\mathbf{v}}}^{p}[c,\mathbf{v}^{\prime}]$ . Recall that $\mathbf{v}^{\prime}$ is the vector obtained from $\mathbf{v}$ by changing all $\infty$ components into $1$ , and $\pazocal{A}_{\mathbf{v}}$ is the VASS obtained from $\pazocal{A}$ by modifying every counter update vector $\mathbf{u}$ into $\mathbf{u}^{\prime}$ , where $\mathbf{u}^{\prime}(i)=\mathbf{u}(i)$ if $\mathbf{v}(i)\neq\infty$ , otherwise $\mathbf{u}^{\prime}(i)=0$ . The main technical step towards obtaining the $\mathbf{PSPACE}$ upper bounds of Theorem 4.1 is the next proposition.

Proposition 4.4.

Let $\pazocal{A}$ be a VASS game with $d$ counters. Furthermore, let $([p],L)$ be a vertex of $\pazocal{G}{A}$ , $\mathbf{v}\in\mathbb{N}_{\infty}^{d}$ , and $c_{i}$ a counter such that $\mathbf{v}_{i}\neq\infty$ . Then, one of the following two possibilities holds:

•
there is $k\in\mathbb{N}$ such that for every $\mathbf{v}$ -consistent $F$ there exist a simple locking Angel’s strategy $\sigma_{\mathbf{v}}$ in $\pazocal{A}_{L}$ and a Demon’s strategy $\pi_{\mathbf{v}}$ in $\pazocal{A}_{L}$ such that $\sigma_{\mathbf{v}}$ is independent of $F$ and
- –
  
  for every Demon’s strategy $\pi$ in $\pazocal{A}_{L}$ , we have that $\textit{max}[c_{i}](\mathit{Comp}_{\pazocal{A}_{L}}^{\sigma_{\mathbf{v}},\pi}(p\,F(n)))\in\pazocal{O}(n^{k})$ ;
- –
  
  for every Angel’s strategy $\sigma$ in $\pazocal{A}_{L}$ , we have that $\textit{max}[c_{i}](\mathit{Comp}_{\pazocal{A}_{L}}^{\sigma,\pi_{\mathbf{v}}}(p\,F(n)))\in\Omega(n^{k})$ .
•

for every $\mathbf{v}$ -consistent $F$ there is a Demon’s strategy $\pi_{\mathbf{v}}$ in $\pazocal{A}_{L}$ such that for every Angel’s strategy $\sigma$ in $\pazocal{A}_{L}$ , we have that $\textit{max}[c_{i}](\mathit{Comp}_{\pazocal{A}_{L}}^{\sigma,\pi_{\mathbf{v}}}(p\,F(n)))\in 2^{\Omega(n)}$ .

Proposition 4.4 is proven by induction on the height of the subgraph rooted by $([p],L)$ . The case when $([p],L)$ is demonic (which includes the base case when $([p],L)$ is a leaf) follows from the constructions used in the proof of Proposition 3.7. When the vertex $([p],L)$ is angelic, it has immediate successors of the form $([q_{i}],L_{i})$ where $L_{i}=L\cup\{(p,\mathbf{u}_{i},q_{i})\}$ . We show that by locking one of the $(p,\mathbf{u}_{i},q_{i})$ transitions in $p$ , Angel can minimize the growth of $c_{i}$ in asymptotically the same way as if he used all of these transitions freely when revisiting $p$ . See Appendix C.2 for details.

Observe that every computation in $\pazocal{A}$ where Angel uses some simple locking strategy determines the unique corresponding path in $\pazocal{G}{A}$ (initiated in a vertex of the form $([p],\emptyset)$ ) in the natural way. Hence, all such computations can be divided into finitely many pairwise disjoint classes according to their corresponding paths in $\pazocal{G}{A}$ . Let $([p_{1}],L_{1}),\ldots,([p_{k}],L_{k})$ be a path in $\pazocal{G}{A}$ where $L_{1}=\emptyset$ . Consider the corresponding sequence $\mathbf{v}_{0},\ldots,\mathbf{v}_{k}$ where $\mathbf{v}_{0}=\vec{1}$ and $\mathbf{v}_{i}$ is equal either to $\pazocal{V}_{[p_{i}]}(\mathbf{v}_{i-1})$ or to $\mathbf{v}_{i-1}$ , depending on whether $([p_{i}],L_{i})$ is demonic or angelic, respectively. Here, $\pazocal{V}$ is the function defined in Section 3.2 (observe that the component $[p]$ of $\pazocal{D}_{A_{L}}$ containing $p$ can be seen as a strongly connected demonic VASS after deleting all transitions from/to the states outside $[p]$ ). The vector $\mathbf{v}_{k}$ describes the maximal asymptotic growth of the counters achievable by Demon when Angel uses the simple locking strategy associated to the path. Furthermore, the sequence $\mathbf{v}_{0},\ldots,\mathbf{v}_{k}$ is computable in time polynomial in $|\pazocal{A}|$ and all finite components of $\mathbf{v}_{k}$ are bounded by $2^{d\cdot|Q|}$ because the total number of all demonic $([p_{i}],L_{i})$ in the path is bounded by $|Q|$ (cf. Proposition 3.7).

The problem whether $\pazocal{C}[c_{i}]\in\pazocal{O}(n^{k})$ can be decided by an alternating polynomial-time algorithm which selects an initial vertex of the form $([p],\emptyset)$ universally, and then constructs a maximal path in $\pazocal{G}{A}$ from $([p],\emptyset)$ where the successors of demonic/angelic vertices are chosen universally/existentially, respectively. After obtaining a maximal path $([p_{1}],L_{1}),\ldots,([p_{k}],L_{k})$ , the vector $\mathbf{v}_{k}$ is computed in polynomial time, and the algorithm answers yes/no depending on whether $\mathbf{v}_{k}(i)\leq k$ or not, respectively. The problem whether $\pazocal{C}[c_{i}]\in\Omega(n^{k})$ is decided similarly, but here the initial vertex is chosen existentially, the successors of demonic/angelic vertices are chosen existentially/universally, and the algorithm answers yes/no depending on whether $\mathbf{v}_{k}(i)\geq k$ or not, respectively. This proves the $\mathbf{PSPACE}$ upper bounds of Theorem 4.1.

Observe that the crucial parameter influencing the computational hardness of the asymptotic analysis for VASS games is the number of maximal paths in $\pazocal{G}{A}$ . If $|Q_{A}|$ and $\textit{Deg}([p],L)$ are bounded by constants, then the above alternating polynomial time algorithms can be simulated by deterministic polynomial time algorithms. Thus, we obtain the following:

Theorem 4.5.

Let $\Lambda$ be a class of VASS games such that for every $\pazocal{A}\in\Lambda$ we have that $|Q_{A}|$ and $\textit{Deg}([p],L)$ , where $([p],L)$ is a leaf of $\pazocal{G}{A}$ , are bounded by a fixed constant depending only on $\Lambda$ . Then, the problems whether $\pazocal{L}{A}\in\pazocal{O}(n^{k})$ , $\pazocal{L}{A}\in\Omega(n^{k})$ , $\pazocal{L}{A}\in\Theta(n^{k})$ for given $\pazocal{A}\in\Lambda$ and $k\in\mathbb{N}$ , are solvable in polynomial time (where the $k$ is written in binary). The same results hold also for $\pazocal{C}[c]$ (for a given counter $c$ of $\pazocal{A}$ ).

5 Conclusions, future work

We presented a precise complexity classification for the problems of polynomial asymptotic complexity of demonic VASS and VASS games. We also identified the structural parameters making these problems computationally hard, and we indicated that these parameters may actually stay reasonably small when dealing with VASS abstractions of computer programs. The actual applicability and scalability of the presented results to the problems of program analysis requires a more detailed study including experimental evaluation.

From a theoretical point of view, a natural question is whether the scope of effective asymptotic analysis can be extended from purely non-deterministic VASS to VASS with probabilistic transitions (i.e., VASS MDPs and VASS stochastic games). These problems are challenging and motivated by their applicability to probabilistic program analysis.

References

[1] E. Albert, P. Arenas, S. Genaim, M. Gómez-Zamalloa, G. Puebla, D. V. Ramírez-Deantes, G. Román-Díez, and D. Zanardini. Termination and cost analysis with COSTA and its user interfaces. ENTCS, 258(1):109–121, 2009.
[2] C. Alias, A. Darte, P. Feautrier, and L. Gonnord. Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs. In Proceedings of SAS 2010, pages 117–133, 2010.
[3] T. Brázdil, K. Chatterjee, A. Kučera, P. Novotný, and D. Velan. Deciding fast termination for probabilistic VASS with nondeterminism. In Proceedings of ATVA 2019, volume 11781 of LNCS, pages 462–478. Springer, 2019.
[4] T. Brázdil, K. Chatterjee, A. Kučera, P. Novotný, D. Velan, and F. Zuleger. Efficient algorithms for asymptotic bounds on termination time in VASS. In Proceedings of LICS 2018, pages 185–194. ACM Press, 2018.
[5] M. Broy and M. Wirsing. On the algebraic specification of nondeterministic programming languages. In Proceedings of CAAP’81, volume 112 of LNCS, pages 162–179. Springer, 1981.
[6] Q. Carbonneaux, J. Hoffmann, T. W. Reps, and Z. Shao. Automated resource analysis with coq proof objects. In Proceedings of CAV 2017, pages 64–85, 2017.
[7] W. Czerwiński, S. Lasota, R. Lazić, J. Leroux, and F. Mazowiecki. The reachability problem for Petri nets is not elementary. In Proceedings of STOC 2019, pages 24–33. ACM Press, 2019.
[8] A. F.-Montoya and R. Hähnle. Resource analysis of complex programs with cost equations. In Proceedings of APLAS 2014, pages 275–295, 2014.
[9] J. Giesl, C. Aschermann, M. Brockschmidt, F. Emmes, F. Frohn, C. Fuhs, J. Hensel, C. Otto, M. Plücker, P. Schneider-Kamp, T. Ströder, S. Swiderski, and R. Thiemann. Analyzing program termination and complexity automatically with aprove. J. Autom. Reasoning, 58(1):3–31, 2017.
[10] S. Gulwani, K. K. Mehra, and T. M. Chilimbi. SPEED: precise and efficient static estimation of program computational complexity. In Proceedings of POPL 2009, pages 127–139, 2009.
[11] J. Hoffmann, K. Aehlig, and M. Hofmann. Multivariate amortized resource analysis. ACM Trans. Program. Lang. Syst., 34(3):14:1–14:62, 2012.
[12] A. Kučera, J. Leroux, and D. Velan. Efficient analysis of VASS termination complexity. In Proceedings of LICS 2020, pages 676–688. ACM Press, 2020.
[13] J. Leroux. Polynomial vector addition systems with states. In Proceedings of ICALP 2018, volume 107 of LIPIcs, pages 134:1–134:13. Schloss Dagstuhl, 2018.
[14] R. Lipton. The reachability problem requires exponential space. Technical report 62, Yale University, 1976.
[15] E.W. Mayr and A.R. Meyer. The complexity of the finite containment problem for Petri nets. JACM, 28(3):561–576, 1981.
[16] Ch. Papadimitriou. Computational Complexity. Addison, 1994.
[17] M. Sinn, F. Zuleger, and H. Veith. A simple and scalable static analysis for bound analysis and amortized complexity analysis. In Proccedings of CAV 2014, pages 745–761, 2014.
[18] M. Sinn, F. Zuleger, and H. Veith. Complexity and resource bound analysis of imperative programs using difference constraints. J. Autom. Reasoning, 59(1):3–45, 2017.
[19] F. Zuleger. The polynomial complexity of vector addition systems with states. In Proceedings of FoSSaCS 2020, volume 12077 of LNCS, pages 622–641. Springer, 2020.

Appendix A The Existence of Equilibrium Value in VASS Games

In this section, we sketch a proof for the equalities

	$\displaystyle\sup_{\pi}\ \operatornamewithlimits{inf\vphantom{p}}_{\sigma}\ \textit{len}(\mathit{Comp}^{\sigma,\pi}(p\mathbf{v}))$	$\displaystyle=$	$\displaystyle\operatornamewithlimits{inf\vphantom{p}}_{\sigma}\ \sup_{\pi}\ \textit{len}(\mathit{Comp}^{\sigma,\pi}(p\mathbf{v}))$
	$\displaystyle\sup_{\pi}\ \operatornamewithlimits{inf\vphantom{p}}_{\sigma}\ \textit{max}[c](\mathit{Comp}^{\sigma,\pi}(p\mathbf{v}))$	$\displaystyle=$	$\displaystyle\operatornamewithlimits{inf\vphantom{p}}_{\sigma}\ \sup_{\pi}\ \textit{max}[c](\mathit{Comp}^{\sigma,\pi}(p\mathbf{v}))$

used in Section 2. These results appear folklore and plausible. Still, they do not immediately follow from the standard determinacy results for Borel objectives because the reward function is not bounded. Due to the importance of these equalities, we believe they are worth a proof sketch.

We prove the determinacy result for arbitrary finitely-branching games with countably many vertices. Consider a game $G=(V,{\rightarrow},c)$ where $V$ is a countably infinite set of vertices partitioned into the subsets $V_{D}$ and $V_{A}$ of demonic and angelic vertices, ${\rightarrow}\subseteq V\times V$ is a finitely-branching transition relation (i.e., every vertex $v$ has only finitely many immediate successors), and $c:V\rightarrow\mathbb{N}$ is a cost function. Furthermore, we fix an initial vertex $\hat{v}$ . For every maximal path $\alpha$ initiated in $\hat{v}$ , let $\textit{max}[c](\alpha)$ be the supremum of the costs of all vertices visited by $\alpha$ . We show that

\sup_{\pi}\ \operatornamewithlimits{inf\vphantom{p}}_{\sigma}\ \textit{max}[c](\alpha^{\sigma,\pi})\quad=\quad\operatornamewithlimits{inf\vphantom{p}}_{\sigma}\ \sup_{\pi}\ \textit{max}[c](\alpha^{\sigma,\pi})

where $\pi$ and $\sigma$ range over the strategies for Demon/Angel in $G$ , and $\alpha^{\sigma,\pi}$ is the unique maximal path initiated in $\hat{v}$ determined by $\pi$ and $\sigma$ .

Let $\Gamma:\mathbb{N}_{\infty}^{V}\rightarrow\mathbb{N}_{\infty}^{V}$ be a (Bellman) operator such that, for a given $f:V\rightarrow\mathbb{N}_{\infty}$ , we have that $\Gamma(f)=g$ , where $g:V\rightarrow\mathbb{N}_{\infty}$ is defined as follows:

g(v)=\begin{cases}\max\big{\{}c(v),\max\{f(u)\mid v\rightarrow u\}\big{\}}&\mbox{if }v\in V_{D}\\ \max\big{\{}c(v),\min\{f(u)\mid v\rightarrow u\}\big{\}}&\mbox{if }v\in V_{A}\end{cases}

Since $\Gamma$ is a continuous operator over the CPO of all functions $V\rightarrow\mathbb{N}_{\infty}$ with component-wise ordering, there is the least fixed-point $\mu\Gamma=\bigsqcup_{i=0}^{\infty}\Gamma^{i}(\perp)$ of $\Gamma$ , where $\perp$ is the least element (i.e., a function assigning $0$ to every vertex). Consider two memoryless strategies $\pi^{*}$ and $\sigma^{*}$ for Demon and Angel such that

•

for every $v\in V_{D}$ , the strategy $\pi^{*}$ selects a successor of $v$ with the maximal $\mu\Gamma$ value;
•

for every $v\in V_{A}$ , the strategy $\sigma^{*}$ selects a successor of $v$ with the minimal $\mu\Gamma$ value.

Now, it suffices to show that

\mu\Gamma(\hat{v})\quad\leq\quad\sup_{\pi}\ \operatornamewithlimits{inf\vphantom{p}}_{\sigma}\ \textit{max}[c](\alpha^{\sigma,\pi})\quad\leq\quad\operatornamewithlimits{inf\vphantom{p}}_{\sigma}\ \sup_{\pi}\ \textit{max}[c](\alpha^{\sigma,\pi})\quad\leq\quad\mu\Gamma(\hat{v})

(3)

The second inequality of (3) holds trivially. For the first inequality, observe that

\operatornamewithlimits{inf\vphantom{p}}_{\sigma}\ \textit{max}[c](\alpha^{\sigma,\pi^{*}})\quad\leq\quad\sup_{\pi}\ \operatornamewithlimits{inf\vphantom{p}}_{\sigma}\ \textit{max}[c](\alpha^{\sigma,\pi})

Hence, it suffices to show $\mu\Gamma(\hat{v})\leq\operatornamewithlimits{inf\vphantom{p}}_{\sigma}\textit{max}[c](\alpha^{\sigma,\pi^{*}})$ , which is achieved by demonstrating $\Gamma^{i}(\perp)(\hat{v})\leq\operatornamewithlimits{inf\vphantom{p}}_{\sigma}\textit{max}[c](\alpha^{\sigma,\pi^{*}})$ for every $i\in\mathbb{N}$ (by induction on $i$ ). The last inequality in (3) is proven similarly (using $\sigma^{*}$ ).

Appendix B Proofs for Section 3

B.1 A proof of Lemma 3.5

See 3.5

Proof B.1.

The structure of $\pazocal{A}_{\varphi,\psi}$ is given by the VASS Program 2. The program starts by executing the first eight lines of the VASS Program 1 constructed for $\varphi$ and $k-1$ , followed by the first eight lines of the same program constructed for $\psi$ and $k-1$ where all variables representing the counters are fresh and previously unused. According to the proof of Lemma 3.3, the Demon can perform $\Theta(n^{k-1})$ transitions when executing the first two lines of the VASS Program 2 regardless whether the formulae $\varphi,\psi$ are satisfiable or not. Let $s(\pazocal{A}_{\varphi})$ and $s(\pazocal{A}_{\psi})$ be the counters of $\pazocal{A}_{\varphi}$ and $\pazocal{A}_{\psi}$ corresponding to the counter $s_{m}$ of the VASS Program 1. According to Lemma 3.3, we have the following:

•

If $\varphi$ is satisfiable, then the counter $s(\pazocal{A}_{\varphi})$ can be pumped to $\Theta(n^{k-1})$ ; otherwise, it can be pumped only to $\Theta(n)$ .
•

If $\psi$ is satisfiable, then the counter $s(\pazocal{A}_{\psi})$ can be pumped to $\Theta(n^{k-1})$ ; otherwise, it can be pumped only to $\Theta(n)$ .

The instructions at lines 2 and 2 ensure that $\pazocal{L}_{\pazocal{A}_{\varphi,\psi}}\in\Theta(n^{k})$ iff the counter $s(\pazocal{A}_{\varphi})$ can be pumped to $\Theta(n^{k-1})$ and the counter $s(\pazocal{A}_{\psi})$ can be pumped only to $\Theta(n)$ . More precisely, the instructions at line 2 multiply the values of these two counters. Hence, if both values are $\Theta(n^{k-1})$ , the multiplication gadget executes $\Theta(n^{2k-2})$ transitions, which is beyond $\Theta(n^{k})$ . If one of the counter values is $\Theta(n)$ and the other is $\Theta(n^{k-1})$ , the multiplication takes $\Theta(n^{k})$ transitions. Finally, if both values are $\Theta(n)$ , the multiplication takes $\Theta(n^{2})$ transitions. The instructions at line 2 compute the square of the value stored in $s(\pazocal{A}_{\psi})$ , which takes either $\Theta(n^{2k-2})$ or $\Theta(n^{2})$ transitions, depending on whether the value of $s(\pazocal{A}_{\psi})$ is $\Theta(n^{k-1})$ or $\Theta(n)$ , respectively. So, the only case when these instructions produce a sequence of transitions of length $\Theta(n^{k})$ is when the value of $s(\pazocal{A}_{\varphi})$ is $\Theta(n^{k-1})$ and the value of $s(\pazocal{A}_{\psi})$ is $\Theta(n)$ .

1 lines 1–1 of

\pazocal{A}_{\varphi}

constructed for

k-1

;

2 lines 1–1 of

\pazocal{A}_{\psi}

constructed for

k-1

; /* all counters are fresh */

a\texttt{\,+=\,}s(\pazocal{A}_{\varphi});

b\texttt{\,+=\,}s(\pazocal{A}_{\psi});

e\texttt{\,+=\,}a*b

; /*

a,b,e

are fresh counters */

c\texttt{\,+=\,}s(\pazocal{A}_{\psi});

d\texttt{\,+=\,}s(\pazocal{A}_{\psi});

f\texttt{\,+=\,}c*d

; /*

c,d,f

are fresh counters */

VASS Program 2

\pazocal{A}_{\varphi,\psi}

B.2 A proof of Lemma 3.6

See 3.6

Proof B.2.

The structure of $\pazocal{A}_{\varphi,\psi}$ is given by the VASS Program 3. The program starts by executing the first eight lines of the VASS Program 1 constructed for $\varphi$ and $k+1$ , followed by the first eight lines of the same program constructed for $\psi$ and $k+1$ where all variables representing the counters are fresh and previously unused. Let $s(\pazocal{A}_{\varphi})$ and $s(\pazocal{A}_{\psi})$ be the counters of $\pazocal{A}_{\varphi}$ and $\pazocal{A}_{\psi}$ corresponding to the counter $s_{m}$ of the VASS Program 1. According to Lemma 3.3, we have the following:

•

If $\varphi$ is satisfiable, then the counter $s(\pazocal{A}_{\varphi})$ can be pumped to $\Theta(n^{k+1})$ ; otherwise, it can be pumped only to $\Theta(n)$ .
•

If $\psi$ is satisfiable, then the counter $s(\pazocal{A}_{\psi})$ can be pumped to $\Theta(n^{k+1})$ ; otherwise, it can be pumped only to $\Theta(n)$ .

The instructions at line 3 pump $d_{k-1}$ to $\Theta(n^{k-1})$ . Thus the instructions at line 3 ensure if $\varphi$ is unsatisfiable then $c$ can be pumped at most to $\Theta(n)$ , and if $\varphi$ is satisfiable then $c$ can be pumped at most to $\Theta(n^{k+1})$ or $\Theta(n^{k})$ depending on whether $\psi$ is satisfiable or unsatisfiable, respectively. Therefore $\pazocal{C}_{\pazocal{A}_{\varphi,\psi}}[c]\in\Theta(n^{k})$ iff $\varphi$ is satisfiable and $\psi$ is unsatisfiable.

1 lines 1–1 of

\pazocal{A}_{\varphi}

constructed for

k+1

;

2 lines 1–1 of

\pazocal{A}_{\psi}

constructed for

k+1

; /* all counters are fresh */

d_{2}\texttt{\,+=\,}d_{1}*e_{1};\ \ d_{3}\texttt{\,+=\,}d_{2}*e_{2};\ \cdots\ ;\ \ d_{k-1}\texttt{\,+=\,}d_{k-2}*e_{k-2};

/* all counters are fresh */

c\texttt{\,+=\,}s(\pazocal{A}_{\varphi});

b\texttt{\,+=\,}s(\pazocal{A}_{\psi})*d_{k-1};

c\texttt{\,+=\,}min(a,b)

; /*

a,b,c

are fresh counters */

VASS Program 3

\pazocal{A}_{\varphi,\psi}

B.3 A proof of Proposition 3.7

In this section we give a full proof of Proposition 3.7. We start by recalling the special variant proven in [19].

Proposition B.3 (see [19]).

Let $\pazocal{A}$ be a strongly connected demonic VASS with $d$ counters. For every counter $c$ , we have that either $\pazocal{C}[c]\in\Theta(n^{k})$ for some $1\leq k\leq 2^{d}$ , or $\pazocal{C}[c]\in\Omega(2^{n})$ . It is decidable in polynomial time which of the two possibilities holds. In the first case, the $k$ is computable in polynomial time.

Our proof of Proposition 3.7 is obtained by modifying a given demonic VASS $\pazocal{A}$ into another demonic VASS $\hat{\pazocal{A}}$ and applying Proposition B.3 to $\hat{\pazocal{A}}$ . See 3.7

Proof B.4.

Let $c_{1},\ldots,c_{d}$ be the counters of $\pazocal{A}$ . We start by constructing a VASS $\pazocal{B}$ that “pumps” every $c_{i}$ to $n^{\mathbf{v}(i)}$ from an initial configuration with all counters set to $n$ (see VASS Program 4). Since the components of $\mathbf{v}$ can be exponential in $d$ , the trivial technique used in line 1 of VASS Program 1 is not applicable because it requires $\Omega(2^{j\cdot d})$ new counters and control states. Hence, $\pazocal{B}$ needs to be constructed more carefully using repeated squaring. Let $\max_{\mathbf{v}}$ be the maximal component of $\mathbf{v}$ , and let $\ell=\lfloor\log(\max_{\mathbf{v}})\rfloor$ . Then, for every $1\leq i\leq d$ , there is a vector $\vec{t}_{i}\in\{0,1\}^{\ell+1}$ computable in time polynomial in $|\pazocal{A}|$ such that $\mathbf{v}(i)=\vec{t}_{i}*(2^{0},\ldots,2^{\ell})$ . Let $f_{i}$ be the least index $k$ such that $\vec{t}_{i}(k)=1$ . At line 4, the counter $m_{j}$ is pumped to $\Theta(n^{2^{j}})$ . Note that when maximizing the value of $m_{j}$ , the corresponding gadget (see Fig. 3) leaves $0$ either in $m_{j-1}$ or in $\alpha$ , and the value of both counters is at most $1$ . The nested loop at lines 4–4 increase the counter $s_{i}$ by $n^{\vec{t}_{i}*(2^{0},\ldots,2^{\ell})}$ for every $i=1,\ldots,d$ using the $m_{j}$ counters. Note that every counter is initialized to $n$ , so no computation is needed for $j=0$ . Also note that the if statements at lines 4–4 are purely symbolic—the conditions $\vec{t}_{i}(j)=1$ , $f_{i}=j$ and $f_{i}\neq j$ are constants denoting either true or false, and the instructions following then are either included into the code of $\pazocal{B}$ or not. At lines 4–4, the values stored in $s_{1},\ldots,s_{d}$ are added to the counters $c_{1},\ldots,c_{d}$ . The gadget for the instruction $x\texttt{\,+=\,}[y]$ “reads” the value of $y$ destructively, i.e., the counter $y$ is not restored to its original value (cf. the gadget for $x\texttt{\,+=\,}y$ of Fig. 3).

Note that the VASS $\pazocal{B}$ has two distinguished control states in and out, and uses $\kappa$ auxiliary counters different from $c_{1},\ldots,c_{d}$ . Hence, the total number of counters of $\pazocal{B}$ is $d+\kappa$ . The transition update vectors of $\pazocal{B}$ are constructed so that the first $d$ components specify the updates for $c_{1},\ldots,c_{d}$ . An important observation is that even if we extended $\pazocal{B}$ with a transition $(\textit{out},\vec{0},\textit{in})$ allowing for “restarting” the computation of $\pazocal{B}$ , this extra transition would be of no use when maximizing the values of $c_{1},\ldots,c_{\ell}$ . The best the Demon could do is to maximize the value of all $m_{j}$ , then maximize all $s_{i}$ , and then empty $s_{i}$ by transferring its content to $c_{i}$ . If the Demon violated from this scenario, leaving some positive values in the auxiliary counters of $\pazocal{B}$ and then “restarting” the computation of $\pazocal{B}$ using the transition $(\textit{out},\vec{0},\textit{in})$ , the resulting value of $c_{1},\ldots,c_{\ell}$ would be only smaller.

Now we construct a VASS $\pazocal{U}$ with $d+\kappa$ counters by taking the union of $\pazocal{A}$ and $\pazocal{B}$ , where the transition update vectors of $\pazocal{A}$ are extended so that they do not modify the extra $\kappa$ counters of $\pazocal{B}$ . Furthermore, for every control state $p$ of $\pazocal{A}$ , we add to $\pazocal{U}$ the transitions $(p,-\vec{m},\textit{in})$ and $(\textit{out},-\vec{m},p)$ . Here, $m=|Q|\cdot M$ , where $M$ is the maximal absolute value of an update vector component in $\pazocal{A}$ . Observe that $\pazocal{U}$ is strongly connected and its size is polynomial in the size of $\pazocal{A}$ .

We show that for every $c_{i}$ , where $i\in\{1,\ldots,d\}$ , the asymptotic growth of $\pazocal{C}[c_{i}]$ in $\pazocal{U}$ is the same as the asymptotic growth of $\pazocal{C}[c_{i},\mathbf{v}]$ in $\pazocal{A}$ . Hence, it suffices to apply Proposition B.3 to $\pazocal{U}$ .

Clearly, $\pazocal{C}_{\pazocal{A}}[c_{i},\mathbf{v}]\in\pazocal{O}(\pazocal{C}_{\pazocal{U}}[c_{i}])$ because $\pazocal{U}$ can use the sub-VASS $\pazocal{B}$ to pump every $c_{j}$ to $\Theta(n^{\mathbf{v}(j)})$ and then simulate a computation of $\pazocal{A}$ . It remains to show $\pazocal{C}_{\pazocal{U}}[c_{i}]\in\pazocal{O}(\pazocal{C}_{\pazocal{A}}[c_{i},\mathbf{v}])$ . To see this, it suffices to verify that the best strategy for the Demon who aims at maximizing the value of $c_{i}$ in a computation of $\pazocal{U}$ initiated in a configuration with all counters set to $n$ is to start in the in state of the sub-VASS $\pazocal{B}$ and pump all $c_{1},\ldots,c_{d}$ to their maximal values, and then continue by simulating $\pazocal{A}$ without ever returning to the in state of the sub-VASS $\pazocal{B}$ . Such a computation can be “simulated” by $\pazocal{A}$ from an initial configuration where every $c_{j}$ is set to $n^{\mathbf{v}(j)}$ , which proves our claim.

Obviously, an extra “detour” to $\pazocal{B}$ is of no use if the counters $c_{1},\ldots,c_{d}$ have previously been pumped to their maximal values. As noted above, the Demon cannot gain anything by deviating from the scenario when $c_{1},\ldots,c_{d}$ are pumped just once at the beginning because the total increase in the values of $c_{1},\ldots,c_{d}$ brought by running the sub-VASS $\pazocal{B}$ could be only smaller. So, the only reason why Demon might still wish to re-visit $\pazocal{B}$ by entering in from a control state $p$ of the sub-VASS $\pazocal{A}$ is a “shorter” path to some other control state $q$ of the sub-VASS $\pazocal{A}$ passing through the sub-VASS $\pazocal{B}$ . However, since $\pazocal{A}$ is strongly connected, the Demon can always move from $p$ to $q$ via the control states of $\pazocal{A}$ and the total decrease in every counter will be only smaller than the decrease caused by the transitions $(p,-\vec{m},\textit{in})$ and $(\textit{out},-\vec{m},q)$ . To sum up, the optimal strategy for Demon is to use the sub-VASS $\pazocal{B}$ only at the beginning to pump all $c_{1},\ldots,c_{d}$ to their maximal values, and then schedule an appropriate computation of the sub-VASS $\pazocal{A}$ .

1 foreach $j=1,\ldots,\ell$ do

m_{j}\texttt{\,+=\,}m_{j-1}*m_{j-1};

3 foreach $i=1,\ldots,d$ do

4 if $\vec{t}_{i}(j)=1$ then

5 if $f_{i}=j$ then

s_{i}\texttt{\,+=\,}m_{j};

6 if $f_{i}\neq j$ then

a(i,j)\texttt{\,+=\,}s_{i};\ \ s_{i}\texttt{\,+=\,}m_{j}*a(i,j);

8 end if

10 end foreach

12 end foreach

14foreach $i=1,\ldots,d$ do

c_{i}\texttt{\,+=\,}[s_{i}];

16 +

x

x\texttt{\,+=\,}[y]

17 end foreach

VASS Program 4 The “pumping” VASS

\pazocal{B}

B.4 A Proof of Lemma 3.8

First, let us restate Lemma 3.8.

See 3.8

Let $\pazocal{A}$ be a strongly connected VASS. For every cycle $\gamma$ of $\pazocal{A}$ , let $\Delta(\gamma)$ be the sum of the counter update vectors of the transitions executed along $\gamma$ .

First we will need the following result of [13]. Let $\pazocal{E}$ be the set of all counters $c$ such that $\pazocal{C}_{\pazocal{A}}[c]\in 2^{\Omega(n)}$ . Then there exists an iteration scheme for $\pazocal{E}$ , i.e., a sequence of cycles $\gamma_{1},\ldots,\gamma_{k}$ such that every counter strictly decremented by some $\Delta(\gamma_{i})$ is strictly incremented by $\sum_{i=1}^{k}\Delta(\gamma_{i})$ . Furthermore, $\pazocal{E}$ is precisely the set of all counters strictly incremented by $\sum_{i=1}^{k}\Delta(\gamma_{i})$ . In [13], it is shown that an iteration scheme can be “iterated exponentially many times”, producing a computation of length $2^{\pazocal{O}(n)}$ such that all counters of $\pazocal{E}$ are simultaneously pumped to the value $2^{\Omega(n)}$ (see Lemma 10 in [13]).

Second, every counter $c$ such that $\pazocal{C}_{\pazocal{A}}[c]\in\pazocal{O}(n^{k})$ can be pumped to the value $\Omega(n^{k})$ by a computation of polynomial length (using the results of [19], it is easy to show that the length of the computation can be bounded by $\pazocal{O}(n^{k+1})$ ; for our purposes, even a singly exponential bound is sufficient, so there is no need to go into the details).

The above mentioned results assume that the vector of initial counter values is $\vec{n}$ . Now let $\mathbf{v}\in\mathbb{N}_{\infty}^{d}$ . Consider a VASS $\hat{\pazocal{A}}_{\mathbf{v}}$ obtained by first modifying $\pazocal{A}$ into $\pazocal{A}_{\mathbf{v}}$ (i.e., for every $c_{i}$ such that $\mathbf{v}_{i}=\infty$ , every counter update vector $\mathbf{u}$ of $\pazocal{A}$ is modified so that $\mathbf{u}_{i}=0$ , see Section 3.2), and then extending $\pazocal{A}_{\mathbf{v}}$ into $\hat{\pazocal{A}}_{\mathbf{v}}$ by the construction of Proposition 3.7. That is, $\hat{\pazocal{A}}_{\mathbf{v}}$ is obtained from $\pazocal{A}_{\mathbf{v}}$ by adding the gadget pumping every counter $c_{i}$ such the $\mathbf{v}_{i}=k<\infty$ to $\Theta(n^{k})$ from an initial configuration where all counters are set to $n$ . Now, the above results are applicable to $\hat{\pazocal{A}}_{\mathbf{v}}$ . That is, for every counter $c_{i}$ such that $\mathbf{v}_{i}\neq\infty$ , there exist

•

a control state $p_{i}\in Q$ ,
•

an infinite family $\tau^{i}_{1},\tau^{i}_{2},\ldots$ of strategies for player Demon in $\hat{\pazocal{A}}_{\mathbf{v}}$ ,
•

a function $S_{i}:\mathbb{N}\rightarrow\mathbb{N}$ such that $S_{i}\in 2^{\pazocal{O}(n)}$ ,

such that for every $n\in\mathbb{N}$ , the value of $c_{i}$ in the configuration reached by applying $\tau^{i}_{n}$ from $p_{i}\vec{n}$ until a maximal computation is obtained or $S_{i}(n)$ transitions are executed, is

•

$\Theta(n^{k})$ if $\pazocal{C}_{\hat{A}_{\mathbf{v}}}[c]\in\Theta(n^{k})$ ,
•

$2^{\Omega(n)}$ if $\pazocal{C}_{\hat{A}_{\mathbf{v}}}[c]\in 2^{\Omega(n)}$ .

By applying the observations of Proposition 3.7, we can safely assume that $p_{i}=\textit{in}$ where in is the distinguished starting state of the pumping gadget, and the above computations never revisit the control state in after passing through the control state out of the gadget. Let $P_{i}(n)$ be the length of the computation from configuration $\textit{in}\thinspace\vec{n}$ under strategy $\tau^{i}_{n}$ until the control state out is reached (and $\infty$ if out is never reached), and let $T_{i}:\mathbb{N}\rightarrow\mathbb{N}$ be such that $T_{i}(n)=\max(0,S_{i}(n)-P_{i}(n)-1)$ . Note that $T_{i}\in 2^{\pazocal{O}(n)}$ .

For every $i\in\{1,\ldots,d\}$ , let $\textit{Gadget}_{i}(n)$ be the maximal value of $c_{i}$ achievable by running the pumping gadget of $\hat{A}_{\mathbf{v}}$ from the control state in where all counters are initialized to $n$ (cf. VASS Program 4). Recall that $\textit{Gadget}_{i}(n)\in\Theta(n^{\mathbf{v}_{i}})$ . Also let $\textit{Gadget}(n)=(\textit{Gadget}_{1}(n),\dots,\textit{Gadget}_{d}(n))$ .

Let $F$ be a $\mathbf{v}$ -consistent function. We define a function $R:\mathbb{N}\rightarrow\mathbb{N}$ such that $R(n)$ is the largest $m$ satisfying the following condition:

•

$\lfloor F_{i}(n)/d\rfloor\geq\textit{Gadget}_{i}(m)+|Q|\cdot M$ for every $i\in\{1,\ldots,d\}$ , where $Q$ are the control states of $\pazocal{A}$ and $M$ is the maximal absolute value of an update vector component of $\pazocal{A}$ ;

Observe that $R\in\Theta(n)$ . For every $n\in\mathbb{N}$ and $i\in\{1,\ldots,d\}$ such that $\mathbf{v}_{i}\neq\infty$ , consider a Demon’s strategy $\varrho^{i}_{n}$ in $\pazocal{A}$ defined as follows: Let $q$ be the control state visited by the strategy $\tau^{i}_{R(n)}$ right after leaving the control state out of the pumping gadget of $\hat{A}_{\mathbf{v}}$ . The strategy $\varrho^{i}_{n}$ takes the shortest path to $q$ and then starts to behave exactly like $\tau^{i}_{R(n)}$ . Note that $\varrho^{i}_{n}$ can faithfully simulate $\tau^{i}_{R(n)}$ either until $\tau^{i}_{R(n)}$ produces a maximal computation (for initial configuration $q\thinspace\textit{Gadget}(R(n))$ ) or for at least $T_{i}(R(n))$ steps, which is sufficient to pump the counter $c_{i}$ to $\Theta(n^{k})$ if $\pazocal{C}_{\mathbf{v}}[c_{i}]\in\Theta(n^{k})$ , or to $2^{\Omega(n)}$ if $\pazocal{C}_{\mathbf{v}}[c_{i}]\in 2^{\Omega(n)}$ . The strategy $\pi_{n}$ is obtained by “concatenating” all $\varrho^{i}_{n}$ (for all counters $c_{i}$ such that $\mathbf{v}_{i}\neq\infty$ ), where $\varrho^{i}_{n}$ is executed either for $T_{i}(R(n))$ steps since initiating the simulation of $\tau^{i}_{R(n)}$ or until $\tau^{i}_{R(n)}$ produces a maximal computation. Note that each simulation of $\tau^{i}_{R(n)}$ "assumes" that the counters are set to $\textit{Gadget}(R(n))$ , and therefore the most any $\varrho^{i}_{n}$ can lower any counter $c_{j}$ is by $\textit{Gadget}_{j}(R(n))+|Q|\cdot M$ . Therefore we can assume that $\pi_{n}$ "splits the counters into $d$ boxes" of size $\lfloor F(n)/d\rfloor$ , and performs each simulation in it’s own box. Hence, no simulation can "undo" the effect of the previous simulations. Also let $S(n)$ be the maximal number of steps $\pi_{n}$ takes until the last simulation $\varrho^{i}_{n}$ is finished from initial configuration $pF(n)$ for any $p\in Q$ . The total length of the whole simulation is bounded by $S(n)\leq\sum_{i,\mathbf{v}_{i}\neq\infty}\left(|Q|+T_{i}(R(n)\right)$ . Observe that $S(n)\in 2^{\pazocal{O}(n)}$ , and for every counter $c_{i}$ such that $\mathbf{v}_{i}=\infty$ we have that the value of $c_{i}$ after performing $\pi_{n}$ in the above indicated way is at least $\lfloor F_{i}(n)/d\rfloor$ , which is $2^{\Omega(n)}$ , since the $i$ -th box "remains untouched".

B.5 An Algorithm Computing $\textit{Vectors}_{\pazocal{A}}$

In this section, we present an algorithm computing the set $\textit{Vectors}_{\pazocal{A}}(\eta)$ for every SCC $\eta$ of $\pazocal{D}{A}$ . Recall that $\textit{Vectors}{A}(\eta)$ consists of all $\mathbf{u}$ such that there is a path $\eta_{1},\ldots,\eta_{m}$ where $\eta_{1}$ is a root of $\pazocal{D}{A}$ , $\eta_{m}=\eta$ , and $\mathbf{u}=\mathbf{v}_{m}$ .

The sets $\textit{Vectors}_{\pazocal{A}}(\eta)$ are computed by Algorithm 5. In particular, at lines 5–5, $\textit{Vectors}{A}(\eta)$ is set to $\pazocal{V}_{\eta}(\vec{1})$ for every root $\eta$ of $\pazocal{D}(\pazocal{A})$ . The algorithm then follows the top-down acyclic structure of $\pazocal{D}(\pazocal{A})$ and computes $\textit{Vectors}{A}(\eta)$ for the remaining components.

input : A Demonic decomposition

\textnormal{{D}}(\pazocal{A})

of a demonic VASS

\pazocal{A}

output : The function

\textit{Vectors}{A}

1 foreach vertex $\mu$ of $\textnormal{{D}}(\pazocal{A})$ do

\textit{Vectors}{A}(\mu):=\emptyset

4 end foreach

\mathit{Aux}:=

the set of all vertices of

\textnormal{{D}}(\pazocal{A})

6 foreach $\eta\in\mathit{Aux}$ where $\eta$ is a root of $\textnormal{{D}}(\pazocal{A})$ do

\textit{Vectors}{A}(\eta):=\{\pazocal{V}_{\eta}(\vec{1})\}

\mathit{Aux}:=\mathit{Aux}\smallsetminus\{\eta\}

10 end foreach

11 while $\mathit{Aux}\neq\emptyset$ do

\eta:=

an element of

\mathit{Aux}

such that

\textit{Pre}(\eta)\cap\mathit{Aux}=\emptyset

\mathit{Aux}:=\mathit{Aux}\smallsetminus\{\eta\}

14 foreach $\mu\in\textit{Pre}(\eta)$ do

15 foreach $\mathbf{v}\in\textit{Vectors}{A}(\mu)$ do

\textit{Vectors}{A}(\eta):=\textit{Vectors}{A}(\eta)\cup\{\pazocal{V}_{\eta}(\mathbf{v})\}

17 end foreach

19 end foreach

21 end while

Algorithm 5 Computing the function

\textit{Vectors}{A}

Appendix C Proofs for Section 4

C.1 $\mathbf{PSPACE}$ lower bounds of Theorem 4.1

In this section, we prove the $\mathbf{PSPACE}$ lower bounds of Theorem 4.1. We use a modified construction of Lemma 3.3 to obtain a reduction from the QBF problem. Intuitively, the only change is that Angel determines the assignment for universally quantified propositional variables. Let us note that in the original construction of [12], Angel also selected the clause to be checked. Here, we use the construction of Lemma 3.3 based on the $\min$ gadgets. Let

\psi\quad\equiv\quad\forall x_{1}\,\exists y_{1}\,\forall x_{2}\ldots\exists y_{v}\ C_{1}\wedge\ldots\wedge C_{m}

be a quantified Boolean formula where each clause $C_{i}$ contains precisely three literals (recall that the (in)validity of a given quantified Boolean formula is a $\mathbf{PSPACE}$ complete problem).

Consider the VASS game $\pazocal{A}_{\psi}$ defined by the VASS Program 6, where $k\geq 2$ is a constant. Note that the only difference between $\pazocal{A}_{\psi}$ and the demonic VASS $\pazocal{A}_{\varphi}$ (cf. the VASS Program 1) is that the valuation for the universally quantified variables is chosen by Angel. Formally, the gadget for D-choose is the same as the one for choose (see (Fig. 3), and the gadget for A-choose is also the same except that the newly added in state of the gadget is angelic. Note that all other states of $\pazocal{A}_{\psi}$ , including the states in gadgets pumping the $x_{i},y_{i}$ counters, are demonic. Using the observations of Lemma 3.3, it is easy to see that

•

if $\psi$ is valid, then $\pazocal{L}_{\pazocal{A}_{\psi}}\in\Theta(n^{k+1})$ and $\pazocal{C}_{\pazocal{A}_{\psi}}[s_{m}]\in\Theta(n^{k})$ ;
•

if $\psi$ is not valid, then $\pazocal{L}_{\pazocal{A}_{\psi}}\in\Theta(n^{k})$ and $\pazocal{C}_{\pazocal{A}_{\psi}}[s_{m}]\in\Theta(n)$ .

From this we immediately obtain the $\mathbf{PSPACE}$ lower bounds of Theorem 4.1.

d_{2}\texttt{\,+=\,}d_{1}*e_{1};\ \ d_{3}\texttt{\,+=\,}d_{2}*e_{2};\ \cdots\ ;\ \ d_{k}\texttt{\,+=\,}d_{k-1}*e_{k-1};

2 foreach $i=1,\ldots,v$ do

3 A-choose:

x_{i}\texttt{\,+=\,}d_{k}

\bar{x}_{i}\texttt{\,+=\,}d_{k};

4 D-choose:

y_{i}\texttt{\,+=\,}d_{k}

\bar{y}_{i}\texttt{\,+=\,}d_{k};

6 end foreach

s_{0}\texttt{\,+=\,}d_{k};

8 foreach $i=1,\ldots,m$ do

9 D-choose:

s_{i}\texttt{\,+=\,}\min(\ell^{i}_{1},s_{i-1})

s_{i}\texttt{\,+=\,}\min(\ell^{i}_{2},s_{i-1})

s_{i}\texttt{\,+=\,}\min(\ell^{i}_{3},s_{i-1});

11 end foreach

f\texttt{\,+=\,}s_{m}*n

VASS Program 6

\pazocal{A}_{\psi}

C.2 A Proof of Proposition 4.4

First, let us restate the proposition.

See 4.4

Convention. For notation simplification, we assume that the counter update vector $\mathbf{u}$ in every transition $(p,\mathbf{u},q)$ where $p$ is angelic satisfies $\mathbf{u}=\vec{0}$ (a transition $(p,\mathbf{u},q)$ where $\mathbf{u}\neq\vec{0}$ can be split into $(p,\vec{0},q^{\prime})$ , $(q^{\prime},\mathbf{u},q)$ where $q^{\prime}$ is a fresh demonic state).

Let us fix a vertex $([p],L)$ of $\pazocal{G}{A}$ , a vector $\mathbf{v}\in\mathbb{N}^{d}_{\infty}$ , and a counter $c_{i}$ such that $\mathbf{v}_{i}\neq\infty$ . First, consider the case when $([p],L)$ is a leaf of $\pazocal{G}{A}$ . Then $([p],L)$ is demonic, and can be seen as a strongly connected demonic VASS. The claim follows trivially by applying Lemma 3.8 to $([p],L)$ and $\mathbf{v}$ .

Now suppose that $([p],L)$ is a demonic vertex of $\pazocal{G}{A}$ with successors $([q_{1}],L),\ldots,([q_{m}],L)$ . Note that $([p],L)$ can be seen as a strongly connected demonic VASS after deleting all transitions from/to the states outside $([p],L)$ . Let $F$ be a $\mathbf{v}$ -consistent function. By applying Lemma 3.8 to $([p],L)$ , the vector $\mathbf{v}$ , and $F$ , we obtain an infinite family of Demon’s strategies $\Pi$ and a function $S\in 2^{\pazocal{O}(n)}$ such that the vector $G(n)$ of counter values in the last configuration of $\beta_{n}[\mathbf{v},p,F,\Pi,S]$ satisfies the following for every $\ell\in\{1,\ldots,d\}$ :

•

$G_{\ell}(n)\in\Theta(n^{k})$ if $\mathbf{v}_{\ell}\neq\infty$ and $\pazocal{C}^{p}_{([p],L)}[c_{\ell},\mathbf{v}]\in\Theta(n^{k})$ ;
•

$G_{\ell}(n)\in 2^{\Omega(n)}$ if $\mathbf{v}_{\ell}=\infty$ or $\pazocal{C}^{p}_{([p],L)}[c_{\ell},\mathbf{v}]\in 2^{\Omega(n)}$ .

Let $\mathbf{u}=\pazocal{V}_{([p],L)}(\mathbf{v})$ , where $\pazocal{V}$ is the function defined in Section 3.2. Note that $G$ is a $\mathbf{u}$ -consistent function. If $\mathbf{u}_{i}=\infty$ , we define $\pi_{\mathbf{v}}$ as the strategy which behaves like the strategy $\pi_{n}$ of $\Pi$ for every computation of $\pazocal{A}_{L}$ initiated in $p\,F(n)$ . Clearly, $\textit{max}[c_{i}](\mathit{Comp}_{\pazocal{A}_{L}}^{\sigma,\pi_{\mathbf{v}}}(p\,F(n)))\in 2^{\Omega(n)}$ for every Angel’s strategy $\sigma$ . If $\mathbf{u}_{i}\neq\infty$ , for every $j\in\{1,\ldots,m\}$ we apply the induction hypothesis to $([q_{j}],L)$ , the vector $\mathbf{u}$ , the counter $c_{i}$ , and the $\mathbf{u}$ -consistent function $G$ . Thus, we obtain that for every $j\in\{1,\ldots,m\}$ one of the following possibilities holds:

•
There exists a $k_{j}\in\mathbb{N}$ , a simple locking Angel’s strategy $\sigma^{j}_{\mathbf{u}}$ in $\pazocal{A}_{L}$ and a Demon’s strategy $\pi^{j}_{\mathbf{u}}$ in $\pazocal{A}_{L}$ such that $\sigma^{j}_{\mathbf{u}}$ is independent of $G$ and
- –
  
  for every Demon’s strategy $\pi$ in $\pazocal{A}_{L}$ , we have $\textit{max}[c_{i}](\mathit{Comp}_{\pazocal{A}_{L}}^{\sigma^{j}_{\mathbf{u}},\pi}(q_{j}\,G(n)))\in\pazocal{O}(n^{k_{j}})$ ;
- –
  
  for every Angel’s strategy $\sigma$ in $\pazocal{A}_{L}$ , we have $\textit{max}[c_{i}](\mathit{Comp}_{\pazocal{A}_{L}}^{\sigma,\pi^{j}_{\mathbf{u}}}(q_{j}\,G(n)))\in\Omega(n^{k_{j}})$ .
•

There is a Demon’s strategy $\pi^{j}_{\mathbf{u}}$ in $\pazocal{A}_{L}$ such that for every Angel’s strategy $\sigma$ in $\pazocal{A}_{L}$ we have that $\textit{max}[c_{i}](\mathit{Comp}_{\pazocal{A}_{L}}^{\sigma,\pi^{j}_{\mathbf{u}}}(q_{j}\,G(n)))\in 2^{\Omega(n)}$ .

We distinguish two cases:

•

There is $j\in\{1,\ldots,m\}$ such that the second possibility holds. Let $\pi_{\mathbf{v}}$ be a Demon’s strategy such that, for an initial configuration $p\,F(n)$ , $\pi_{\mathbf{v}}$ starts by simulating the strategy $\pi_{n}$ of $\Pi$ until a configuration with the $G(n)$ vector of counter values is reached. Then, $\pi_{\mathbf{v}}$ takes the shortest path to a configuration $q_{j}\mathbf{w}$ , and then switches to simulating $\pi^{j}_{\mathbf{u}}$ for the initial configuration $q_{j}G(n^{\prime})$ where $n^{\prime}\in\mathbb{N}$ is the largest number such that $G(n^{\prime})\leq\mathbf{w}$ . The properties of $\pi^{j}_{\mathbf{u}}$ (see above) imply that $\textit{max}[c_{i}](\mathit{Comp}_{\pazocal{A}_{L}}^{\sigma,\pi_{\mathbf{v}}}(p\,F(n)))\in 2^{\Omega(n)}$ for an arbitrary Angel’s strategy $\sigma$ .
•

For all $j\in\{1,\ldots,m\}$ , the first possibility holds. Let $k$ be the maximum of all $k_{j}$ for $j\in\{1,\ldots,m\}$ . Furthermore, let $\sigma_{\mathbf{v}}$ be a simple locking strategy which for a computation initiated in $p\,F(n)$ behaves like the simple locking strategy $\sigma_{\mathbf{u}}^{j}$ when the computation enters a control state of $([q_{j}],L)$ . Note that a computation initiated in $p\,F(n)$ cannot visit an angelic control state before leaving the component $([p],L)$ , and the decisions taken by simple locking strategies may depend on the sequence of previously visited components of $\pazocal{G}{A}$ . Hence, $\sigma_{\mathbf{v}}$ is a simple locking strategy. For every Demon’s strategy $\pi$ , we have that $\textit{max}[c_{i}](\mathit{Comp}_{\pazocal{A}_{L}}^{\sigma_{\mathbf{v}},\pi}(p\,F(n)))\in\pazocal{O}(n^{k})$ by our choice of $k$ and the properties of $\sigma_{\mathbf{u}}^{j}$ strategies (see above). Now consider the Demon’s strategy $\pi_{\mathbf{v}}$ defined in the same way as in the previous case, where $j$ is the index such that $k=k_{j}$ . Then, the properties of $\pi^{j}_{\mathbf{u}}$ imply that $\textit{max}[c_{i}](\mathit{Comp}_{\pazocal{A}_{L}}^{\sigma,\pi_{\mathbf{v}}}(p\,F(n)))\in\Omega(n^{k})$ for an arbitrary Angel’s strategy $\sigma$ .

Finally, suppose that $([p],L)$ is angelic. Then $[p]=\{p\}$ , and let $(p,\vec{0},q_{1}),\ldots,(p,\vec{0},q_{m})$ be the outgoing transitions of $p$ (see the Convention above). For every $j\in\{1,\ldots,m\}$ , let $L_{j}=L\cup\{(p,\vec{0},q_{j})\}$ . Let $F$ be a $\mathbf{v}$ -consistent function. By induction hypothesis, for every $j\in\{1,\ldots,m\}$ , one of the following possibilities holds:

•
there exists a $k_{j}\in\mathbb{N}$ , a simple locking Angel’s strategy $\sigma^{j}_{\mathbf{v}}$ in $\pazocal{A}_{L_{j}}$ and a Demon’s strategy $\pi^{j}_{\mathbf{v}}$ in $\pazocal{A}_{L_{j}}$ such that $\sigma^{j}_{\mathbf{v}}$ is independent of $F$ and
- –
  
  for every Demon’s strategy $\pi^{j}$ in $\pazocal{A}_{L_{j}}$ , we have $\textit{max}[c_{i}](\mathit{Comp}_{\pazocal{A}_{L_{j}}}^{\sigma^{j}_{\mathbf{v}},\pi^{j}}(p\,F(n)))\in\pazocal{O}(n^{k_{j}})$ ;
- –
  
  for every Angel’s strategy $\sigma^{j}$ in $\pazocal{A}_{L_{j}}$ , we have $\textit{max}[c_{i}](\mathit{Comp}_{\pazocal{A}_{L_{j}}}^{\sigma^{j},\pi^{j}_{\mathbf{v}}}(p\,F(n)))\in\Omega(n^{k_{j}})$ .
•

there is a Demon’s strategy $\pi^{j}_{\mathbf{v}}$ in $\pazocal{A}_{L_{j}}$ such that for every Angel’s strategy $\sigma^{j}$ in $\pazocal{A}_{L_{j}}$ we have that $\textit{max}[c_{i}](\mathit{Comp}_{\pazocal{A}_{L_{j}}}^{\sigma^{j},\pi^{j}_{\mathbf{v}}}(p\,F(n)))\in 2^{\Omega(n)}$ .

Strictly speaking, the induction hypothesis applies to the initial configurations $q_{j}\,F(n)$ , but since $p$ is a control state of $A_{L_{j}}$ and $(p,\vec{0},q_{j})$ is the only out-going transition of $p$ in $\pazocal{A}_{L_{j}}$ , the above claim follows immediately.

Let us first assume that there exists $j$ such that the first possibility holds. Then, we fix a $j$ such that $k_{j}$ is minimal, and we put $k=k_{j}$ . Consider a simple locking strategy $\sigma_{\mathbf{v}}$ in $\pazocal{A}_{L}$ which starts by locking the transition $(p,\vec{0},q_{j})$ and then proceeds by simulating the simple locking strategy $\sigma^{j}_{\mathbf{v}}$ . For every Demon’s strategy $\pi$ , we have that $\mathit{Comp}_{\pazocal{A}_{L}}^{\sigma_{\mathbf{v}},\pi}(p\,F(n))$ is the same computation as $\mathit{Comp}_{\pazocal{A}_{L_{j}}}^{\sigma^{j}_{\mathbf{v}},\pi}(p\,F(n))$ . Hence, $\textit{max}[c_{i}](\mathit{Comp}_{\pazocal{A}_{L}}^{\sigma_{\mathbf{v}},\pi}(p\,F(n)))\in\pazocal{O}(n^{k})$ by induction hypothesis.

Now consider a Demon’s strategy $\pi_{\mathbf{v}}$ in $\pazocal{A}_{L}$ defined as follows. Let $q_{1}\mathbf{v}_{1},\ldots,q_{\ell}\mathbf{v}_{\ell}$ be a computation in $\pazocal{A}_{L}$ initiated in a configuration $p\,F(n)$ such that $q_{\ell}$ is demonic. Furthermore, let $\alpha\equiv q_{1}\xrightarrow{\mathbf{u}_{1}}q_{2}\xrightarrow{\mathbf{u}_{2}}\cdots\xrightarrow{\mathbf{u}_{\ell-1}}q_{\ell}$ be the associated path in $\pazocal{A}_{L}$ . The mode of $\alpha$ is the $j$ such that $(p,\vec{0},q_{j})$ is the last outgoing transition of $p$ occurring in $\alpha$ . The $j$ -th projection of $\pi$ , denoted by $\pi_{j}$ , is then obtained by concatenating all subsequences of $\alpha$ initiated by the transition $(p,\vec{0},q_{j})$ and terminated either by the next occurrence of $p$ or by $q_{\ell}$ . Consider the computation $\gamma_{j}$ in $\pazocal{A}_{L_{j}}$ obtained by performing $\pi_{j}$ from the initial configuration $p\,\lfloor F(n)/m\rfloor$ , where $\lfloor F(n)/m\rfloor(i)=\lfloor F_{i}(n)/m\rfloor$ . The transition selected by $\pi_{\mathbf{v}}$ after performing the computation $q_{1}\mathbf{v}_{1},\ldots,q_{\ell}\mathbf{v}_{\ell}$ is the transition selected by $\pi^{j}_{\mathbf{v}}$ , after performing $\gamma_{j}$ . Intuitively, $\pi_{\mathbf{v}}$ “switches” among the strategies $\pi^{1}_{\mathbf{v}},\ldots,\pi^{m}_{\mathbf{v}}$ according to the current mode, and thus simulates computations of $\pazocal{A}_{L_{1}},\ldots,\pazocal{A}_{L_{m}}$ initiated in $p\,\lfloor F(n)/m\rfloor$ . The computation first reaching a terminal configuration is simulated completely. Hence, there exists $j$ such that $\mathit{Comp}_{\pazocal{A}_{L}}^{\sigma,\pi_{\mathbf{v}}}(p\,F(n))$ “subsumes” $\mathit{Comp}_{\pazocal{A}_{L}}^{\sigma^{j},\pi^{j}_{\mathbf{v}}}(p\,\lfloor F(n)/m\rfloor)$ , where $\sigma^{j}$ is the “projection” of $\sigma$ into $\pazocal{A}_{L_{j}}$ . This implies $\textit{max}[c_{i}](\mathit{Comp}_{\pazocal{A}_{L}}^{\sigma,\pi_{\mathbf{v}}}(p\,F(n)))\in\Omega(n^{k})$ by induction hypothesis and our choice of $k$ .

Finally, assume that the second possibility holds for all $j\in\{1,\ldots,m\}$ . Then, we construct a Demon’s strategy $\pi_{\mathbf{v}}$ in the same way as above, and conclude (by the same reasoning) that $\textit{max}[c_{i}](\mathit{Comp}_{\pazocal{A}_{L}}^{\sigma,\pi_{\mathbf{v}}}(p\,F(n)))\in 2^{\Omega(n)}$ for an arbitrary Angel’s strategy $\sigma$ .

Deciding Polynomial Termination Complexity for VASS Programs

Abstract

keywords:

category:

1 Introduction

Example 1.1.

Example 1.2.

2 Preliminaries

Definition 2.1 (VASS).

3 Demonic VASS

Theorem 3.1.

Theorem 3.2.

3.1 Lower bounds

Lemma 3.3.

Proof 3.4.

Lemma 3.5.

Lemma 3.6.

3.2 Upper bounds

Proposition 3.7.

Lemma 3.8.

4 VASS Games

Theorem 4.1.

Definition 4.2.

4.1 Locking sets and the locking decomposition of A\pazocal{A}

Definition 4.3.

4.2 Upper bounds

Proposition 4.4.

Theorem 4.5.

5 Conclusions, future work

References

Appendix A The Existence of Equilibrium Value in VASS Games

Appendix B Proofs for Section 3

B.1 A proof of Lemma 3.5

Proof B.1.

B.2 A proof of Lemma 3.6

Proof B.2.

B.3 A proof of Proposition 3.7

Proposition B.3 (see [19]).

Proof B.4.

B.4 A Proof of Lemma 3.8

B.5 An Algorithm Computing VectorsA\textit{Vectors}_{\pazocal{A}}

Appendix C Proofs for Section 4

C.1 𝐏𝐒𝐏𝐀𝐂𝐄\mathbf{PSPACE} lower bounds of Theorem 4.1

C.2 A Proof of Proposition 4.4

4.1 Locking sets and the locking decomposition of $\pazocal{A}$

B.5 An Algorithm Computing $\textit{Vectors}_{\pazocal{A}}$

C.1 $\mathbf{PSPACE}$ lower bounds of Theorem 4.1