Masaryk University, Czechia and https://www.muni.cz/lide/422654-michal-ajdarow
Masaryk University, Czechia and
https://www.fi.muni.cz/usr/kucera/tony@fi.muni.czhttps://orcid.org/0000-0002-6602-8028
Michal Ajdarów and Antonín Kučera [100]Theory of computation Models of
computation The work is supported by the Czech Science Foundation, Grant No.
21-24711S.Serge Haddad and Daniele Varacca 2 32nd International Conference on
Concurrency Theory (CONCUR 2021) CONCUR 2021 CONCUR 2021 August 23–27, 2021
Virtual Conference 203 24

# 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

###### category:

##  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–; |  $(0,0,0)$$(0,0,0)$$(0,0,0)$$(-1,0,0)$ /* i-- */ $(0,0,0)$$(0,-1,-1)$ // j:=0; Aux:=0 // $(-1,+1,+1)$ // i--; j++; Aux++ //$(+1,0,-1)$ // i++; Aux-- //$(0,-1,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_ 111A 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

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 choose: $x_{i}\texttt{\,+=\,}d_{k}$ or $\bar{x}_{i}\texttt{\,+=\,}d_{k};$

4

5 end foreach

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

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

8 choose: $s_{i}\texttt{\,+=\,}\min(\ell^{i}_{1},s_{i-1})$ or
$s_{i}\texttt{\,+=\,}\min(\ell^{i}_{2},s_{i-1})$ or
$s_{i}\texttt{\,+=\,}\min(\ell^{i}_{3},s_{i-1});$

9

10 end foreach

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

VASS Program 1 $\pazocal{A}_{\varphi}$ inout – $x$ \+ $\alpha$ \+ $z$ \+ $x$ –
$\alpha$ \+ $z$ – $y$$z\texttt{\,+=\,}x*y$inout – $y$ \+ $x$ \+ $\alpha$ \+
$y$ – $\alpha$ $x\texttt{\,+=\,}y$inout – $s_{i-1}$ – $\ell$ \+ $s_{i}$ \+
$\alpha$ \+ $\ell$ – $\alpha$
$s_{i}\texttt{\,+=\,}\min(\ell,s_{i-1})$ininoutinoutout$\textit{ins}_{1}$$\textit{ins}_{2}$$\textit{ins}_{1};\
\textit{ins}_{2}$ininoutinoutout$\textit{ins}_{1}$$\textit{ins}_{j}$$\textbf{choose:
}\textit{ins}_{1};\textbf{ or }\cdots\textbf{ or }\textit{ins}_{j}$ 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.

$(n,n,n)$$(n^{2},n,2^{\Omega(n)})$$(n^{2},n,\infty)$$(n^{2},2^{\Omega(n)},\infty)$$(n^{2},n,\infty)$$(n^{5},n,\infty)$$(n^{5},n,\infty)$$(n^{5},n^{5},\infty)$$(n^{2},\infty,\infty)$$(n^{2},\infty,\infty)$
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 */

3 $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 */

3 $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
*/

4 $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

2 $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);$

7

8 end if

9

10 end foreach

11

12 end foreach

13

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

15 $c_{i}\texttt{\,+=\,}[s_{i}];$ inout– $y$

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

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

3

4 end foreach

5 $\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

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

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

9

10 end foreach

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

12 $\eta:=$ an element of $\mathit{Aux}$ such that
$\textit{Pre}(\eta)\cap\mathit{Aux}=\emptyset$

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

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

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

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

17 end foreach

18

19 end foreach

20

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.

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}$ or $\bar{x}_{i}\texttt{\,+=\,}d_{k};$

4 D-choose: $y_{i}\texttt{\,+=\,}d_{k}$ or $\bar{y}_{i}\texttt{\,+=\,}d_{k};$

5

6 end foreach

7$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})$ or
$s_{i}\texttt{\,+=\,}\min(\ell^{i}_{2},s_{i-1})$ or
$s_{i}\texttt{\,+=\,}\min(\ell^{i}_{3},s_{i-1});$

10

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$.