Masaryk University, Czechia and https://www.muni.cz/lide/422654-michal-
ajdarowxajdarow@fi.muni.czhttps://orcid.org/0000-0003-0694-0944Masaryk
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.2 34th International Conference on Concurrency Theory (CONCUR 2023)
CONCUR 2023 CONCUR 2023 September 18–23, 2023 Antwerp, Belgium

# Asymptotic Complexity Estimates for Probabilistic Programs and their VASS
Abstractions

Michal Ajdarów  Antonín Kučera

###### Abstract

The standard approach to analyzing the asymptotic complexity of probabilistic
programs is based on studying the asymptotic growth of certain expected values
(such as the expected termination time) for increasing input size. We argue
that this approach is not sufficiently robust, especially in situations when
the expectations are infinite. We propose new estimates for the asymptotic
analysis of probabilistic programs with non-deterministic choice that overcome
this deficiency. Furthermore, we show how to efficiently compute/analyze these
estimates for selected classes of programs represented as Markov decision
processes over vector addition systems with states.

###### keywords:

Probabilistic programs, asymptotic complexity, vector addition systems

###### category:

##  1 Introduction

Vector Addition Systems with States (VASS) [10] are a model for discrete
systems with multiple unbounded resources expressively equivalent to Petri
nets [19]. Intuitively, a VASS with $d\geq 1$ counters is a finite directed
graph where the transitions are labeled by $d$-dimensional vectors of integers
representing _counter updates_. A computation starts in some state for some
initial vector of non-negative counter values and proceeds by selecting
transitions non-deterministically and performing the associated counter
updates. Since the counters cannot assume negative values, transitions that
would decrease some counter below zero are disabled.

In program analysis, VASS are used as abstractions for programs operating over
unbounded integer variables. Input parameters are represented by initial
counter values, and more complicated arithmetical functions, such as
multiplication, are modeled by VASS gadgets computing these functions in a
weak sense (see, e.g., [16]). Branching constructs, such as if-then-else, are
usually replaced with non-deterministic choice. VASS are particularly useful
for evaluating the _asymptotic complexity_ of infinite-state programs, i.e.,
the dependency of the running time (and other complexity measures) on the size
of the program input [21, 22]. Traditional VASS decision problems such as
reachability, liveness, or boundedness are computationally hard [8, 17, 18],
and other verification problems such as equivalence-checking [11] or model-
checking [9] are even undecidable. In contrast to this, decision problems
related to the asymptotic growth of VASS complexity measures are solvable with
low complexity and sometimes even in _polynomial time_ [3, 23, 14, 15, 1]; see
[13] for a recent overview.

The existing results about VASS asymptotic analysis are applicable to programs
with non-determinism (in _demonic_ or _angelic_ form, see [4]), but cannot be
used to analyze the complexity of _probabilistic programs_. This motivates the
study of Markov decision process over VASS (VASS MDPs) with both non-
deterministic and probabilistic states, where transitions in probabilistic
states are selected according to fixed probability distributions. Here, the
problems of asymptotic complexity analysis become even more challenging
because VASS MDPs subsume infinite-state stochastic models that are
notoriously hard to analyze. So far, the only existing result about asymptotic
VASS MDP analysis is [2] where the linearity of expected termination time is
shown decidable in polynomial time for VASS MDPs with DAG-like MEC
decomposition.

Our Contribution: We study the problems of asymptotic complexity analysis for
probabilistic programs and their VASS abstractions.

For non-deterministic programs, termination complexity is a function
$\pazocal{L}_{\max}$ assigning to every $n\in\mathbb{N}$ the length of the
longest computation initiated in a configuration with each counter set to $n$.
A natural way of generalizing this concept to probabilistic programs is to
define a function $\pazocal{L}_{\mathrm{exp}}$ such that
$\pazocal{L}_{\mathrm{exp}}(n)$ is the maximal _expected length_ of a
computation initiated in a configuration of size $n$, where the maximum is
taken over all strategies resolving non-determinism. The same approach is
applicable to other complexity measures. We show that this natural idea is
generally _inappropriate_ , especially in situations when
$\pazocal{L}_{\mathrm{exp}}(n)$ is _infinite_ for a sufficiently large $n$. By
“inappropriate” we mean that this form of asymptotic analysis can be
misleading. For example, if $\pazocal{L}_{\mathrm{exp}}(n)=\infty$ for all
$n\geq 1$, one may conclude that the computation takes a very long time
independently of $n$. However, this is not necessarily the case, as
demonstrated in a simple example of Fig. 1 (we refer to Section 3 for a
detailed discussion). Therefore, we propose new notions of _lower/upper/tight
complexity estimates_ and demonstrate their advantages over the expected
values. These notions can be adapted to other models of probabilistic
programs, and constitute the main conceptual contribution of our work.

Then, we concentrate on algorithmic properties of the complexity estimates in
the setting of VASS MDPs. Our first result concerns _counter complexity_. We
show that for every VASS MDP with DAG-like MEC decomposition and every counter
$c$, there are only two possibilities:

  * •

The function $n$ is a _tight estimate_ of the asymptotic growth of the maximal
$c$-counter value assumed along a computation initiated in a configuration of
size $n$.

  * •

The function $n^{2}$ is a _lower estimate_ of the asymptotic growth of the
maximal $c$-counter value assumed along a computation initiated in a
configuration of size $n$.

Furthermore, it is decidable in _polynomial time_ which of these alternatives
holds.

Since the termination and transition complexities can be easily encoded as the
counter complexity for a fresh “step counter”, the above result immediately
extends also to these complexities. To some extent, this result can be seen as
a generalization of the result about termination complexity presented in [2].
See Section 4 for more details.

Our next result is a full classification of asymptotic complexity for one-
dimensional VASS MDPs. We show that for every one-dimensional VASS MDP

  * •

the counter complexity is either unbounded or $n$ is a tight estimate;

  * •

termination complexity is either unbounded or one of the functions $n$,
$n^{2}$ is a tight estimate.

  * •

transition complexity is either unbounded, or bounded by a constant, or one of
the functions $n$, $n^{2}$ is a tight estimate.

Furthermore, it is decidable in _polynomial time_ which of the above cases
hold.

Since the complexity of the considered problems remains low, the results are
encouraging. On the other hand, they require non-trivial insights, indicating
that establishing a full and effective classification of the asymptotic
complexity of multi-dimensional VASS MDPs is a challenging problem.

##  2 Preliminaries

We use $\mathbb{N}$, $\mathbb{Z}$, $\mathbb{Q}$, and $\mathbb{R}$ to denote
the sets of non-negative integers, integers, rational numbers, and real
numbers. Given a function $f\colon\mathbb{N}\rightarrow\mathbb{N}$, we use
$O(f)$ and $\Omega(f)$ to denote the sets of all
$g\colon\mathbb{N}\rightarrow\mathbb{N}$ such that $g(n)\leq a\cdot f(n)$ and
$g(n)\geq b\cdot f(n)$ for all sufficiently large $n\in\mathbb{N}$, where
$a,b$ are some positive constants. If $h\in O(f)$ and $h\in\Omega(f)$, we
write $h\in\Theta(f)$.

Let $A$ be a finite index set. The vectors of $\mathbb{R}^{A}$ are denoted by
bold letters such as $\mathbf{u},\mathbf{v},\mathbf{z},\ldots$. The component
of $\mathbf{v}$ of index $i\in A$ is denoted by $\mathbf{v}(i)$. If the index
set is of the form $A=\\{1,2,\dots,d\\}$ for some positive integer $d$, we
write $\mathbb{R}^{d}$ instead of $\mathbb{R}^{A}$. For every
$n\in\mathbb{N}$, we use $\mathbf{n}$ to denote the constant vector where all
components are equal to $n$. The other standard operations and relations on
$\mathbb{R}$ such as $+$, $\leq$, or $<$ are extended to $\mathbb{R}^{d}$ in
the component-wise way. In particular, $\mathbf{v}<\mathbf{u}$ if
$\mathbf{v}(i)<\mathbf{u}(i)$ for every index $i$.

A _probability distribution_ over a finite set $A$ is a vector
$\nu\in[0,1]^{A}$ such that $\sum_{a\in A}\nu(a)=1$. We say that $\nu$ is
_rational_ if every $\nu(a)$ is rational, and Dirac if $\nu(a)=1$ for some
$a\in A$.

###  2.1 VASS Markov Decision Processes

######  Definition 2.1.

Let $d\geq 1$. A _$d$ -dimensional VASS MDP_ is a tuple
$\pazocal{A}=\left(Q,(Q_{n},Q_{p}),T,P\right)$, where

  * •

$Q\neq\emptyset$ is a finite set of _states_ split into two disjoint subsets
$Q_{n}$ and $Q_{p}$ of _nondeterministic_ and _probabilistic_ states,

  * •

$T\subseteq Q\times\mathbb{Z}^{d}\times Q$ is a finite set of _transitions_
such that, for every $p\in Q$, the set $\mathit{Out}(p)\subseteq T$ of all
transitions of the form $(p,\mathbf{u},q)$ is non-empty.

  * •

$P$ is a function assigning to each $t\in\mathit{Out}(p)$ where $p\in Q_{p}$ a
positive rational probability so that $\sum_{t\in T(p)}P(t)=1$.

The encoding size of $\pazocal{A}$ is denoted by $|\\!|\pazocal{A}|\\!|$,
where the integers representing counter updates are written in binary and
probability values are written as fractions of binary numbers. For every $p\in
Q$, we use $\mathit{In}(p)\subseteq T$ to denote the set of all transitions of
the form $(q,\mathbf{u},p)$. The update vector $\mathbf{u}$ of a transition
$t=(p,\mathbf{u},q)$ is also denoted by $\mathbf{u}_{t}$.

A _finite path_ in $\pazocal{A}$ of length $n\geq 0$ is a finite sequence of
the form
$p_{0},\mathbf{u}_{1},p_{1},\mathbf{u}_{2},\ldots,\mathbf{u}_{n},p_{n}$ where
$(p_{i},\mathbf{u}_{i+1},p_{i+1})\in T$ for all $i<n$. We use
$\mathit{len}(\alpha)$ to denote the length of $\alpha$. If there is a finite
path from $p$ to $q$, we say that $q$ is _reachable_ from $p$. An _infinite
path_ in $\pazocal{A}$ is an infinite sequence
$\pi=p_{0},\mathbf{u}_{1},p_{1},\mathbf{u}_{2},\ldots$ such that every finite
prefix of $\pi$ ending in a state is a finite path in $\pazocal{A}$.

A _strategy_ is a function $\sigma$ assigning to every finite path
$p_{0},\mathbf{u}_{1},\ldots,p_{n}$ such that $p_{n}\in Q_{n}$ a probability
distribution over $\mathit{Out}(p_{n})$. A strategy is _Markovian (M)_ if it
depends only on the last state $p_{n}$, and _deterministic (D)_ if it always
returns a Dirac distribution. The set of all strategies is denoted by
$\Sigma_{\pazocal{A}}$, or just $\Sigma$ when $\pazocal{A}$ is understood.
Every initial state $p\in Q$ and every strategy $\sigma$ determine the
probability space over infinite paths initiated in $p$ in the standard way. We
use to denote the associated probability measure.

A _configuration_ of $\pazocal{A}$ is a pair $p\mathbf{v}$, where $p\in Q$ and
$\mathbf{v}\in\mathbb{Z}^{d}$. If some component of $\mathbf{v}$ is negative,
then $p\mathbf{v}$ is _terminal_. The set of all configurations of
$\pazocal{A}$ is denoted by $\mathit{C}(\pazocal{A})$.

Every infinite path $p_{0},\mathbf{u}_{1},p_{1},\mathbf{u}_{2},\ldots$ and
every initial vector $\mathbf{v}\in\mathbb{Z}^{d}$ determine the corresponding
_computation_ of $\pazocal{V}$, i.e., the sequence of configurations
$p_{0}\mathbf{v}_{0},p_{1}\mathbf{v}_{1},p_{2}\mathbf{v}_{2},\ldots$ such that
$\mathbf{v}_{0}=\mathbf{v}$ and
$\mathbf{v}_{i+1}=\mathbf{v}_{i}+\mathbf{u}_{i+1}$. Let $\mathit{Term}(\pi)$
be the least $j$ such that $p_{j}\mathbf{v}_{j}$ is terminal. If there is no
such $j$, we put $\mathit{Term}(\pi)=\infty$ .

Note that every computation uniquely determines its underlying infinite path.
We define the probability space over all computations initiated in a given
$p\mathbf{v}$, where the underlying probability measure is obtained from in an
obvious way. For a measurable function $X$ over computations, we use
$\mathbb{E}^{\sigma}_{p\mathbf{v}}[X]$ to denote the expected value of $X$.

##  3 Asymptotic Complexity Measures for VASS MDPs

In this section, we introduce asymptotic complexity estimates applicable to
probabilistic programs with non-determinism and their abstract models (such as
VASS MDPs). We also explain their relationship to the standard measures based
on the expected values of relevant random variables.

input $N$
---
repeat
| random choice:
|  | $0.5:\ \ N:=N+1;$
|  | $0.5:\ \ N:=N-1;$
until $N=0$

$p$$\pazocal{A}$$0.5,+1$$0.5,-1$

Figure 1: A probabilistic program with infinite expected running time for
every $N\geq 1$, and its $1$-dimensional VASS MDP model $\pazocal{A}$.

Let us start with a simple motivating example. Consider the simple
probabilistic program of Fig. 1. The program inputs a positive integer $N$ and
then repeatedly increments/decrements $N$ with probability $0.5$ until $N=0$.
One can easily show that for every $N\geq 1$, the program terminates with
probability one, and the expected termination time is _infinite_. Based on
this, one may conclude that the execution takes a very long time,
independently of the initial value of $N$. However, this conclusion is _not_
consistent with practical experience gained from trial runs111For $N=1$, about
$95\%$ of trial runs terminate after at most $1000$ iterations of the repeat-
until loop. For $N=10$, only about $75\%$ of all runs terminate after at most
$1000$ iterations, but about $90\%$ of them terminate after at most $10000$
iterations.. The program tends to terminate “relatively quickly” for small
$N$, and the termination time _does_ depend on $N$. Hence, the function
assigning $\infty$ to every $N\geq 1$ is _not_ a faithful characterization of
the asymptotic growth of termination time. We propose an alternative
characterization based on the following observations222Formal proofs of these
observations are simple; in Section 5, we give a full classification of the
asymptotic behaviour of one-dimensional VASS MDPs subsuming the trivial
example of Fig. 1.:

  * •

For every $\varepsilon>0$, the probability of all runs terminating after more
than $n^{2+\varepsilon}$ steps (where $n$ is the initial value of $N$)
approaches _zero_ as $n\to\infty$.

  * •

For every $\varepsilon>0$, the probability of all runs terminating after more
than $n^{2-\varepsilon}$ steps (where $n$ is the initial value of $N$)
approaches _one_ as $n\to\infty$.

Since the execution time is “squeezed” between $n^{2-\varepsilon}$ and
$n^{2+\varepsilon}$ for an arbitrarily small $\varepsilon>0$ as $n\to\infty$,
it can be characterized as “asymptotically quadratic”. This analysis is in
accordance with experimental outcomes.

###  3.1 Complexity of VASS Runs

We recall the complexity measures for VASS runs used in previous works [3, 23,
14, 15, 1]. These functions can be seen as variants of the standard time/space
complexities for Turing machines.

Let $\pazocal{A}=\left(Q,(Q_{n},Q_{p}),T,P\right)$ be a $d$-dimensional VASS
MDP, $c\in\\{1,\ldots,d\\}$, and $t\in T$. For every computation
$\pi=p_{0}\mathbf{v}_{0},p_{1}\mathbf{v}_{1},p_{2}\mathbf{v}_{2},\ldots$, we
put

$\displaystyle\pazocal{L}(\pi)$ $\displaystyle=$
$\displaystyle\mathit{Term}(\pi)$ $\displaystyle\pazocal{C}[c](\pi)$
$\displaystyle=$ $\displaystyle\sup\\{\mathbf{v}_{i}(c)\mid 0\leq
i<\mathit{Term}(\pi)\\}$ $\displaystyle\pazocal{T}[t](\pi)$ $\displaystyle=$
the total number of all $0\leq i<\mathit{Term}(\pi)$ such that
$(p_{i},\mathbf{v}_{i{+}1}{-}\mathbf{v}_{i},p_{i+1})=t$

We refer to the functions $\pazocal{L}$, $\pazocal{C}[c]$, and
$\pazocal{T}[t]$ as _termination_ , _$c$ -counter_, and _$t$ -transition
complexity_, respectively.

Let $\pazocal{F}$ be one of the complexity functions defined above. In VASS
abstractions of computer programs, the input is represented by initial counter
values, and the input size corresponds to the maximal initial counter value.
The existing works on _non-probabilistic_ VASS concentrate on analyzing the
asymptotic growth of the functions
$\pazocal{F}_{\max}:\mathbb{N}\to\mathbb{N}_{\infty}$ where

$\displaystyle\pazocal{F}_{\max}(n)$ $\displaystyle=$
$\displaystyle\max\\{\pazocal{F}(\pi)\mid\pi\mbox{ is a computation initiated
in $p\mathbf{n}$ where $p\in Q$}\\}$

For VASS MDP, we can generalize $\pazocal{F}_{\max}$ into
$\pazocal{F}_{\mathrm{exp}}$ as follows:

$\displaystyle\pazocal{F}_{\mathrm{exp}}(n)$ $\displaystyle=$
$\displaystyle\max\\{\mathbb{E}_{p\mathbf{n}}^{\sigma}[\pazocal{F}]\mid\sigma\in\Sigma_{\pazocal{A}},p\in
Q\\}$

Note that for non-probabilistic VASS, the values of $\pazocal{F}_{\max}(n)$
and $\pazocal{F}_{\mathrm{exp}}(n)$ are the same. However, the function
$\pazocal{F}_{\mathrm{exp}}$ suffers from the deficiency illustrated in the
motivating example at the beginning of Section 3. To see this, consider the
one-dimensional VASS MDP $\pazocal{A}$ modeling the simple probabilistic
program (see Fig. 1). For every $n\geq 1$ and the only (trivial) strategy
$\sigma$, we have that and $\pazocal{L}_{\mathrm{exp}}(n)=\infty$. However,
the practical experience with trial runs of $\pazocal{A}$ is the same as with
the original probabilistic program (see above).

###  3.2 Asymptotic Complexity Estimates

In this section, we introduce asymptotic complexity estimates allowing for a
precise analysis of the asymptotic growth of the termination, $c$-counter, and
$t$-transition complexity, especially when their expected values are infinite
for a sufficiently large input. For the sake of readability, we first present
a simplified variant applicable to _strongly connected_ VASS MDPs.

Let $\pazocal{F}$ be one of the complexity functions for VASS computations
defined in Section 3.1, and let $f:\mathbb{N}\to\mathbb{N}$. We say that $f$
is a _tight estimate of $\pazocal{F}$_ if, for arbitrarily small
$\varepsilon>0$, the value of $\pazocal{F}(n)$ is “squeezed” between
$f^{1-\varepsilon}(n)$ and $f^{1+\varepsilon}(n)$ as $n\to\infty$. More
precisely, for every $\varepsilon>0$,

  * •

there exist $p\in Q$ and strategies $\sigma_{1},\sigma_{2},\ldots$ such that
$\liminf_{n\to\infty}\ $;

  * •

for all $p\in Q$ and strategies $\sigma_{1},\sigma_{2},\ldots$ we have that
$\limsup_{n\to\infty}\ $.

The above definition is adequate for strongly connected VASS MDPs because
tight estimates tend to exist in this subclass. Despite some effort, we have
not managed to construct an example of a strongly connected VASS MDP where an
$\pazocal{F}$ with some upper polynomial estimate does _not_ have a tight
estimate (see Conjecture 3.2). However, if the underlying graph of
$\pazocal{A}$ is _not_ strongly connected, then the asymptotic growth of
$\pazocal{F}$ can differ for computations visiting a different sequence of
maximal end components (MECs) of $\pazocal{A}$, and the asymptotic growth of
$\pazocal{F}$ can be “squeezed” between $f^{1-\varepsilon}(n)$ and
$f^{1+\varepsilon}(n)$ only for the subset of computations visiting the same
sequence of MECs. This explains why we need a more general definition of
complexity estimates presented below.

An _end component (EC)_ of $\pazocal{A}$ is a pair $(C,L)$ where $C\subseteq
Q$ and $L\subseteq T$ such that the following conditions are satisfied:

  * •

$C\neq\emptyset$;

  * •

if $p\in C\cap Q_{n}$, then at least one outgoing transition of $p$ belongs to
$L$;

  * •

if $p\in C\cap Q_{p}$, then all outgoing transitions of $p$ belong to $L$;

  * •

if $(p,\mathbf{u},q)\in L$, then $p,q\in C$;

  * •

for all $p,q\in C$ we have that $q$ is reachable from $p$ and vice versa.

Note that if $(C,L)$ and $(C^{\prime},L^{\prime})$ are ECs such that $C\cap
C^{\prime}\neq\emptyset$, then $(C\cup C^{\prime},L\cup L^{\prime})$ is also
an EC. Hence, every $p\in Q$ either belongs to a unique _maximal end
component_ (MEC), or does not belong to any EC. Also observe that each MEC can
be seen as a strongly connected VASS MDP. We say that $\pazocal{A}$ has _DAG-
like MEC decomposition_ if for every pair $M,M^{\prime}$ of different MECs
such that the states of $M^{\prime}$ are reachable from the states of $M$ we
have that the states of $M$ are not reachable from the states of $M^{\prime}$.

For every infinite path $\pi$ of $\pazocal{A}$, let $\mathit{mecs}(\pi)$ be
the unique sequence of MECs visited by $\pi$. Observe that
$\mathit{mecs}(\pi)$ disregards the states that do not belong to any EC;
intuitively, this is because the transitions executed in such states do not
influence the asymptotic growth of $\pazocal{F}$. Observe that the length of
$\mathit{mecs}(\pi)$, denoted by $\mathit{len}(\mathit{mecs}(\pi))$, can be
finite or infinite. The first possibility corresponds to the situation when an
infinite suffix of $\pi$ stays within the same MEC. Furthermore, for all
$\sigma\in\Sigma$ and $p\in Q$, we have that , and the probability decays
exponentially in $k$ (these folklore results are easy to prove). All of these
notions are lifted to computations in an obvious way.

Observe that if a strategy $\sigma$ aims at maximizing the growth of
$\pazocal{F}$, we can safely assume that $\sigma$ eventually stays in a
_bottom_ MEC that cannot be exited (intuitively, $\sigma$ can always move from
a non-bottom MEC to a bottom MEC by executing a few extra transitions that do
not influence the asymptotic growth of $\pazocal{F}$, and the bottom MEC may
allow increasing $\pazocal{F}$ even further). On the other hand, the maximal
asymptotic growth of $\pazocal{F}$ may be achievable along some “minimal”
sequence of MECs, and this information is certainly relevant for understanding
the behaviour of a given probabilistic program. This leads to the following
definition:

######  Definition 3.1.

A _type_ is a finite sequence $\beta$ of MECs such that
$\mathit{mecs}(\pi)=\beta$ for some infinite path $\pi$.

We say that $f$ is a _lower estimate of $\pazocal{F}$ for a type $\beta$_ if
for every $\varepsilon>0$ there exist $p\in Q$ and a sequence of strategies
$\sigma_{1},\sigma_{2},\ldots$ such that for all $n\geq 1$ and

$\liminf_{n\to\infty}\ $

Similarly, we say that $f$ is an _upper estimate of $\pazocal{F}$ for a type
$\beta$_ if for every $\varepsilon>0$, every $p\in Q$, and every sequence of
strategies $\sigma_{1},\sigma_{2},\ldots$ such that for all $n\geq 1$ we have
that

$\limsup_{n\to\infty}\ $

If there is no upper estimate of $\pazocal{F}$ for a type $\beta$, we say that
$\pazocal{F}$ is _unbounded for $\beta$_. Finally, we say that $f$ is a _tight
estimate of $\pazocal{F}$ for $\beta$_ if it is both a lower estimate and an
upper estimate of $\pazocal{F}$ for $\beta$.

Let us note that in the subclass of _non-probabilistic_ VASS, MECs become
strongly connected components (SCCs), and types correspond to paths in the
directed acyclic graph of SCCs. Each such path determines the corresponding
asymptotic increase of $\pazocal{F}$, as demonstrated in [1]. We conjecture
that types play a similar role for VASS MDPs. More precisely, we conjecture
the following:

######  Conjecture 3.2.

If some polynomial is an upper estimate of $\pazocal{F}$ for $\beta$, then
there exists a tight estimate $f$ of $\pazocal{F}$ for $\beta$.

Even if Conjecture 3.2 is proven wrong, there are interesting subclasses of
VASS MDPs where it holds, as demonstrated in subsequent sections.

$q$$\frac{1}{2},(-1,+1,0,)$$\frac{1}{2},(+1,+1,0,)$$\vec{0}$$\vec{0}$$\vec{0}$$\frac{1}{2},\vec{0}$$\frac{1}{2},\vec{0}$$(0,-1,0)$$(0,-1,+1)$$\frac{1}{2},(0,-1,+1)$$\frac{1}{2},(0,+1,+1)$$M_{1}$$M_{3}$$M_{2}$$M_{4}$
Figure 2: A VASS MDP $\pazocal{A}$ with four MECs and seven types.

For every pair of MECs $M,M^{\prime}$, let $P(M,M^{\prime})$ be the maximal
probability (achievable by some strategy) of reaching a state of $M^{\prime}$
from a state of $M$ in $\pazocal{A}$ without passing through a state of some
other MEC $M^{\prime\prime}$. Note that $P(M,M^{\prime})$ is efficiently
computable by standard methods for finite-state MDPs. The _weight_ of a given
type $\beta=M_{1},\ldots,M_{k}$ is defined as
$\mathit{weight}(\beta)=\prod_{i=1}^{k-1}P(M_{i},M_{i+1})$. Intuitively,
$\mathit{weight}(\beta)$ corresponds to the maximal probability of “enforcing”
the asymptotic growth of $\pazocal{F}$ according to the tight estimate $f$ of
$\pazocal{F}$ for $\beta$ achievable by some strategy.

Generally, higher asymptotic growth of $\pazocal{F}$ may be achievable for
types with smaller weights. Consider the following example to understand
better the types, their weights, and the associated tight estimates.

######  Example 3.3.

Let $\pazocal{A}$ be the VASS MDP of Fig. 2. There are four MECs
$M_{1},M_{2},M_{3},M_{4}$ where $M_{2},M_{3},M_{4}$ are bottom MECs. Hence,
there are four types of length one and three types of length two. Let us
examine the types of length two initiated in $M_{1}$ for
$\pazocal{F}\equiv\pazocal{C}[c]$ where $c$ is the third counter.

Note that in $M_{1}$, the first counter is repeatedly incremented/decremented
with the same probability $\frac{1}{2}$. The second counter “counts” these
transitions and thus it is “pumped” to a _quadratic_ value (cf. the VASS MDP
of Fig. 1). Then, a strategy may decide to move to $M_{2}$, where the value of
the second counter is transferred to the third counter. Hence, $n^{2}$ is the
tight estimate of $\pazocal{C}[c]$ for the type $M_{1},M_{2}$, and
$\mathit{weight}(M_{1},M_{2})=1$. Alternatively, a strategy may decide to move
to the probabilistic state $q$. Then, either $M_{3}$ or $M_{4}$ is entered
with the same probability $\frac{1}{2}$, which implies
$\mathit{weight}(M_{1},M_{3})=\mathit{weight}(M_{1},M_{4})=\frac{1}{2}$. In
$M_{3}$, the third counter is unchanged, and hence $n$ is the tight estimate
of $\pazocal{C}[c]$ for the type $M_{1},M_{3}$. However, in $M_{4}$, the
second counter previously pumped to a quadratic value is repeatedly
incremented/decremented with the same probability $\frac{1}{2}$, and the third
counter “counts” these transitions. This means that $n^{4}$ is a tight
estimate of $\pazocal{C}[c]$ for the type $M_{1},M_{4}$.

This analysis provides detailed information about the asymptotic growth of
$\pazocal{C}[c]$ in $\pazocal{A}$. Every type shows “how” the growth specified
by the corresponding tight estimate is achievable, and its weight corresponds
to the “maximal achievable probability of this growth”. This information is
completely lost when analyzing the maximal expected value of $\pazocal{C}[c]$
for computations initiated in configurations $p\mathbf{n}$ where $p$ is a
state of $M_{1}$, because these expectations are _infinite_ for all $n\geq 1$.

Finally, let us clarify the relationship between the lower/upper estimates of
$\pazocal{F}$ and the asymptotic growth of $\pazocal{F}_{\mathrm{exp}}$. The
following observation is easy to prove.

If $\pazocal{F}_{\mathrm{exp}}\in O(f)$ where $f:\mathbb{N}\to\mathbb{N}$ is
an unbounded function, then $f$ is an upper estimate of $\pazocal{F}$ for
every type. Furthermore, if $f:\mathbb{N}\to\mathbb{N}$ is a lower estimate of
$\pazocal{F}$ for some type, then
$\pazocal{F}_{\mathrm{exp}}\in\Omega(f^{1-\epsilon})$ for each $\epsilon>0$.
However, if $\pazocal{F}_{\mathrm{exp}}\in\Omega(f)$ where
$f:\mathbb{N}\to\mathbb{N}$, then $f$ is _not_ necessarily a lower estimate of
$\pazocal{F}$ for some type.

Observation 3.2 shows that complexity estimates are generally more informative
than the asymptotics of $\pazocal{F}_{\mathrm{exp}}$ even if
$\pazocal{F}_{\mathrm{exp}}\in\Theta(f)$ for some “reasonable” function $f$.
For example, it may happen that there are only two types $\beta_{1}$ and
$\beta_{2}$ where $n$ and $n^{3}$ are tight estimates of $\pazocal{L}$ for
$\beta_{1}$ and $\beta_{2}$ with weights $0.99$ and $0.01$, respectively. In
this case, $\pazocal{L}_{\mathrm{exp}}\in\Theta(n^{3})$, although the
termination time is linear for $99\%$ of computations.

##  4 A Dichotomy between Linear and Quadratic Estimates

In this section, we prove the following result:

######  Theorem 4.1.

Let $\pazocal{A}$ be a VASS MDP with DAG-like MEC decomposition and
$\pazocal{F}$ one of the complexity functions $\pazocal{L}$, $\pazocal{C}[c]$,
or $\pazocal{T}[t]$. For every type $\beta$, we have that either $n$ is a
tight estimate of $\pazocal{F}$ for $\beta$, or $n^{2}$ is a lower estimate of
$\pazocal{F}$ for $\beta$. It is decidable in polynomial time which of the two
cases holds.

Theorem 4.1 can be seen as a generalization of the linear/quadratic dichotomy
results previously achieved for non-deterministic VASS [3] and for the
termination complexity in VASS MDPs [2].

It suffices to prove Theorem 4.1 for the _counter complexity_. The
corresponding results for the termination and transition complexities then
follow as simple consequences. To see this, observe that we can extend a given
VASS MDP with a fresh “step counter” $sc$ that is incremented by every
transition (in the case of $\pazocal{L}$) or the transition $t$ (in the case
of $\pazocal{T}[t]$) and thus “emulate” $\pazocal{L}$ and $\pazocal{T}[t]$ as
$\pazocal{C}[sc]$.

We first consider the case when $\pazocal{A}$ is strongly connected and then
generalize the obtained results to VASS MDPs with DAG-like MEC decomposition.
So, let $\pazocal{A}$ be a strongly connected $d$-dimensional VASS MDP and $c$
a counter of $\pazocal{A}$. The starting point of our analysis is the dual
constraint system designed in [23] for non-probabilistic strongly connected
VASS. We generalize this system to strongly connected VASS MDPs in the way
shown in Figure 3 (the original system of [23] can be recovered by
disregarding the probabilistic states).

Constraint system (I): Find $\mathbf{x}\in\mathbb{Z}^{T}$ such that
$\displaystyle\sum_{t\in T}\mathbf{x}(t)\mathbf{u}_{t}$
$\displaystyle\geq\vec{0}$ $\displaystyle\mathbf{x}$
$\displaystyle\geq\vec{0}$ and for each $p\in Q$
$\displaystyle\sum_{t\in\mathit{Out}(p)}\mathbf{x}(t)$
$\displaystyle=\sum_{t\in\mathit{In}(p)}\mathbf{x}(t)$ and for all $p\in
Q_{p}$, $t\in\mathit{Out}(p)$ $\displaystyle\mathbf{x}(t)$
$\displaystyle=P(t)\cdot\sum_{t^{\prime}\in\mathit{Out}(p)}\mathbf{x}(t^{\prime})$
Objective: _Maximize_
• the number of valid inequalities of the form $\sum_{t\in T}\mathbf{x}(t)\mathbf{u}_{t}(c)>0,$ • the number of valid inequalities of the form $\mathbf{x}(t)>0$. |  Constraint system (II): Find $\mathbf{y}\in\mathbb{Z}^{d},\mathbf{z}\in\mathbb{Z}^{Q}$ such that $\displaystyle\mathbf{y}$ $\displaystyle\geq\vec{0}$ $\displaystyle\mathbf{z}$ $\displaystyle\geq\vec{0}$ and for each $(p,\mathbf{u},q)\in T$ where $p\in Q_{n}$ $\mathbf{z}(q)-\mathbf{z}(p)+\sum_{i=1}^{d}\mathbf{u}(i)\mathbf{y}(i)\leq 0$ and for each $p\in Q_{p}$ $\sum_{t=(p,\mathbf{u},q)\in\mathit{Out}(p)}P(t)\big{(}\mathbf{z}(q)-\mathbf{z}(p)+\sum_{i=1}^{d}\mathbf{u}_{t}(i)\mathbf{y}(i)\big{)}\leq 0$ Objective: _Maximize_ • the number of valid inequalities of the form $\mathbf{y}(c)>0$, • the number of transitions $t=(p,\mathbf{u},q)$ such that $p\in Q_{n}$ and $\mathbf{z}(q)-\mathbf{z}(p)+\sum_{i=1}^{d}\mathbf{u}(i)\mathbf{y}(i)<0,$ • the number of states $p\in Q_{p}$ such that $\sum_{t=(p,\mathbf{u},q)\in\mathit{Out}(p)}P(t)\big{(}\mathbf{z}(q)-\mathbf{z}(p)+\sum_{i=1}^{d}\mathbf{u}(i)\mathbf{y}(i)\big{)}<0\,.$
---|---
Figure 3: Constraint systems for strongly connected VASS MDPs.

Note that solutions of both (I) and (II) are closed under addition. Therefore,
both (I) and (II) have solutions maximizing the specified objectives,
computable in polynomial time. For clarity, let us first discuss an intuitive
interpretation of these solutions, starting with simplified variants obtained
for non-probabilistic VASS in [23].

In the non-probabilistic case, a solution of (I) can be interpreted as a
_weighted multicycle_ , i.e., as a collection of cycles $M_{1},\dots,M_{k}$
together with weights $a_{1},\ldots,a_{k}$ such that the total effect of the
multicycle, defined by $\sum_{i=1}^{k}a_{i}\cdot\mathit{effect}(M_{i})$, is
non-negative for every counter. Here, $\mathit{effect}(M_{i})$ is the effect
of $M_{i}$ on the counters. The objective of (I) ensures that the multicycle
includes as many transitions as possible, and the total effect of the
multicycle is positive on as many counters as possible. For VASS MDPs, the
$M_{1},\dots,M_{k}$ should not be interpreted as cycles but as Markovian
strategies for some ECs, and $\mathit{effect}(M_{i})$ corresponds to the
vector of expected counter changes per transition in $M_{i}$. The objective of
(I) then maximizes the number of transitions used in the strategies
$M_{1},\dots,M_{k}$, and the number of counters where the expected effect of
the “multicycle” is positive.

A solution of (II) for non-probabilistic VASS can be interpreted as a ranking
function for configurations defined by
$\mathit{rank}(p\mathbf{v})=\mathbf{z}(p)+\sum_{i=1}^{d}\mathbf{y}(i)\mathbf{v}(i)$,
such that the value of $\mathit{rank}$ cannot increase when moving from a
configuration $p\mathbf{v}$ to a configuration $q\mathbf{u}$ using a
transition $t=(p,\mathbf{u}-\mathbf{v},q)$. The objective of (II) ensures that
as many transitions as possible decrease the value of $\mathit{rank}$, and
$\mathit{rank}$ depends on as many counters as possible. For VASS MDPs, this
interpretation changes only for the outgoing transitions $t=(p,\mathbf{u},q)$
of probabilistic states. Instead of considering the change of $\mathit{rank}$
caused by such $t$, we now consider the expected change of $\mathit{rank}$
caused by executing a step from $p$. The objective ensures that
$\mathit{rank}$ depends on as many counters as possible, the value of
$\mathit{rank}$ is decreased by as many outgoing transitions of non-
deterministic states as possible, and the expected change of $\mathit{rank}$
caused by performing an step is negative in as many probabilistic states as
possible.

The key tool for our analysis is the following dichotomy (a proof is in
Appendix A.1).

######  Lemma 4.2.

Let $\mathbf{x}$ be a (maximal) solution to the constraint system (I) and
$\mathbf{y},\mathbf{z}$ be a (maximal) solution to the constraint system (II).
Then, for each counter $c$ we have that either $\mathbf{y}(c)>0$ or
$\sum_{t\in T}\mathbf{x}(t)\mathbf{u}_{t}(c)>0$, and for each transition
$t=(p,\mathbf{u},q)\in T$ we have that

  * •

if $p\in Q_{n}$ then either
$\mathbf{z}(q)-\mathbf{z}(p)+\sum_{i=1}^{d}\mathbf{u}(i)\mathbf{y}(i)<0$ or
$\mathbf{x}(t)>0$;

  * •

if $p\in Q_{p}$ then either

$\sum_{t^{\prime}=(p,\mathbf{u}^{\prime},q^{\prime})\in\mathit{Out}(p)}P(t^{\prime})\big{(}\mathbf{z}(q^{\prime})-\mathbf{z}(p)+\sum_{i=1}^{d}\mathbf{u}^{\prime}(i)\mathbf{y}(i)\big{)}<0$

or $\mathbf{x}(t)>0$.

For the rest of this section, we fix a maximal solution $\mathbf{x}$ of (I)
and a maximal solution $\mathbf{y},\mathbf{z}$ of (II), such that the smallest
non-zero element of $\mathbf{y},\mathbf{z}$ is at least $1$. We define a
ranking function $\mathit{rank}:\mathit{C}(\pazocal{A})\rightarrow\mathbb{N}$
as
$\mathit{rank}(s\mathbf{v})=\mathbf{z}(s)+\sum_{i=1}^{d}\mathbf{v}(i)\mathbf{y}(i)$.
Now we prove the following theorem:

######  Theorem 4.3.

For each counter $c$, if $\mathbf{y}(c)>0$ then $n$ is a tight estimate of
$\pazocal{C}[c]$ (for the only type of $\pazocal{A}$). Otherwise, i.e., when
$\mathbf{y}(c)=0$, the function $n^{2}$ is a lower estimate of
$\pazocal{C}[c]$.

Note that Theorem 4.3 implies Theorem 4.1 for strongly connected VASS MDPs. A
proof is obtained by combining the following lemmata.

######  Lemma 4.4.

For every counter $c$ such that $\mathbf{y}(c)>0$, every $\varepsilon>0$,
every $p\in Q$, and every $\sigma\in\Sigma$, there exists $n_{0}$ such that
for all $n\geq n_{0}$ we have that where $k$ is a constant depending only on
$\pazocal{A}$.

A proof is in Appendix A.3.

For $\mathit{Targets}\subseteq\mathit{C}(\pazocal{A})$ and $m\in\mathbb{N}$,
we use $\mathrm{Reach}^{\leq m}(\mathit{Targets})$ to denote the set of all
computations $\pi=p_{0}\mathbf{v}_{0},p_{1}\mathbf{v}_{1},\ldots$ such that
$p_{i}\mathbf{v}_{i}\in\mathit{Targets}$ for some $i\leq m$.

######  Lemma 4.5.

For each counter $c$ such that $\mathbf{y}(c)=0$ we have that
$\pazocal{C}_{\mathrm{exp}}[c]\in\Omega(n^{2})$ and $n^{2}$ is a lower
estimate of $\pazocal{C}[c]$. Furthermore, for every $\varepsilon>0$ there
exist a sequence of strategies $\sigma_{1},\sigma_{2},\dots$, a constant $k$,
and $p\in Q$ such that for every $0<\varepsilon^{\prime}<\varepsilon$, we have
that

$\lim_{n\to\infty}$

where
$\mathit{Targets}_{n}=\\{q\mathbf{v}\in\mathit{C}(\pazocal{A})\mid\mathbf{v}(c)\geq
n^{2-\varepsilon}\mbox{ for every counter $c$ such that
$\mathbf{y}(c)=0$}\\}$.

A proof is in Appendix A.4.

It remains to prove Theorem 4.1 for VASS MDPs with DAG-like MEC decomposition.
Here, we proceed by analyzing the individual MECs one by one, transferring the
output of the previous MEC to the next one. We start in a top MEC with all
counters initialized to $n$. Here we can directly apply Theorem 4.3 to
determine which of the $\pazocal{C}[c]$ have a tight estimate $n$ and a lower
estimate $n^{2}$, respectively. It follows from Lemma 4.5 that all counters
$c$ such that $n^{2}$ is a lover estimate of $\pazocal{C}[c]$ can be
simultaneously pumped to $n^{2-\varepsilon}$ with very high probability.
However, this computation may decrease the counters $c$ such that $n$ is a
tight estimate for $\pazocal{C}[c]$. To ensure that the value of these
counters is still $\Omega(n)$ when entering the next MEC, we first divide the
initial counter vector $\mathbf{n}$ into two halves, each of size
$\lfloor\frac{\mathbf{n}}{2}\rfloor$, and then pump the counters $c$ such that
$n^{2}$ is a lower estimate for $\pazocal{C}[c]$ to the value
$(\lfloor\frac{n}{2}\rfloor)^{2-\varepsilon}$. We show that the length of this
computation is at most quadratic. The value of the other counters stays at
least $\lfloor\frac{n}{2}\rfloor$. When analyzing the next MEC, we treat the
counters previously pumped to quadratic values as “infinite” because they are
sufficiently large so that they cannot prevent pumping additional counters to
asymptotically quadratic values. Technically, this is implemented by modifying
every counter update vector $\mathbf{u}$ so that $\mathbf{u}[c]=0$ for every
“quadratic” counter $c$. A precise formulation of these observations and the
corresponding proofs are given in Appendix A.5.

We conjecture that the dichotomy of Theorem 4.1 holds for _all_ VASS MDPs, but
we do not have a complete proof. If the MEC decomposition is not DAG-like, a
careful analysis of computations revisiting the same MECs is required; such
repeated visits may but do not have to enable additional asymptotic growth of
$\pazocal{C}[c]$.

##  5 One-Dimensional VASS MDPs

In this section, we give a full and effective classification of tight
estimates of $\pazocal{L}$, $\pazocal{C}[c]$, and $\pazocal{T}[t]$ for one-
dimensional VASS MDPs. More precisely, we prove the following theorem:

######  Theorem 5.1.

Let $\pazocal{A}$ be a one-dimensional VASS MDP. We have the following:

  * •

Let $c$ be the only counter of $\pazocal{A}$. Then one of the following
possibilities holds:

    * –

There exists a type $\beta=M$ such that $\pazocal{C}[c]$ is unbounded for
$\beta$.

    * –

$n$ is a tight estimate of $\pazocal{C}[c]$ for every type.

  * •

Let $t$ be a transition of $\pazocal{A}$. Then one of the following
possibilities holds:

    * –

There exists a type $\beta=M$ such that $\pazocal{T}[t]$ is unbounded for
$\beta$.

    * –

There exists a type $\beta$ such that $\mathit{weight}(\beta)>0$ and
$\pazocal{T}[t]$ is unbounded for $\beta$.

    * –

There exists a type $\beta=M$ such that $n^{2}$ is a tight estimate of
$\pazocal{T}[t]$ for $\beta$.

    * –

The transition $t$ occurs in some MEC $M$, $n$ is a tight estimate of
$\pazocal{T}[t]$ for every type $\beta$ containing the MEC $M$, and $0$ is a
tight estimate of $\pazocal{T}[t]$ for every type $\beta$ not containing the
MEC $M$.

    * –

The transition $t$ does not occur in any MEC, and for every type $\beta$ of
length $k$ we have that $k$ is an upper estimate of $\pazocal{T}[t]$ for
$\beta$.

  * •

One of the following possibilities holds:

    * –

There exists a type $\beta=M$ such that $\pazocal{L}$ is unbounded for
$\beta$.

    * –

There exists a type $\beta=M$ such that $n^{2}$ is a tight estimate of
$\pazocal{L}$ for $\beta$.

    * –

$n$ is a tight estimate of $\pazocal{L}$ for every type.

It is decidable in polynomial time which of the above cases hold.

Note that some cases are mutually exclusive and some may hold simultaneously.
Also recall that $\mathit{weight}(\beta)=1$ for every type $\beta$ of length
one, and $\mathit{weight}(\beta)$ decays exponentially in the length of
$\beta$. Hence, if a transition $t$ does not occur in any MEC, there is a
constant $\kappa<1$ depending only on $\pazocal{A}$ such that for every
$\sigma\in\Sigma$ and $p\mathbf{v}\in\mathit{C}(\pazocal{A})$.

For the rest of this section, we fix a one-dimensional VASS MDP
$\pazocal{A}=\left(Q,(Q_{n},Q_{p}),T,P\right)$ and some linear ordering
$\sqsubseteq$ on $Q$. A proof of Theorem 5.1 is obtained by analyzing bottom
strongly connected components (BSCCs) in a Markov chain obtained from
$\pazocal{A}$ by “applying” some MD strategy $\sigma$ (we use
$\Sigma_{\mathrm{MD}}$ to denote the class of all MD strategies for
$\pazocal{A}$). Recall that $\sigma$ selects the same outgoing transition in
every $p\in Q_{n}$ whenever $p$ is revisited, and hence we can “apply”
$\sigma$ to $\pazocal{A}$ by removing the other outgoing transitions. The
resulting Markov chain is denoted by $\pazocal{A}_{\sigma}$. Note that every
BSCC $\mathbb{B}$ of $\pazocal{A}_{\sigma}$ can also be seen as an end
component of $\pazocal{A}$. For a MEC $M$ of $\pazocal{A}$, we write
$\mathbb{B}\subseteq M$ if all states and transitions of $\mathbb{B}$ are
included in $M$.

For every BSCC $\mathbb{B}$ of $\pazocal{A}_{\sigma}$, let $p_{\mathbb{B}}$ be
the least state of $\mathbb{B}$ with respect to $\sqsubseteq$. Let
$\mathbb{U}_{\mathbb{B}}$ be a function assigning to every infinite path
$\pi=p_{0},\mathbf{u}_{1},p_{1},\mathbf{u}_{2},\ldots$ the sum
$\sum_{i=1}^{\ell}\mathbf{u}_{i}$ if $p_{0}=p_{\mathbb{B}}$ and $\ell\geq 1$
is the least index such that $p_{\ell}=p_{\mathbb{B}}$, otherwise
$\mathbb{U}_{\mathbb{B}}(\pi)=0$. Hence, $\mathbb{U}_{\mathbb{B}}(\pi)$ is the
change of the (only) counter $c$ along $\pi$ until $p_{\mathbb{B}}$ is
revisited.

######  Definition 5.2.

Let $\mathbb{B}$ be a BSCC of $\pazocal{A}_{\sigma}$. We say that $\mathbb{B}$
is

  * •

_increasing_ if $\mathbb{E}^{\sigma}_{p_{\mathbb{B}}}(\mathbb{U}_{B})>0$,

  * •

_decreasing_ if $\mathbb{E}^{\sigma}_{p_{\mathbb{B}}}(\mathbb{U}_{B})<0$,

  * •

_bounded-zero_ if $\mathbb{E}^{\sigma}_{p_{\mathbb{B}}}(\mathbb{U}_{B})=0$ and
,

  * •

_unbounded-zero_ if $\mathbb{E}^{\sigma}_{p_{\mathbb{B}}}(\mathbb{U}_{B})=0$
and .

Note that the above definition does not depend on the concrete choice of
$\sqsubseteq$. We prove the following results relating the existence of
upper/lower estimates of $\pazocal{L}$, $\pazocal{C}[c]$, and $\pazocal{T}[t]$
to the existence of BSCCs with certain properties. More concretely,

  * •

for $\pazocal{C}[c]$, we show that

    * –

$\pazocal{C}[c]$ is unbounded for some type $\beta=M$ if there exists an
increasing BSCC $\mathbb{B}$ of $\pazocal{A}_{\sigma}$ for some
$\sigma\in\Sigma_{\mathrm{MD}}$ such that $\mathbb{B}\subseteq M$ (Lemma B.3);

    * –

otherwise, $n$ is a tight estimate of $\pazocal{C}[c]$ for every type (Lemma
B.11)

  * •

for $\pazocal{L}$, we show that

    * –

$\pazocal{L}$ is unbounded for some type $\beta=M$ if there exists an
increasing or bounded-zero BSCC $\mathbb{B}$ of $\pazocal{A}_{\sigma}$ for
some $\sigma\in\Sigma_{\mathrm{MD}}$ such that $\mathbb{B}\subseteq M$ (Lemma
B.3, Lemma B.5);

    * –

otherwise, $n^{2}$ is an upper estimate of $\pazocal{L}$ for every type
$\beta$ (Lemma B.10);

    * –

if there exists an unbounded-zero BSCC $\mathbb{B}$ of $\pazocal{A}_{\sigma}$
for some $\sigma\in\Sigma_{\mathrm{MD}}$, then $n^{2}$ is a lower estimate of
$\pazocal{L}$ for $\beta=M$ where $\mathbb{B}\subseteq M$ (Lemma B.4);

    * –

if every BSCC $\mathbb{B}$ of every $\pazocal{A}_{\sigma}$ is decreasing, then
$\pazocal{L}_{\mathrm{exp}}(n)\in\Theta(n)$ (this follows from [2]), and hence
$n$ is a tight estimate of $\pazocal{L}$ for every type (Observation 3.2);

  * •

for $\pazocal{T}[t]$, we distinguish two cases:

    * –

If $t$ is not contained in any MEC of $\pazocal{A}$, then for every type
$\beta$ of length $k$, the transition $t$ cannot be executed more than $k$
times along a arbitrary computation $\pi$ where $\mathit{mecs}(\pi)=\beta$.

    * –

If $t$ is contained in a MEC $M$ of $\pazocal{A}$, then

      * *

$\pazocal{T}[t]$ is unbounded for $\beta=M$ if there exist an increasing BSCC
$\mathbb{B}$ of $\pazocal{A}_{\sigma}$ for some
$\sigma\in\Sigma_{\mathrm{MD}}$ such that $\mathbb{B}\subseteq M$ (Lemma B.3),
or bounded-zero BSCC $\mathbb{B}$ of $\pazocal{A}_{\sigma}$ for some
$\sigma\in\Sigma_{\mathrm{MD}}$ such that $\mathbb{B}$ contains $t$ (Lemma
B.5);

      * *

$\pazocal{T}[t]$ is unbounded for every $\beta=M_{1},\dots,M_{k}$ such that
$M=M_{i}$ for some $i$ and there exists an increasing BSCC $\mathbb{B}$ of
$\pazocal{A}_{\sigma}$ for some $\sigma\in\Sigma_{\mathrm{MD}}$ such that
$\mathbb{B}\subseteq M_{j}$ for some $j\leq i$ (Lemma B.3);

      * *

otherwise, $n^{2}$ is an upper estimate of $\pazocal{T}[t]$ for every type
(Lemma B.10);

      * *

if there is an unbounded-zero BSCC $\mathbb{B}$ of $\pazocal{A}_{\sigma}$ for
some $\sigma\in\Sigma_{\mathrm{MD}}$ such that $\mathbb{B}$ contains $t$, then
$n^{2}$ is a lower estimate of $\pazocal{T}[t]$ for $\beta=M$ (Lemma B.4);

      * *

if every BSCC $\mathbb{B}$ of every $\pazocal{A}_{\sigma}$ is decreasing, then
$\pazocal{T}[t]_{\mathrm{exp}}(n)\in\Theta(n)$ (this follows from [2]), and
hence $n$ is an upper estimate of $\pazocal{T}[t]$ for every type (Observation
3.2).

The polynomial time bound of Theorem 5.1 is then obtained by realizing the
following: First, we need to decide the existence of an increasing BSCC of
$\pazocal{A}_{\sigma}$ for some $\sigma\in\Sigma_{\mathrm{MD}}$. This can be
done in polynomial time using the constraint system (I) of Fig. 3 (Lemma B.1).
If no such increasing BSCC exists, we need to decide the existence of a
bounded-zero BSCC, which can be achieved in polynomial time for a subclass of
one-dimensional VASS MDPs where no increasing BSCC exists (Lemma B.7). Then,
if no bounded-zero BSCC exists, we need to decide the existence of an
unbounded-zero BSCC, which can again be done in polynomial time using the
constraint system (I) of Fig. 3 (realize that any solution $\mathbf{x}$ of (I)
implies the existence of a BSCC that is either increasing, bounded-zero, or
unbounded-zero).

Hence, the “algorithmic part” of Theorem 5.1 is an easy consequence of the
above observations, but there is one remarkable subtlety. Note that we need to
decide the existence of a bounded-zero BSCC only for a subclass of one-
dimensional VASS MDPs where no increasing BSCCs exist. This is actually
crucial, because deciding the existence of a bounded-zero BSCC in _general_
one-dimensional VASS MDPs is NP-complete (Lemma B.27).

The main difficulties requiring novel insights are related to proving the
observation about $\pazocal{C}[c]$, stating that if there is no increasing
BSCC of $\pazocal{A}_{\sigma}$ for any $\sigma\in\Sigma_{\mathrm{MD}}$, then
$n$ is an upper estimate of $\pazocal{C}[c]$ for every type. A comparably
difficult (and in fact closely related) task is to show that if there is no
increasing or bounded-zero BSCC, then $n^{2}$ is an upper estimate of
$\pazocal{L}$ for every type. Note that here we need to analyze the behaviour
of $\pazocal{A}$ under _all_ strategies (not just MD), and consider the
notoriously difficult case when the long-run average change of the counter
caused by applying the strategy is zero. Here we need to devise a suitable
decomposition technique allowing for interpreting general strategies as
“interleavings” of MD strategies and lifting the properties of MD strategies
to general strategies. Furthermore, we need to devise techniques for reducing
the problems of our interest to analyzing certain types of random walks that
have already been studied in stochastic process theory. We discuss this more
in the following subsection, and we refer to Appendix B for a complete
exposition of these results.

###  5.1 MD decomposition

As we already noted, one crucial observation behind Theorem 5.1 is that if
there is no increasing BSCC of $\pazocal{A}_{\sigma}$ for any
$\sigma\in\Sigma_{\mathrm{MD}}$, then $n$ is an upper estimate of
$\pazocal{C}[c]$ for every type. In this section, we sketch the main steps
towards this result.

First, we show that every path in $\pazocal{A}$ can be decomposed into
“interweavings” of paths generated by MD strategies.

Let $\alpha=p_{0},\mathbf{v}_{1},\dots,p_{k}$ be a path. For every $i\leq k$,
we use $\alpha_{..i}=p_{0},\mathbf{v}_{1},\ldots,p_{i}$ to denote the prefix
of $\alpha$ of length $i$. We say that $\alpha$ is _compatible_ with a MD
strategy $\sigma$ if $\sigma(\alpha_{..i})=(p_{i},\mathbf{v}_{i+1},p_{i+1})$
for all $i<k$ such that $p_{i}\in Q_{n}$. Furthermore, for every path
$\beta=q_{0},\mathbf{u}_{1},q_{1},\dots,q_{\ell}$ such that $p_{k}=q_{0}$, we
define a path
$\alpha\circ\beta=p_{0},\mathbf{v}_{1},p_{1},\dots,p_{k},\mathbf{u}_{1},q_{1},\dots,q_{\ell}$.

######  Definition 5.3.

Let $\pazocal{A}$ be a VASS MDP,
$\pi_{1},\dots,\pi_{k}\in\Sigma_{\mathrm{MD}}$, and $p_{1},\dots,p_{k}\in Q$.
An _MD-decomposition_ of a path $\alpha=s_{1},\ldots,s_{m}$ under
$\pi_{1},\dots,\pi_{k}$ and $p_{1},\dots,p_{k}$ is a decomposition of $\alpha$
into finitely many paths
$\alpha=\gamma_{1}^{1}\circ\cdots\circ\gamma_{1}^{k}\;\circ\;\gamma_{2}^{1}\circ\cdots\circ\gamma_{2}^{k}\;\circ\;\cdots\;\circ\;\gamma_{\ell}^{1}\circ\cdots\circ\gamma_{\ell}^{k}$
satisfying the following conditions:

  * •

for all $i<\ell$ and $j\leq k$, the last state of $\gamma_{i}^{j}$ is the same
as the first state of $\gamma_{i+1}^{j}$;

  * •

for every $j\leq k$, $\gamma_{1}^{j}\circ\cdots\circ\gamma_{\ell}^{j}$ is a
path that begins with $p_{j}$ and is compatible with $\pi_{j}$.

Note that $\pi_{1},\dots,\pi_{k}$ and $p_{1},\dots,p_{k}$ are not necessarily
pairwise different, and the length of $\gamma_{i}^{j}$ can be zero. Also note
that the same $\alpha$ may have several MD-decompositions.

Intuitively, an MD decomposition of $\alpha$ shows how to obtain $\alpha$ by
repeatedly selecting zero or more transitions by $\pi_{1},\ldots,\pi_{k}$. The
next lemma shows that for every VASS MDP $\pazocal{A}$, one can _fix_ MD
strategies $\pi_{1},\ldots,\pi_{k}$ and states $p_{1},\ldots,p_{k}$ such that
_every_ path $\alpha$ in $\pazocal{A}$ has an MD-decomposition under
$\pi_{1},\ldots,\pi_{k}$ and $p_{1},\ldots,p_{k}$. Furthermore, such a
decomposition is constructible _online_ as $\alpha$ is read from left to
right.

######  Lemma 5.4.

For every VASS MDP $\pazocal{A}$, there exist
$\pi_{1},\dots,\pi_{k}\in\Sigma_{\mathrm{MD}}$, $p_{1},\dots,p_{k}\in Q$, and
a function $Decomp{A}$ such that the following conditions are satisfied for
every finite path $\alpha$:

  * •

$Decomp{A}(\alpha)$ returns an MD-decomposition of $\alpha$ under
$\pi_{1},\dots,\pi_{k}$ and $p_{1},\ldots,p_{k}$.

  * •

$Decomp{A}(\alpha)=Decomp{A}(\alpha_{..\mathit{len}(\alpha)-1})\;\circ\;\gamma^{1}\circ\cdots\circ\gamma^{k}$,
where exactly one of $\gamma^{i}$ has positive length (the $i$ is called the
_mode_ of $\alpha$).

  * •

If the last state of $\alpha_{..\mathit{len}(\alpha)-1}$ is probabilistic,
then the mode of $\alpha$ does not depend on the last transition of $\alpha$.

A proof of Lemma 5.4 is in Appendix B.

According to Lemma 5.4, _every_ strategy $\sigma$ for $\pazocal{A}$ just
performs a certain “interleaving” of the MD strategies $\pi_{1},\dots,\pi_{k}$
initiated in the states $p_{1},\ldots,p_{k}$. We aim to show that if every
BSCC of every $\pazocal{A}_{\pi_{j}}$ is non-increasing, then $n$ is an upper
estimate of $\pazocal{C}[c]$ for every type. Since we do not have any control
over the length of the individual $\gamma_{i}^{j}$ occurring in MD-
decompositions, we need to introduce another concept of _extended VASS MDPs_
where the strategies $\pi_{1},\dots,\pi_{k}$ can be interleaved in “longer
chunks”. Intuitively, an extended VASS MDP is obtained from $\pazocal{A}$ by
taking $k$ copies of $\pazocal{A}$ sharing the same counter. The $j$-th copy
selects transitions according to $\pi_{j}$. At each round, only one $\pi_{j}$
makes a move, where the $j$ is selected by a special type of “pointing”
strategy defined especially for extended MDPs. Note that $\sigma$ can be
faithfully simulated in the extended VASS MDP by a pointing strategy that
selects the indexes consistently with $Decomp{A}$. However, we can also
construct another pointing strategy that simulates each $\pi_{j}$ longer
(i.e., “precomputes” the steps executed by $\pi_{j}$ in the future) and thus
“close cycles” in the BSCC visited by $\pi_{j}$. This computation can be seen
as an interleaving of a finite number of independent random walks with non-
positive expectations. Then, we use the optional stopping theorem to get an
upper bound on the total expected number of “cycles”, which can then be used
to obtain the desired upper estimate. We refer to Appendix B for details.

###  5.2 A Note about Energy Games

One-dimensional VASS MDPs are closely related to energy games/MDPs [5, 6, 7,
12]. An important open problem for energy games is the complexity of deciding
the existence of a _safe_ configuration where, for a sufficiently high energy
amount, the responsible player can avoid decreasing the energy resource
(counter) below zero. This problem is known to be in
$\mathbf{NP}\cap\mathbf{coNP}$, and a pseudopolynomial algorithm for the
problem exists; however, it is still open whether the problem is in
$\mathbf{P}$ when the counter updates are encoded in binary. Our analysis
shows that this problem is solvable in polynomial time for energy (i.e., one-
dimensional VASS) MDPs $\pazocal{A}$ such that there is no increasing SCC of
$\pazocal{A}_{\sigma}$ for any $\sigma\in\Sigma_{\mathrm{MD}}$.

We say that a SCC $\mathbb{B}$ of $\pazocal{A}_{\sigma}$ is _non-decreasing_
if $\mathbb{B}$ does not contain any negative cycles. Note that every bounded-
zero SCC is non-decreasing, and a increasing SCC may but does not have to be
non-decreasing.

######  Lemma 5.5.

An energy MDP has a safe configuration iff there exists a non-decreasing SCC
$\mathbb{B}$ of $\pazocal{A}_{\sigma}$ for some
$\sigma\in\Sigma_{\mathrm{MD}}$.

The “$\Leftarrow$” direction of Lemma 5.5 is immediate, and the other
direction can be proven using our MD decomposition technique, see Appendix
B.3.

Note that if there is no increasing SCC $\mathbb{B}$ of $\pazocal{A}_{\sigma}$
for any $\sigma\in\Sigma_{\mathrm{MD}}$, then the existence of a non-
decreasing SCC is equivalent to the existence of a bounded-zero SCC, and hence
it can be decided in polynomial time (see the results presented above).
However, for general energy MDPs, the best upper complexity bound for the
existence of a non-decreasing SCC is $\mathbf{NP}\cap\mathbf{coNP}$.
Interestingly, a small modification of this problem already leads to
$\mathbf{NP}$-completeness, as demonstrated by the following lemma.

######  Lemma 5.6.

The problem whether there exists a non-decreasing SCC $\mathbb{B}$ of
$\pazocal{A}_{\sigma}$ for some $\sigma\in\Sigma_{\mathrm{MD}}$ such that
$\mathbb{B}$ contains a given state $p\in Q$ is $\mathbf{NP}$-complete.

A proof of Lemma 5.6 is in Appendix B.4.

##  6 Conclusions

We introduced new estimates for measuring the asymptotic complexity of
probabilistic programs and their VASS abstractions. We demonstrated the
advantages of these measures over the asymptotic analysis of expected values,
and we have also shown that tight complexity estimates can be computed
efficiently for certain subclasses of VASS MDPs.

A natural continuation of our work is extending the results achieved for one-
dimensional VASS MDPs to the multi-dimensional case. In particular, an
interesting open question is whether the polynomial asymptotic analysis for
non-deterministic VASS presented in [23] can be generalized to VASS MDPs.
Since the study of multi-dimensional VASS MDPs is notoriously difficult, a
good starting point would be a complete understanding of VASS MDPs with two
counters.

## References

  * [1] M. Ajdarów and A. Kučera.  Deciding polynomial termination complexity for VASS programs.  In Proceedings of CONCUR 2021, volume 203 of LIPIcs, pages 30:1–30:15. Schloss Dagstuhl, 2021.
  * [2] 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.
  * [3] 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.
  * [4] 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.
  * [5] K. Chatterjee and L. Doyen.  Energy parity games.  In Proceedings of ICALP 2010, Part II, volume 6199 of LNCS, pages 599–610. Springer, 2010.
  * [6] K. Chatterjee and L. Doyen.  Energy and mean-payoff parity Markov decision processes.  In Proceedings of MFCS 2011, volume 6907 of LNCS, pages 206–218. Springer, 2011.
  * [7] K. Chatterjee, M. Henzinger, S. Krinninger, and D. Nanongkai.  Polynomial-time algorithms for energy games with special weight structures.  In Proceedings of ESA 2012, volume 7501 of LNCS, pages 301–312. Springer, 2012.
  * [8] 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.
  * [9] J. Esparza.  Decidability of model checking for infinite-state concurrent systems.  AI, 34:85–107, 1997.
  * [10] J.E. Hopcroft and J.-J. Pansiot.  On the reachability problem for 5-dimensional vector addition systems.  TCS, 8:135–159, 1979.
  * [11] P. Jančar.  Undecidability of bisimilarity for Petri nets and some related problems.  TCS, 148(2):281–301, 1995.
  * [12] M. Jurdziński, R. Lazić, and S. Schmitz.  Fixed-dimensional energy games are in pseudo-polynomial time.  In Proceedings of ICALP 2015, volume 9135 of LNCS, pages 260–272. Springer, 2015.
  * [13] A. Kučera.  Algorithmic analysis of termination and counter complexity in vector addition systems with states: A survey of recent results.  ACM SIGLOG News, 8(4):4–21, 2021.
  * [14] 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.
  * [15] 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.
  * [16] J. Leroux and Ph. Schnoebelen.  On functions weakly computable by Petri nets and vector addition systems.  In Reachability Problems, volume 8762 of LNCS, pages 190–202. Springer, 2014.
  * [17] R. Lipton.  The reachability problem requires exponential space.  Technical report 62, Yale University, 1976.
  * [18] E.W. Mayr and A.R. Meyer.  The complexity of the finite containment problem for Petri nets.  JACM, 28(3):561–576, 1981.
  * [19] C.A. Petri.  Kommunikation mit automaten.  Schriften des Institutes für Instrumentelle Mathematik, 3, 1962.
  * [20] M.L. Puterman.  Markov Decision Processes.  Wiley, 1994.
  * [21] M. Sinn, F. Zuleger, and H. Veith.  A simple and scalable static analysis for bound analysis and amortized complexity analysis.  In Proceedings of CAV 2014, volume 8559 of LNCS, pages 745–761. Springer, 2013.
  * [22] M. Sinn, F. Zuleger, and H. Veith.  Complexity and resource bound analysis of imperative programs using difference constraints.  Journal of Automated Reasoning, 59(1):3–45, 2017.
  * [23] 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 Proofs for Section 4

###  A.1 Proof of Lemma 4.2

######  Lemma (4.2).

Let $\mathbf{x}$ be a (maximal) solution to the constraint system (I) and
$\mathbf{y},\mathbf{z}$ be a (maximal) solution to the constraint system (II).
Then, for each counter $c$ we have that either $\mathbf{y}(c)>0$ or
$\sum_{t\in T}\mathbf{x}(t)\mathbf{u}_{t}(c)>0$, and for each transition
$t=(p,\mathbf{u},q)\in T$ we have that

  * •

if $p\in Q_{n}$ then either
$\mathbf{z}(q)-\mathbf{z}(p)+\sum_{i=1}^{d}\mathbf{u}(i)\mathbf{y}(i)<0$ or
$\mathbf{x}(t)>0$;

  * •

if $p\in Q_{p}$ then either

$\sum_{t^{\prime}=(p,\mathbf{u}^{\prime},q^{\prime})\in\mathit{Out}(p)}P(t^{\prime})\big{(}\mathbf{z}(q^{\prime})-\mathbf{z}(p)+\sum_{i=1}^{d}\mathbf{u}^{\prime}(i)\mathbf{y}(i)\big{)}<0$

or $\mathbf{x}(t)>0$.

Proof: Let $A=T_{n}\cup Q_{p}$, where $T_{n}=\bigcup_{p\in
Q_{n}}\mathit{Out}(p)$. For each $a\in A$, let $\mathit{next}_{a}$ be a
probability distribution on $Q$ such that

  * •

$\mathit{next}_{(p,\mathbf{u},q)}(q)=1$ for $a=(p,\mathbf{u},q)\in T_{n}$,

  * •

$\mathit{next}_{p}(q)=\sum_{(p,\mathbf{u},q)\in\mathit{Out}(p)\cap\mathit{In}(q)}P((p,\mathbf{u},q))$
for $a=p\in Q_{p}$,

  * •

and $\mathit{next}_{a}(p)=0$ else,

let $\mathit{from}_{a}$ be a probability distribution on $Q$ such that

  * •

$\mathit{from}_{(p,\mathbf{u},q)}(p)=1$ for $a=(p,\mathbf{u},q)\in T_{n}$,

  * •

$\mathit{from}_{p}(p)=1$ for $a=p\in Q_{p}$,

  * •

and $\mathit{from}_{a}(p)=0$ else,

and let $\mathit{effect}_{a}$ be defined as

  * •

$\mathit{effect}_{(p,\mathbf{u},q)}=\mathbf{u}$ for $a=(p,\mathbf{u},q)\in
T_{n}$,

  * •

and
$\mathit{effect}_{p}=\sum_{(p,\mathbf{u},q)\in\mathit{Out}(p)}P((p,\mathbf{u},q))\mathbf{u}$
for $a=p\in Q_{p}$.

Then we can rewrite the constraint systems as

Constraint system (I’): Find $\mathbf{x}^{\prime}\in\mathbb{Z}^{A}$ such that $\displaystyle\sum_{a\in A}\mathbf{x}^{\prime}(a)\mathit{effect}_{a}$ $\displaystyle\geq\vec{0}$ $\displaystyle\mathbf{x}^{\prime}$ $\displaystyle\geq\vec{0}$ and for each $p\in Q$ $\displaystyle\sum_{a\in A}(\mathbf{x}^{\prime}(a)\mathit{next}_{a}(p)-\mathbf{x}^{\prime}(a)\mathit{from}_{a}(p))$ $\displaystyle=0$ |  Constraint system (II’): Find $\mathbf{y}\in\mathbb{Z}^{d},\mathbf{z}\in\mathbb{Z}^{Q}$ such that $\displaystyle\mathbf{y}$ $\displaystyle\geq\vec{0}$ $\displaystyle\mathbf{z}$ $\displaystyle\geq\vec{0}$ and for each $a\in A$ $\sum_{p\in Q}(\mathbf{z}(p)\mathit{next}_{a}(p)-\mathbf{z}(p)(\mathit{from}_{a}(p)))+\sum_{i=1}^{d}\mathit{effect}_{a}(i)\mathbf{y}(i)\leq 0$
---|---

We recognize systems (I) and (I’) as equivalent, and systems (II) and (II’) as
equivalent as per the following lemma.

######  Lemma A.1.

If $\mathbf{x}^{\prime},\mathbf{y},\mathbf{z}$ is a solution to the rewritten
constraint systems (I’) and (II’), then $\mathbf{x},\mathbf{y},\mathbf{z}$ is
a solution to the original constraint systems (I) and (II), where
$\mathbf{x}(t)=\mathbf{x}^{\prime}(t)$ for $t\in T_{n}$, and
$\mathbf{x}((p,\mathbf{u},q))=P((p,\mathbf{u},q))\mathbf{x}^{\prime}(p)$ for
$(p,\mathbf{u},q)\in T\setminus T_{n}$. Similarly, if
$\mathbf{x},\mathbf{y},\mathbf{z}$ is a solution to the original constraint
systems (I) and (II), then $\mathbf{x}^{\prime},\mathbf{y},\mathbf{z}$ is a
solution to the rewritten constraint systems (I’) and (II’), where
$\mathbf{x}^{\prime}(t)=\mathbf{x}(t)$ for $t\in T_{n}$, and
$\mathbf{x}^{\prime}(p)=\sum_{t\in\mathit{Out}(p)}\mathbf{x}(t)$ for $p\in
Q_{p}$.

######  Proof A.2.

The first half (I): Let $\mathbf{x}^{\prime}$ be a solution of (I’), we will
show that $\mathbf{x}$ is a solution to (I), where
$\mathbf{x}(t)=\mathbf{x}^{\prime}(t)$ for $t\in T_{n}$, and
$\mathbf{x}((p,\mathbf{u},q))=P((p,\mathbf{u},q))\mathbf{x}^{\prime}(p)$ for
$(p,\mathbf{u},q)\in T\setminus T_{n}$.

It holds from (I’) that

$\displaystyle\sum_{a\in
A}\mathbf{x}^{\prime}(a)\mathit{effect}_{a}=\sum_{t\in
T_{n}}\mathbf{x}^{\prime}(t)\mathit{effect}_{t}+\sum_{p\in
Q_{p}}\mathbf{x}^{\prime}(p)\mathit{effect}_{p}=$ $\displaystyle=\sum_{t\in
T_{n}}\mathbf{x}^{\prime}(t)\mathbf{u}_{t}+\sum_{p\in
Q_{p}}\mathbf{x}^{\prime}(p)(\sum_{(p,\mathbf{u},q)\in\mathit{Out}(p)}P((p,\mathbf{u},q))\mathbf{u})$
$\displaystyle=\sum_{t\in T_{n}}\mathbf{x}(t)\mathbf{u}_{t}+\sum_{p\in
Q_{p}}\sum_{(p,\mathbf{u},q)\in\mathit{Out}(p)}\mathbf{x}^{\prime}(p)P((p,\mathbf{u},q))\mathbf{u}$
$\displaystyle=\sum_{t\in T_{n}}\mathbf{x}(t)\mathbf{u}_{t}+\sum_{p\in
Q_{p}}\sum_{(p,\mathbf{u},q)\in\mathit{Out}(p)}\mathbf{x}((p,\mathbf{u},q))\mathbf{u}$
$\displaystyle=\sum_{t\in T}\mathbf{x}(t)\mathbf{u}_{t}\geq\vec{0}$

$\mathbf{x}\geq 0$ holds from both $\mathbf{x}^{\prime}\geq 0$ and $P(t)\geq
0$ for each $t\in T\setminus T_{n}$.

For each $p\in Q$ it holds from (I’)

$\displaystyle\sum_{a\in
A}(\mathbf{x}^{\prime}(a)\mathit{next}_{a}(p)-\mathbf{x}^{\prime}(a)\mathit{from}_{a}(p))=$
$\displaystyle=\sum_{a\in
T_{n}}(\mathbf{x}^{\prime}(a)\mathit{next}_{a}(p)-\mathbf{x}^{\prime}(a)\mathit{from}_{a}(p))+\sum_{a\in
Q_{r}}(\mathbf{x}^{\prime}(a)\mathit{next}_{a}(p)-\mathbf{x}^{\prime}(a)\mathit{from}_{a}(p))$
$\displaystyle=\sum_{t\in\mathit{In}(p)\cap
T_{n}}\mathbf{x}^{\prime}(t)-\sum_{t\in\mathit{Out}(p)\cap
T_{n}}\mathbf{x}^{\prime}(t)+\sum_{a\in
Q_{r}}\mathbf{x}^{\prime}(a)(\sum_{t\in\mathit{Out}(a)\cap\mathit{In}(p)}P(t))-\mathbf{x}^{\prime}(p)$
$\displaystyle=\sum_{t\in\mathit{In}(p)\cap
T_{n}}\mathbf{x}(t)-\sum_{t\in\mathit{Out}(p)\cap
T_{n}}\mathbf{x}(t)+\sum_{a\in
Q_{r}}\sum_{t\in\mathit{Out}(a)\cap\mathit{In}(p)}\mathbf{x}^{\prime}(a)P(t)-\sum_{t\in\mathit{Out}(p)}P(t)\mathbf{x}^{\prime}(p)$
$\displaystyle=\sum_{t\in\mathit{In}(p)\cap
T_{n}}\mathbf{x}(t)-\sum_{t\in\mathit{Out}(p)\cap
T_{n}}\mathbf{x}(t)+\sum_{a\in
Q_{r}}\sum_{t\in\mathit{Out}(a)\cap\mathit{In}(p)}\mathbf{x}(t)-\sum_{t\in\mathit{Out}(p)}\mathbf{x}(t)$
$\displaystyle=\sum_{t\in\mathit{In}(p)}\mathbf{x}(t)-\sum_{t\in\mathit{Out}(p)}\mathbf{x}(t)=0$

And for each $p\in Q_{p},t\in\mathit{Out}(p)$ it holds
$\sum_{t^{\prime}\in\mathit{Out}(p)}\mathbf{x}(t^{\prime})=\sum_{t^{\prime}\in\mathit{Out}(p)}P(t^{\prime})\mathbf{x}^{\prime}(p)=\mathbf{x}^{\prime}(p)$,
therefore it holds
$\mathbf{x}(t)=P(t)\mathbf{x}^{\prime}(p)=P(t)\sum_{t^{\prime}\in\mathit{Out}(p)}x(t^{\prime})$.

Thus $\mathbf{x}$ is a solution to (I).

The first half (II): Let $\mathbf{y},\mathbf{z}$ be a solution of (II’), we
will show it is also a solution of (II).

For each $a=(p,\mathbf{u},q)\in T_{n}$ it holds from (II’)

$\displaystyle\sum_{p^{\prime}\in
Q}(\mathbf{z}(p^{\prime})(\mathit{next}_{a}(p^{\prime})-\mathbf{z}(p^{\prime})(\mathit{from}_{a}(p^{\prime})))+\sum_{i=1}^{d}\mathit{effect}_{a}(i)\mathbf{y}(i)=\mathbf{z}(q)-\mathbf{z}(p)+\sum_{i=1}^{d}\mathbf{u}(i)\mathbf{y}(i)\leq
0$

And for each $a=p\in Q_{p}$ it holds from (II’)

$\displaystyle\sum_{q\in
Q}(\mathbf{z}(q)\mathit{next}_{a}(q)-\mathbf{z}(q)\mathit{from}_{a}(q)))+\sum_{i=1}^{d}\mathit{effect}_{a}(i)\mathbf{y}(i)=$
$\displaystyle=\sum_{q\in
Q}(\mathbf{z}(q)(\sum_{t\in\mathit{Out}(p)\cap\mathit{In}(q)}P(t)))-\mathbf{z}(p)+\sum_{i=1}^{d}\mathit{effect}_{a}(i)\mathbf{y}(i)$
$\displaystyle=\sum_{t\in\mathit{Out}(p)}\mathbf{z}(q)P(t)-\sum_{t\in\mathit{Out}(p)}\mathbf{z}(p)P(t)+\sum_{i=1}^{d}\mathit{effect}_{a}(i)\mathbf{y}(i)$
$\displaystyle=\sum_{t\in\mathit{Out}(p)}P(t)(\mathbf{z}(q)-\mathbf{z}(p))+\sum_{i=1}^{d}\sum_{t\in\mathit{Out}(p)}P(t)\mathbf{u}_{t}(i)\mathbf{y}(i)$
$\displaystyle=\sum_{t\in\mathit{Out}(p)}P(t)(\mathbf{z}(q)-\mathbf{z}(p))+\sum_{t\in\mathit{Out}(p)}\sum_{i=1}^{d}P(t)\mathbf{u}_{t}(i)\mathbf{y}(i)$
$\displaystyle=\sum_{t\in\mathit{Out}(p)}P(t)\big{(}\mathbf{z}(q)-\mathbf{z}(p)+\sum_{i=1}^{d}\mathbf{u}_{t}(i)\mathbf{y}(i)\big{)}\leq
0$

Therefore $\mathbf{y},\mathbf{z}$ is a solution of (II).

The second half (I’): Let $\mathbf{x}$ be a solution of (I), we will show that
$\mathbf{x}^{\prime}$ is a solution of (I’), where
$\mathbf{x}^{\prime}(t)=\mathbf{x}(t)$ for $t\in T_{n}$, and
$\mathbf{x}^{\prime}(p)=\sum_{t\in\mathit{Out}(p)}\mathbf{x}(t)$ for $p\in
Q_{p}$.

From (I) it holds for $T_{p}=\bigcup_{p\in Q_{p}}\mathit{Out}(p)$

$\displaystyle\sum_{t\in T}\mathbf{x}(t)\mathbf{u}_{t}=$
$\displaystyle=\sum_{t\in T_{n}}\mathbf{x}(t)\mathbf{u}_{t}+\sum_{t\in
T_{p}}\mathbf{x}(t)\mathbf{u}_{t}$ $\displaystyle=\sum_{t\in
T_{n}}\mathbf{x}^{\prime}(t)\mathbf{u}_{t}+\sum_{(p,\mathbf{u},q)\in
T_{p}}\mathbf{u}P((p,\mathbf{u},q))\cdot\big{(}\sum_{t^{\prime}\in\mathit{Out}(p)}\mathbf{x}(t^{\prime})\big{)}$
$\displaystyle=\sum_{t\in
T_{n}}\mathbf{x}^{\prime}(t)\mathbf{u}_{t}+\sum_{(p,\mathbf{u},q)\in
T_{p}}\mathbf{u}P((p,\mathbf{u},q))\mathbf{x}^{\prime}(p)$
$\displaystyle=\sum_{t\in
T_{n}}\mathbf{x}^{\prime}(t)\mathbf{u}_{t}+\sum_{p\in
Q_{p}}\sum_{(p,\mathbf{u},q)\in\mathit{Out}(p)}\mathbf{u}P((p,\mathbf{u},q))\mathbf{x}^{\prime}(p)$
$\displaystyle=\sum_{t\in
T_{n}}\mathbf{x}^{\prime}(t)\cdot\mathit{effect}_{t}+\sum_{p\in
Q_{p}}\mathbf{x}^{\prime}(p)\cdot\mathit{effect}_{p}$
$\displaystyle=\sum_{a\in
A}\mathbf{x}^{\prime}(a)\cdot\mathit{effect}_{a}\geq\vec{0}$

We get $\mathbf{x}^{\prime}\geq 0$ trivially from (I).

It also holds

$\displaystyle\sum_{a\in
A}(\mathbf{x}^{\prime}(a)\mathit{next}_{a}(p)-\mathbf{x}^{\prime}(a)\mathit{from}_{a}(p))=$
$\displaystyle=\sum_{t\in
T_{n}}(\mathbf{x}^{\prime}(t)\mathit{next}_{t}(p)-\mathbf{x}^{\prime}(t)\mathit{from}_{t}(p))+\sum_{q\in
Q_{p}}(\mathbf{x}^{\prime}(q)\mathit{next}_{q}(p)-\mathbf{x}^{\prime}(q)\mathit{from}_{q}(p))$
$\displaystyle=\sum_{t\in\mathit{In}(p)\cap
T_{n}}\mathbf{x}^{\prime}(t)-\sum_{t\in\mathit{Out}(p)\cap
T_{n}}\mathbf{x}^{\prime}(t)+\sum_{q\in
Q_{p}}\mathbf{x}^{\prime}(q)(\sum_{t\in\mathit{Out}(q)\cap\mathit{In}(p)}P(t))-\sum_{q\in
Q_{p}\cap\\{p\\}}\mathbf{x}^{\prime}(q)$
$\displaystyle=\sum_{t\in\mathit{In}(p)\cap
T_{n}}\mathbf{x}^{\prime}(t)-\sum_{t\in\mathit{Out}(p)\cap
T_{n}}\mathbf{x}^{\prime}(t)+\sum_{q\in
Q_{p}}\sum_{t\in\mathit{Out}(q)\cap\mathit{In}(p)}P(t)\mathbf{x}^{\prime}(q)-\sum_{q\in
Q_{p}\cap\\{p\\}}\mathbf{x}^{\prime}(q)$
$\displaystyle=\sum_{t\in\mathit{In}(p)\cap
T_{n}}\mathbf{x}(t)-\sum_{t\in\mathit{Out}(p)\cap
T_{n}}\mathbf{x}(t)+\sum_{q\in
Q_{p}}\sum_{t\in\mathit{Out}(q)\cap\mathit{In}(p)}P(t)\cdot(\sum_{t^{\prime}\in\mathit{Out}(q)}\mathbf{x}(t^{\prime}))-$
$\displaystyle-\sum_{q\in
Q_{p}\cap\\{p\\}}\sum_{t\in\mathit{Out}(q)}\mathbf{x}(t)$
$\displaystyle=\sum_{t\in\mathit{In}(p)\cap
T_{n}}\mathbf{x}(t)-\sum_{t\in\mathit{Out}(p)\cap
T_{n}}\mathbf{x}(t)+\sum_{q\in
Q_{p}}\sum_{t\in\mathit{Out}(q)\cap\mathit{In}(p)}\mathbf{x}(t)-\sum_{q\in
Q_{p}\cap\\{p\\}}\sum_{t\in\mathit{Out}(q)}\mathbf{x}(t)$
$\displaystyle=\sum_{t\in\mathit{In}(p)\cap
T_{n}}\mathbf{x}(t)-\sum_{t\in\mathit{Out}(p)\cap
T_{n}}\mathbf{x}(t)+\sum_{t\in
T_{p}\cap\mathit{In}(p)}\mathbf{x}(t)-\sum_{q\in
Q_{p}\cap\\{p\\}}\sum_{t\in\mathit{Out}(q)}\mathbf{x}(t)$

If $p\in Q_{n}$, then this becomes

$\displaystyle\sum_{t\in\mathit{In}(p)\cap
T_{n}}\mathbf{x}(t)-\sum_{t\in\mathit{Out}(p)\cap
T_{n}}\mathbf{x}(t)+\sum_{t\in
T_{p}\cap\mathit{In}(p)}\mathbf{x}(t)-\sum_{q\in
Q_{p}\cap\\{p\\}}\sum_{t\in\mathit{Out}(q)}\mathbf{x}(t)=$
$\displaystyle=\sum_{t\in\mathit{In}(p)\cap
T_{n}}\mathbf{x}(t)-\sum_{t\in\mathit{Out}(p)\cap
T_{n}}\mathbf{x}(t)+\sum_{t\in T_{p}\cap\mathit{In}(p)}\mathbf{x}(t)-0=$
$\displaystyle=\sum_{t\in\mathit{In}(p)}\mathbf{x}(t)-\sum_{t\in\mathit{Out}(p)\cap
T_{n}}\mathbf{x}(t)=\sum_{t\in\mathit{In}(p)}\mathbf{x}(t)-\sum_{t\in\mathit{Out}(p)}\mathbf{x}(t)=0$

with the last line being from (I). And if $p\in Q_{p}$, then it becomes

$\displaystyle\sum_{t\in\mathit{In}(p)\cap T_{n}}\mathbf{x}(t)-0+\sum_{t\in
T_{p}\cap\mathit{In}(p)}\mathbf{x}(t)-\sum_{q\in
Q_{p}\cap\\{p\\}}\sum_{t\in\mathit{Out}(q)}\mathbf{x}(t)=$
$\displaystyle=\sum_{t\in\mathit{In}(p)\cap T_{n}}\mathbf{x}(t)+\sum_{t\in
T_{p}\cap\mathit{In}(p)}\mathbf{x}(t)-\sum_{t\in\mathit{Out}(p)}\mathbf{x}(t)=$
$\displaystyle=\sum_{t\in\mathit{In}(p)}\mathbf{x}(t)-\sum_{t\in\mathit{Out}(p)}\mathbf{x}(t)=0$

with the last line being from (I). Therefore $\mathbf{x}^{\prime}$ is a
solution of (I’)

The second half (II’): Let $\mathbf{y},\mathbf{z}$ be a solution of (II) we
will show that $\mathbf{y},\mathbf{z}$ is also a solution of (II’).

From (II) we have for each $t=(p,\mathbf{u},q)\in T_{n}$ that

$\displaystyle\mathbf{z}(q)-\mathbf{z}(p)+\sum_{i=1}^{d}\mathbf{u}(i)\mathbf{y}(i)=$
$\displaystyle=\mathbf{z}(q)\cdot\mathit{next}_{t}(q)-\mathbf{z}(p)\cdot\mathit{from}_{t}(p)+\sum_{i=1}^{d}\mathit{effect}_{t}(i)\mathbf{y}(i)=$
$\displaystyle=\sum_{r\in
Q}\mathbf{z}(r)\cdot\mathit{next}_{t}(r)-\mathbf{z}(r)\cdot\mathit{from}_{t}(r))+\sum_{i=1}^{d}\mathit{effect}_{t}(i)\mathbf{y}(i)\leq
0$

Where we used that $\mathit{next}_{t}(r)=0$ for every $r\neq q$, and
$\mathit{from}_{t}(r)=0$ for every $r\neq p$.

Additionally, From (II) we also have for each $p\in Q_{p}$ that

$\displaystyle\sum_{t=(p,\mathbf{u},q)\in\mathit{Out}(p)}P(t)\big{(}\mathbf{z}(q)-\mathbf{z}(p)+\sum_{i=1}^{d}\mathbf{u}_{t}(i)\mathbf{y}(i)\big{)}=$
$\displaystyle=-\mathbf{z}(p)+\sum_{t=(p,\mathbf{u},q)\in\mathit{Out}(p)}P(t)\big{(}\mathbf{z}(q)+\sum_{i=1}^{d}\mathbf{u}_{t}(i)\mathbf{y}(i)\big{)}=$
$\displaystyle=-\mathbf{z}(p)+\sum_{q\in
Q}\sum_{t\in\mathit{Out}(p)\cap\mathit{In}(q)}P(t)\big{(}\mathbf{z}(q)+\sum_{i=1}^{d}\mathbf{u}_{t}(i)\mathbf{y}(i)\big{)}=$
$\displaystyle=-\mathbf{z}(p)+\sum_{q\in
Q}\sum_{t\in\mathit{Out}(p)\cap\mathit{In}(q)}P(t)\mathbf{z}(q)+\sum_{t\in\mathit{Out}(p)}P(t)\big{(}\sum_{i=1}^{d}\mathbf{u}_{t}(i)\mathbf{y}(i)\big{)}=$
$\displaystyle=-\mathbf{z}(p)+\sum_{q\in
Q}\mathbf{z}(q)\sum_{t\in\mathit{Out}(p)\cap\mathit{In}(q)}P(t)+\sum_{i=1}^{d}\mathbf{y}(i)\cdot(\sum_{t\in\mathit{Out}(p)}P(t)\mathbf{u}_{t}(i))=$
$\displaystyle=-\mathbf{z}(p)\cdot\mathit{from}_{p}(p)+\sum_{q\in
Q}\mathbf{z}(q)\cdot\mathit{next}_{p}(q)+\sum_{i=1}^{d}\mathbf{y}(i)\cdot\mathit{effect}_{p}(i)=$
$\displaystyle=\sum_{q\in
Q}(\mathbf{z}(q)\cdot\mathit{next}_{p}(q)-\mathbf{z}(q)\cdot\mathit{from}_{p}(q))+\sum_{i=1}^{d}\mathbf{y}(i)\cdot\mathit{effect}_{p}(i)\leq
0$

Therefore $\mathbf{y},\mathbf{z}$ is also a solution to (II’)

We will now rewrite the constraint systems (I’) and (II’) into matrix form.
Let $D$ be a $A\times\\{1,\dots,d\\}$ matrix whose columns are indexed by
elements of $A$, and rows indexed by counters $c\in\\{1,\dots,d\\}$, such that
the column $D(a)=\mathit{effect}_{a}$. And let $F$ be a $A\times Q$ matrix,
whose columns are indexed by elements of $A$, and rows are indexed by states
$p\in Q$, such that the column $F(a)$ is equal to the vector $\mathbf{w}$ such
that $\mathbf{w}(p)=\mathit{next}_{a}(p)-\mathit{from}_{a}(p)$ for each $p\in
Q$.

Then we can further rewrite the systems (I’) and (II’) as follows:

constraint system (I’): Find $\mathbf{x}^{\prime}\in\mathbb{Z}^{A}$ such that $\displaystyle D\mathbf{x}^{\prime}$ $\displaystyle\geq\vec{0}$ $\displaystyle\mathbf{x}^{\prime}$ $\displaystyle\geq\vec{0}$ $\displaystyle F\mathbf{x}^{\prime}$ $\displaystyle=\vec{0}$ |  constraint system (II’): Find $\mathbf{y}\in\mathbb{Z}^{d},\mathbf{z}\in\mathbb{Z}^{Q}$ with $\displaystyle\mathbf{y}$ $\displaystyle\geq\vec{0}$ $\displaystyle\mathbf{z}$ $\displaystyle\geq\vec{0}$ $\displaystyle F^{T}\mathbf{z}+D^{T}\mathbf{y}$ $\displaystyle\leq\vec{0}$
---|---

The rest then follows exactly the same as the the proof of the dichotomy on
non-stochastic VASS in [23] (Lemma 4), as the only difference between our
systems and the ones used in [23] is that the matrix $F$ now also may contain
rational numbers other than $-1,0,1$. The proof in [23] is already made over
$\mathbb{Z}$, and the only additional requirement it needs is that each column
of $F$ sums up to $0$, which is satisfied also by our $F$.

###  A.2 The proof from [23] (Lemma 4)

######  Disclaimer.

For the sake of completeness we include a copy of the proof from [23] (Lemma
4). All credit for the proof in this subsection goes to the author of [23].
The only changes we made was to rename some variables.

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

there exists $x$ with $\begin{array}[]{rcr}Ax&\geq&b\\\ Cx&=&d\end{array}$ |  there exist $y,z$ with $\begin{array}[]{rcr}y&\geq&0\\\ A^{T}y+C^{T}z&=&0\\\ b^{T}y+d^{T}z&>&0\end{array}$
---|---

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

constraint system ($A_{a}$): there exists $x\in\mathbb{Z}^{A}$ with $\displaystyle Ux$ $\displaystyle\geq 0$ $\displaystyle x$ $\displaystyle\geq 0$ $\displaystyle Fx$ $\displaystyle=0$ $\displaystyle x(a)$ $\displaystyle\geq 1$ (1) |  constraint system ($B_{a}$): there exist $y\in\mathbb{Z}^{d},z\in\mathbb{Z}^{Q(\mathit{B})}$ with $\displaystyle y$ $\displaystyle\geq 0$ $\displaystyle z$ $\displaystyle\geq 0$ $\displaystyle U^{T}y+F^{T}z$ $\displaystyle\leq 0\text{ with }<0\text{ in line }a$ (2)
---|---

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

######  Lemma A.3.

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

######  Proof A.4.

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

constraint system ($A_{a}^{\prime}$): |  $\displaystyle\begin{pmatrix}U\\\ Id\end{pmatrix}x$ $\displaystyle\geq$ $\displaystyle\begin{pmatrix}0\\\ \mathtt{char}_{a}\end{pmatrix}$ $\displaystyle Fx$ $\displaystyle=$ $\displaystyle 0$
---|---

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

constraint system ($B_{a}^{\prime}$): $\displaystyle\begin{pmatrix}y\\\ k\end{pmatrix}$ $\displaystyle\geq$ $\displaystyle 0$ $\displaystyle\begin{pmatrix}U\\\ Id\end{pmatrix}^{T}\begin{pmatrix}y\\\ k\end{pmatrix}+F^{T}z$ $\displaystyle=$ $\displaystyle 0$ $\displaystyle\begin{pmatrix}0\\\ \mathtt{char}_{a}\end{pmatrix}^{T}\begin{pmatrix}y\\\ k\end{pmatrix}+0^{T}z$ $\displaystyle>$ $\displaystyle 0$ |  constraint system ($B_{a}^{\prime}$) simplified: $\displaystyle y$ $\displaystyle\geq$ $\displaystyle 0$ $\displaystyle k$ $\displaystyle\geq$ $\displaystyle 0$ $\displaystyle U^{T}y+k+F^{T}z$ $\displaystyle=$ $\displaystyle 0$ $\displaystyle k(a)$ $\displaystyle>$ $\displaystyle 0$
---|---

We observe that solutions of constraint system ($B_{a}^{\prime}$) are
invariant under shifts of $z$, i.e, if $y$, $k$, $z$ is a solution, then $y$,
$k$, $z+c\cdot\mathbf{1}$ is also a solution for all $c\in\mathbb{Z}$ (because
elements of every row of $F^{T}$ sum up to $0$). Hence, we can force $z$ to be
non-negative. We recognize that constraint systems ($B_{a}^{\prime}$) and
($B_{a}$) are equivalent. ∎

We now consider the constraint systems ($C_{c}$) and ($D_{c}$) stated below.
Both constraint systems are parameterized by a counter $c$ (we note that only
Equations (3) and (4) are parameterized by $c$).

constraint system ($C_{c}$): there exists $x\in\mathbb{Z}^{A}$ with $\displaystyle Ux$ $\displaystyle\geq 0\text{ with }\geq 1\text{ in line }c$ (3) $\displaystyle x$ $\displaystyle\geq 0$ $\displaystyle Fx$ $\displaystyle=0$ |  constraint system ($D_{c}$): there exist $y\in\mathbb{Z}^{d},z\in\mathbb{Z}^{Q(\mathit{B})}$ with $\displaystyle y$ $\displaystyle\geq 0$ $\displaystyle z$ $\displaystyle\geq 0$ $\displaystyle U^{T}y+F^{T}z$ $\displaystyle\leq 0$ $\displaystyle y(c)$ $\displaystyle>0$ (4)
---|---

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

######  Lemma A.5.

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

######  Proof A.6.

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

constraint system ($C_{c}^{\prime}$): |  $\displaystyle\begin{pmatrix}U\\\ Id\end{pmatrix}x$ $\displaystyle\geq$ $\displaystyle\begin{pmatrix}\mathtt{char}_{c}\\\ 0\end{pmatrix}$ $\displaystyle Fx$ $\displaystyle=$ $\displaystyle 0$
---|---

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

constraint system ($D_{c}^{\prime}$): $\displaystyle\begin{pmatrix}y\\\ k\end{pmatrix}$ $\displaystyle\geq$ $\displaystyle 0$ $\displaystyle\begin{pmatrix}U\\\ Id\end{pmatrix}^{T}\begin{pmatrix}y\\\ k\end{pmatrix}+F^{T}z$ $\displaystyle=$ $\displaystyle 0$ $\displaystyle\begin{pmatrix}\mathtt{char}_{c}\\\ 0\end{pmatrix}^{T}\begin{pmatrix}y\\\ k\end{pmatrix}+0^{T}z$ $\displaystyle>$ $\displaystyle 0$ |  constraint system ($B_{a}^{\prime}$) simplified: $\displaystyle y$ $\displaystyle\geq$ $\displaystyle 0$ $\displaystyle k$ $\displaystyle\geq$ $\displaystyle 0$ $\displaystyle U^{T}y+k+F^{T}z$ $\displaystyle=$ $\displaystyle 0$ $\displaystyle y(c)$ $\displaystyle>$ $\displaystyle 0$
---|---

We observe that solutions of constraint system ($D_{c}^{\prime}$) are
invariant under shifts of $z$, i.e, if $y$, $k$, $z$ is a solution, then $y$,
$k$, $z+c\cdot\mathbf{1}$ is also a solution for all $c\in\mathbb{Z}$ (because
elements of every row of $F^{T}$ sum up to $0$). Hence, we can force $z$ to be
non-negative. We recognize that constraint systems ($D_{c}^{\prime}$) and
($D_{c}$) are equivalent. ∎

###  A.3 Proof of Lemma 4.4

######  Lemma (4.4).

For every counter $c$ such that $\mathbf{y}(c)>0$, every $\varepsilon>0$,
every $p\in Q$, and every $\sigma\in\Sigma$, there exists $n_{0}$ such that
for all $n\geq n_{0}$ we have that where $k$ is a constant depending only on
$\pazocal{A}$.

Let $P_{1}V_{1},P_{2}V_{2},\dots$ be the random variables encoding the
computation under $\sigma$ from $p\mathbf{n}$ (i.e. $P_{i}V_{i}$ represents
the configuration at $i$-th step of the computation). And let
$R_{1},R_{2},\dots$ represent the value of $rank$ at $i-$th step (i.e.
$R_{i}=rank(P_{i}V_{i})$). Then $R_{1},R_{2},\dots$ is a supermartingale.

######  Lemma A.7.

$R_{1},R_{2},\dots$ is a supermartingale.

######  Proof A.8.

One can express $R_{i+1}=R_{i}+X_{i+1}$, where $X_{i+1}=R_{i+1}-R_{i}$ is the
change of $rank$ in the $(i+1)$-st step. Then it holds
$\mathbb{E}^{\sigma}_{p\vec{n}}(R_{i+1}|R_{i})=\mathbb{E}^{\sigma}_{p\vec{n}}(R_{i}|R_{i})+\mathbb{E}^{\sigma}_{p\vec{n}}(X_{i+1}|R_{i})=R_{i}+\mathbb{E}^{\sigma}_{p\vec{n}}(X_{i+1}|R_{i})$.
We want to show that $\mathbb{E}^{\sigma}_{p\vec{n}}(X_{i+1}|R_{i})\leq 0$.
Let $T_{i+1}$ be random variable representing the transition taken at
$(i+1)$-st step. Then
$\mathbb{E}^{\sigma}_{p\vec{n}}(X_{i+1}|R_{i})=\sum_{t\in T}$ where
$\mathit{RankEff}(t)$ represents the change of $rank$ under transition $t$.

Let $T_{n}=\bigcup_{p\in Q_{n}}\mathit{Out}(p)$ and $T_{p}=\bigcup_{p\in
Q_{p}}\mathit{Out}(p)$ , then we can write
$\mathbb{E}^{\sigma}_{p\vec{n}}(X_{i+1}|R_{i})=\sum_{t\in T_{p}}$.

Since for each $t=(p,\mathbf{u},q)\in T$ it holds
$\mathit{RankEff}(t)=\mathbf{z}(q)-\mathbf{z}(p)+\sum_{i=1}^{d}\mathbf{y}(i)\mathbf{u}(i)$,
for each $t\in T_{n}$ it holds $\mathit{RankEff}(t)\leq 0$, and for each $p\in
Q_{n}$, it holds $\sum_{t\in\mathit{Out}(p)}P(t)\mathit{RankEff}(t)\leq 0$.
Therefore we can write

$\sum_{t\in T_{p}}$

and

$\sum_{t\in T_{n}}$

Thus $E(X_{i+1}|R_{i})\leq 0$

Now let us consider the stopping rule $\tau$ that stops when either any
counter reaches $0$, or any counter $c$ with $\mathbf{y}(c)>0$ becomes larger
then $n^{1+\epsilon}$ for the first time. (i.e. either
$V_{\tau}(c^{\prime})<0$ for any $c^{\prime}\in\\{1,\dots,d\\}$, or
$V_{\tau}(c)\geq n^{1+\epsilon}$ for $c$ with $\mathbf{y}(c)>0$). Then for all
$i$, it holds that $R_{min(i,\tau)}\leq max_{p\in
Q}\mathbf{z}(p)+max_{c\in\\{1,\dots,d\\}}\mathbf{y}(c)\cdot
d\cdot(n^{1+\epsilon}+u)$, where $u$ is the maximal increase of a counter in a
single transition. Therefore we can apply optional stopping theorem to obtain:

$max_{p\in Q}\mathbf{z}(p)+max_{c\in\\{1,\dots,d\\}}\mathbf{y}(c)\cdot d\cdot
n\geq E(R_{1})\geq E(R_{\tau})\geq pX_{n^{1+\epsilon}}+(1-p)X_{0}$

where $X_{n^{1+\epsilon}}$ represents the minimal possible value of $R_{\tau}$
if any counter $c$ with $\mathbf{y}(c)>0$ has $R_{\tau}(c)\geq
n^{1+\epsilon}$, $p$ is the probability of any such counter being at least
$n^{1+\epsilon}$ upon stopping, and $X_{0}$ represents the minimal value of
$R_{\tau}$ if no such counter reached $n^{1+\epsilon}$. We can simplify this
as

$max_{p\in Q}\mathbf{z}(p)+max_{c\in\\{1,\dots,d\\}}\mathbf{y}(c)\cdot d\cdot
n\geq pX_{n^{1+\epsilon}}+(1-p)X_{0}$ $max_{p\in
Q}\mathbf{z}(p)+max_{c\in\\{1,\dots,d\\}}\mathbf{y}(c)\cdot d\cdot
n-(1-p)\cdot X_{0}\geq pX_{n^{1+\epsilon}}$ $max_{p\in
Q}\mathbf{z}(p)+max_{c\in\\{1,\dots,d\\}}\mathbf{y}(c)\cdot d\cdot
n-(1-p)max_{c\in\\{1,\dots,d\\}}\mathbf{y}(c)\cdot d\cdot u\geq
pX_{n^{1+\epsilon}}$ $max_{p\in
Q}\mathbf{z}(p)+max_{c\in\\{1,\dots,d\\}}\mathbf{y}(c)\cdot d\cdot
n-max_{c\in\\{1,\dots,d\\}}\mathbf{y}(c)\cdot d\cdot u+p\cdot
max_{c\in\\{1,\dots,d\\}}\mathbf{y}(c)\cdot d\cdot u\geq pX_{n^{1+\epsilon}}$
$max_{p\in Q}\mathbf{z}(p)+max_{c\in\\{1,\dots,d\\}}\mathbf{y}(c)\cdot d\cdot
n-max_{c\in\\{1,\dots,d\\}}\mathbf{y}(c)\cdot d\cdot u\geq
pX_{n^{1+\epsilon}}-p\cdot max_{c\in\\{1,\dots,d\\}}\mathbf{y}(c)\cdot d\cdot
u$ $max_{p\in Q}\mathbf{z}(p)+max_{c\in\\{1,\dots,d\\}}\mathbf{y}(c)\cdot
d\cdot n-max_{c\in\\{1,\dots,d\\}}\mathbf{y}(c)\cdot d\cdot u\geq
p(X_{n^{1+\epsilon}}-max_{c\in\\{1,\dots,d\\}}\mathbf{y}(c)\cdot d\cdot u)$
$\frac{max_{p\in Q}\mathbf{z}(p)+max_{c\in\\{1,\dots,d\\}}\mathbf{y}(c)\cdot
d\cdot n-max_{c\in\\{1,\dots,d\\}}\mathbf{y}(c)\cdot d\cdot
u}{X_{n^{1+\epsilon}}-max_{c\in\\{1,\dots,d\\}}\mathbf{y}(c)\cdot d\cdot
u}\geq p$ $\frac{max_{p\in
Q}\mathbf{z}(p)+max_{c\in\\{1,\dots,d\\}}\mathbf{y}(c)\cdot d\cdot
n-max_{c\in\\{1,\dots,d\\}}\mathbf{y}(c)\cdot d\cdot
u}{n^{1+\epsilon}-max_{c\in\\{1,\dots,d\\}}\mathbf{y}(c)\cdot d\cdot u}\geq p$

As for all sufficiently large $n$ it holds $0.5\cdot n^{1+\epsilon}\leq
n^{1+\epsilon}-max_{c\in\\{1,\dots,d\\}}\mathbf{y}(c)\cdot d\cdot u$ we have

$\frac{max_{p\in Q}\mathbf{z}(p)+max_{c\in\\{1,\dots,d\\}}\mathbf{y}(c)\cdot
d\cdot n-max_{c\in\\{1,\dots,d\\}}\mathbf{y}(c)\cdot d\cdot u}{0.5\cdot
n^{1+\epsilon}}\geq p$ $\frac{max_{p\in
Q}\mathbf{z}(p)-max_{c\in\\{1,\dots,d\\}}\mathbf{y}(c)\cdot d\cdot u}{0.5\cdot
n^{1+\epsilon}}+\frac{max_{c\in\\{1,\dots,d\\}}\mathbf{y}(c)\cdot d\cdot
n}{0.5\cdot n^{1+\epsilon}}\geq p$ $\frac{max_{p\in
Q}\mathbf{z}(p)-max_{c\in\\{1,\dots,d\\}}\mathbf{y}(c)\cdot d\cdot u}{0.5\cdot
n^{1+\epsilon}}+\frac{max_{c\in\\{1,\dots,d\\}}\mathbf{y}(c)\cdot d}{0.5\cdot
n^{\epsilon}}\geq p$

Also as $n^{1+\epsilon}\geq n^{\epsilon}$ we have

$\frac{max_{p\in Q}\mathbf{z}(p)-max_{c\in\\{1,\dots,d\\}}\mathbf{y}(c)\cdot
d\cdot u}{0.5\cdot
n^{\epsilon}}+\frac{max_{c\in\\{1,\dots,d\\}}\mathbf{y}(c)\cdot d}{0.5\cdot
n^{\epsilon}}\geq p$ $\frac{max_{p\in
Q}2\cdot\mathbf{z}(p)-max_{c\in\\{1,\dots,d\\}}2\cdot\mathbf{y}(c)\cdot d\cdot
u+max_{c\in\\{1,\dots,d\\}}2\cdot\mathbf{y}(c)\cdot d}{n^{\epsilon}}\geq p$

As $k=max_{p\in
Q}2\cdot\mathbf{z}(p)-max_{c\in\\{1,\dots,d\\}}2\cdot\mathbf{y}(c)\cdot d\cdot
u+max_{c\in\\{1,\dots,d\\}}2\cdot\mathbf{y}(c)\cdot d$ is a constant dependent
only on the VASS MDP, it holds for each counter $c$ with $\mathbf{y}(c)>0$ and
for all sufficiently large $n$ that .

###  A.4 Proof of Lemma 4.5

######  Lemma (4.5).

For each counter $c$ such that $\mathbf{y}(c)=0$ we have that
$\pazocal{C}_{\mathrm{exp}}[c]\in\Omega(n^{2})$ and $n^{2}$ is a lower
estimate of $\pazocal{C}[c]$. Furthermore, for every $\varepsilon>0$ there
exist a sequence of strategies $\sigma_{1},\sigma_{2},\dots$, a constant $k$,
and $p\in Q$ such that for every $0<\varepsilon^{\prime}<\varepsilon$, we have
that

$\lim_{n\to\infty}$

where
$\mathit{Target}_{n}=\\{q\mathbf{v}\in\mathit{C}(\pazocal{A})\mid\mathbf{v}(c)\geq
n^{2-\varepsilon}\mbox{ for every counter $c$ such that
$\mathbf{y}(c)=0$}\\}$.

Let $\pazocal{A}_{\mathbf{x}}$ be the VASS MDP induced by transitions $t$ with
$\mathbf{x}(t)>0$.

######  Lemma A.9.

In $\pazocal{A}_{\mathbf{x}}$, Each pair of states $p,q\in Q$ is either a part
of the same MEC of $\pazocal{A}_{\mathbf{x}}$, or $p$ is not reachable from
$q$ and vice-versa, in $\pazocal{A}_{\mathbf{x}}$.

######  Proof A.10.

This follows directly from $\mathbf{x}$ satisfying kirhoff laws.

Therefore $\pazocal{A}_{\mathbf{x}}$ can be decomposed into multiple MECs, and
there are no transitions in the MEC decomposition of
$\pazocal{A}_{\mathbf{x}}$. Let these MECs be $B_{1},\dots,B_{k}$, and let
$\mathbf{x}_{1},\dots,\mathbf{x}_{k}$ be the restriction of $\mathbf{x}$ to
the transitions of $B_{1},\dots,B_{k}$. (i.e.
$\mathbf{x}_{i}(t)=\mathbf{x}(t)$ if $B_{i}$ contains $t$, and otherwise
$\mathbf{x}_{i}(t)=0$).

For each $1\leq i\leq k$, let
$\overline{\mathbf{x}}_{i}=\frac{\mathbf{x}_{i}}{\sum_{t\in
T}\mathbf{x}_{i}(t)}$ be the normalized vector of $\mathbf{x}_{i}$, and let
$\sigma_{i}$ be a Markovian strategy for $B_{i}$ such that
$\sigma_{i}(p)(t)=\frac{\overline{\mathbf{x}}_{i}(t)}{\sum_{t\in\mathit{Out}(p)}\overline{\mathbf{x}}_{i}(t)}$
for $t$ such that $\sum_{t\in\mathit{Out}(p)}\overline{\mathbf{x}}_{i}(t)>0$,
and undefined otherwise. We will use $M_{i}$ to represent the Markov chain
obtained by applying $\sigma_{i}$ to $B_{i}$.

######  Lemma A.11.

Let $m_{i}\in\mathbb{Z}^{Q}$ be such that
$m_{i}(p)=\sum_{t\in\mathit{Out}(p)}\overline{\mathbf{x}}_{i}(t)$. Then
$m_{i}$ is an invariant distribution on $M_{i}$. Also the expected effect of a
single computational step in $M_{i}$ taken from distribution $m_{i}$ is equal
to $\sum_{(p,\mathbf{u},q)\in
T}\overline{\mathbf{x}}_{i}((p,\mathbf{u},q))\mathbf{u}$.

######  Proof A.12.

Let us consider a single computation step in $M_{i}$ taken from distribution
$m_{i}$, and let $X$ be resulting distribution on transitions during this
step. Then for each transition $t=(p,\mathbf{u},q)\in T$ it holds:

  * •

if $p\in Q_{p}$ then $X(t)=P(t)\cdot
m_{i}(p)=P(t)\cdot\sum_{t\in\mathit{Out}(p)}\overline{\mathbf{x}}_{i}(t)=\overline{\mathbf{x}}_{i}(t)$.

  * •

if $p\in Q_{n}$ then $X(t)=\sigma_{i}(p)(t)\cdot
m_{i}(p)=\frac{\overline{\mathbf{x}}_{i}(t)}{\sum_{t\in\mathit{Out}(p)}\overline{\mathbf{x}}_{i}(t)}\cdot\sum_{t\in\mathit{Out}(p)}\overline{\mathbf{x}}_{i}(t)=\overline{\mathbf{x}}_{i}(t)$.

And as the next distribution $m_{i}^{\prime}$ on states can be expressed as
$m_{i}^{\prime}(p)=\sum_{(q,\mathbf{u},p)\in
T}X((q,\mathbf{u},p))=\sum_{(q,\mathbf{u},p)\in
T}\overline{\mathbf{x}}_{i}((q,\mathbf{u},p))=\sum_{t\in\mathit{Out}(p)}\overline{\mathbf{x}}_{i}(t)=m_{i}(p)$,
$m_{i}$ is an invariant distribution on $M_{i}$.

Let $\mathbf{j}_{1},\dots,\mathbf{j}_{k}$ be the expected update vectors per
single computational step generated by the invariants in $M_{1},\dots,M_{k}$.
Then from $x$ being a solution to (I), we get that for $a_{i}=\sum_{t\in
T}x_{i}(t)$ it holds

$\sum_{i=1}^{k}a_{i}\cdot\mathbf{i}_{i}\geq\vec{0}$

as well as

$(\sum_{i=1}^{k}a_{i}\cdot\mathbf{i}_{i})(c)>0$

for $c$ with $\mathbf{y}(c)=0$.

Therefore we can use the results of [2], which states that if there exists a
sequence of Markov chains $M_{1},\dots,M_{k}$ with their respective increments
$\mathbf{j}_{1},\dots,\mathbf{j}_{k}$, and positive integer coefficients
$a_{1},\dots,a_{k}$ such that $\sum_{i=1}^{k}a_{i}\mathbf{j}_{i}\geq\vec{0}$,
then there exists a function $L(n)\in\Theta(n)$, a state $p\in Q$, and
sequence of strategies $\sigma_{1},\sigma_{2},\dots$ such that the probability
$X_{n}$ of the computation from $p\mathbf{n}$ under $\sigma_{n}$ never
decreasing at each of the first $L^{2-\epsilon^{\prime}}(n)$ steps any counter
below $b_{1}n\mathbb{E}_{p\vec{n}}^{\sigma_{n}}(C_{i}^{n}(c))-b_{2}n$, where
$b_{1},b_{2}$ are some constants and $C_{i}^{n}$ is the random variable
representing the counter vector after $i$ steps when computing form
$p\mathbf{n}$ under $\sigma_{n}$, satisfies
$\lim_{n\rightarrow\infty}X_{n}=1$. And furthermore, for each counter $c$ with
$(\sum_{i=1}^{k}a_{i}\mathbf{j}_{i})(c)>0$ it holds that
$\mathbb{E}_{p\vec{n}}^{\sigma_{n}}(C_{i}^{n}(c))\in\Omega(i)$.

Therefore, with probability at least $X_{n}$ we reach a configuration
$q\mathbf{v}$ with each counter $c$ such that $\mathbf{y}(c)=0$ having
$\mathbf{v}(c)\geq n^{2-\epsilon}$ within $L^{2-\epsilon^{\prime}}(n)\leq
kn^{2-\epsilon^{\prime}}$ steps, and it holds
$\lim_{n\rightarrow\infty}X_{n}=1$.

###  A.5 VASS MDP with DAG-like MEC Decomposition

We formalize and prove the idea sketched at the end of Section 4.

######  Lemma A.13.

Let $\pazocal{A}$ be a DAG-like VASS MDP with $d$ counters and a DAG-like MEC
decomposition, and $\beta=M_{1},\dots,M_{k}$ be it’s type. Let
$\mathbf{w}_{0},\mathbf{w}_{1},\dots,\mathbf{w}_{k}\in\\{n,\infty\\}^{d}$, and
let $M_{i}^{\mathbf{w}_{i-1}}$ be the MEC obtained by taking $M_{i}$ and
changing the effect $\mathbf{u}$ of every transition to $\mathbf{u}^{\prime}$
such that for each $c\in\\{1,\dots,d\\}$,
$\mathbf{u}^{\prime}(c)=\mathbf{u}(c)$ if $\mathbf{w}_{i-1}(c)=n$, and
$\mathbf{u}^{\prime}(c)=0$ if $\mathbf{w}_{i-1}(c)=\infty$. Furthermore, let
the following hold for each counter $c\in\\{1,\dots,d\\}$ and $1\leq i\leq k$

  * •

$\mathbf{w}_{0}(c)=n$,

  * •

$\mathbf{w}_{i}(c)=n$ if both $\mathbf{w}_{i-1}(c)=n$ and $n$ is a tight
estimate of $c$ in $M_{i}^{\mathbf{w}_{i-1}}$,

  * •

$\mathbf{w}_{i}(c)=\infty$ if either $\mathbf{w}_{i-1}(c)=\infty$ or $n^{2}$
is a lower estimate of $c$ in $M_{i}^{\mathbf{w}_{i-1}}$.

Then for each $\epsilon>0$, there exists a sequence of strategies
$\sigma_{1}^{1},\sigma_{1}^{2},\dots,\sigma_{1}^{k},\sigma_{2}^{1},\dots,\sigma_{2}^{k},\sigma_{3}^{1},\dots$,
such that for each $1\leq i\leq k$, and each $n$, the computation under
$\sigma_{n}^{i}$ initiated in some state of $M_{i}$ with initial counter
vector $\mathbf{v}$ such that for each $c\in\\{1,\dots,d\\}$ it holds

  * •

$\mathbf{v}(c)\geq\lfloor\frac{n}{2^{i}}\rfloor$ if $\mathbf{w}_{i-1}(c)=n$,

  * •

$\mathbf{v}(c)\geq\lfloor(\frac{n}{2^{i}})^{2-\epsilon_{i-1}}/2^{i}\rfloor$ if
$\mathbf{w}_{i-1}(c)=\infty$,

reaches with probability $X_{n}$ a configuration of $M_{i}$ with counter
vector $\mathbf{u}$ such that for each $c\in\\{1,\dots,d\\}$ it holds

  * •

$\mathbf{u}(c)\geq\lfloor\frac{n}{2^{i+1}}\rfloor$ if $\mathbf{w}_{i}(c)=n$,

  * •

$\mathbf{u}(c)\geq\lfloor(\frac{n}{2^{i+1}})^{2-\epsilon_{i}}/2^{i+1}\rfloor$
if $\mathbf{w}_{i}(c)=\infty$,

where $\epsilon_{i}=\frac{i\epsilon}{k}$, and it holds
$\lim_{n\rightarrow\infty}X_{n}=1$. Furthermore, for each counter
$c\in\\{1,\dots,d\\}$, if $\mathbf{w}_{k}(c)=n$ then $n$ is a tight estimate
of $\pazocal{C}[c]$ for type $\beta$, and if $\mathbf{w}_{k}(c)=\infty$ then
$n^{2}$ is a lower estimate of $\pazocal{C}[c]$ for type $\beta$.

######  Proof A.14.

Proof by induction on $k$. Base case of $k=1$ holds from Lemma 4.5, and the
second part holds from Lemma 4.3. Assume now the Lemma holds for the type
$M_{1},\dots,M_{i-1}$. Let $\sigma_{1},\sigma_{2},\dots$ and $p\in Q$ be from
the Lemma 4.5 for $M_{i}^{\mathbf{w}_{i-1}}$ and for $\epsilon_{i}$. Then from
induction assumption, there are strategies such that when the computation
reaches $M_{i}$ the counters vector is $\mathbf{v}$ with probability $Y_{i}$
such that $\lim_{n\rightarrow\infty}Y_{n}=1$ and

  * •

$\mathbf{v}(c)\geq\lfloor\frac{n}{2^{i}}\rfloor$ if $\mathbf{w}_{i-1}(c)=n$,

  * •

$\mathbf{v}(c)\geq\lfloor(\frac{n}{2^{i}})^{2-\epsilon_{i-1}}/2^{i}\rfloor$ if
$\mathbf{w}_{i-1}(c)=\infty$.

Now let us consider the following: upon reaching $M_{i}$, we divide the
counters vector $\mathbf{v}$ into two halves, each of size
$\lfloor\frac{\mathbf{v}}{2}\rfloor$, and then we perform the computation of
$\sigma_{\lfloor\frac{n}{2^{i+1}}\rfloor}$ on the first half for
$ln^{2-\frac{(i+0.5)\epsilon}{k}}$ steps. (i.e., if the effect on any counter
$c$ is less then $-\lfloor\frac{\mathbf{v}}{2}\rfloor(c)$, then the
computation stops). Then from Lemma 4.5 we will with probability $X_{n}$ reach
a configuration $\mathbf{u}$ with all counters $c$ such that
$\mathbf{w}_{i-1}(c)=n$ and $\mathbf{w}_{i}(c)=\infty$ being at least
$\mathbf{u}(c)\geq(\lfloor\frac{n}{2^{i+1}}\rfloor)^{2-\epsilon_{i}}$, such
that $\lim_{n\rightarrow\infty}X_{n}=1$. As the length of this computation is
only $ln^{2-\frac{(i+0.5)\epsilon}{k}}$ we cannot decrease any "deleted"
counter $c$ with $\mathbf{w}_{i-1}(c)=\infty$ by more then
$an^{2-\frac{(i+0.5)\epsilon}{k}}$ for some constant $a$. Therefore for all
sufficiently large $n$, the computation cannot terminate due to such counter
being depleted. And since the second half of $\mathbf{v}$ is untouched, we
still have for each counter $c$ with $\mathbf{w}_{i-1}(c)=\infty$ at least
$\lfloor(\frac{n}{2^{i}})^{2-\epsilon_{i-1}}/2^{i+1}\rfloor$ and for each
counter $c$ with $\mathbf{w}_{i-1}(c)=n$ at least
$\lfloor\frac{n}{2^{i+1}}\rfloor$.

Therefore with probability at least $X_{n}Y_{n}$ the computation ends in
configuration $q\mathbf{u}$ of $M_{i}$ such that for each counter $c$

  * •

$\mathbf{u}(c)\geq\lfloor\frac{n}{2^{i+1}}\rfloor$ if $\mathbf{w}_{i}(c)=n$,

  * •

$\mathbf{u}(c)\geq\lfloor(\frac{n}{2^{i+1}})^{2-\epsilon_{i}}/2^{i+1}\rfloor$
if $\mathbf{w}_{i}(c)=\infty$

And it holds $\lim_{n\rightarrow\infty}X_{n}Y_{n}=1$. Thus $n^{2}$ is a lower
estimate of $\pazocal{C}[c]$ for type $M_{1},\dots,M_{i}$ for each $c$ with
$\mathbf{w}_{i}(c)=\infty$.

For the second part of the lemma, let $\sigma$ be some strategy. Then for
every counter $c$ with $\mathbf{w}_{i}(c)=n$, we have from the induction
assumption that the probability, of the strategy $\sigma$ started in initial
configuration $p\vec{n}$, reaching $M_{i}$ along type $M_{1},\dots,M_{i}$ with
$c$ being at least $n^{1+\epsilon^{\prime}}$ for some $0<\epsilon^{\prime}$,
is at most $Z_{n}$, where $\limsup_{n\to\infty}Z_{n}=0$. Let
$\sigma^{\prime}$be a strategy, which for an initial state $q$ such that $q$
is a state of $M_{1}$, computes as $\sigma$ after a path from $p$ to $q$. Then
from Lemma 4.4 we have for each $0<\hat{\epsilon}$ that

$\prob{}^{\sigma^{\prime}}_{qn^{1+\epsilon^{\prime}}}(\pazocal{C}_{M_{i}^{\mathbf{w}_{i-1}}}[c]\geq
n^{1+\hat{\epsilon}})=\prob{}^{\sigma^{\prime}}_{qn^{1+\epsilon^{\prime}}}(\pazocal{C}_{M_{i}^{\mathbf{w}_{i-1}}}[c]\geq(n^{1+\epsilon^{\prime}})^{\log_{n^{1+\epsilon^{\prime}}}n^{1+\hat{\epsilon}}})\leq
kn^{1-\log_{n^{1+\epsilon^{\prime}}}n^{1+\hat{\epsilon}}}$

Let $y=1-\log_{n^{1+\epsilon^{\prime}}}n^{1+\hat{\epsilon}}$, note that for
$\epsilon^{\prime}<\hat{\epsilon}$ it holds $y<0$. Also let $R_{q}=$. Then we
can write for each $\epsilon^{\prime}<\hat{\epsilon}<\epsilon$

$\prob{}^{\sigma}_{p\vec{n}}(\pazocal{C}[c]\geq
n^{1+\epsilon}\mid\mathit{mecs}{=}M_{1},\dots,M_{i})\leq\\\
\leq\prob{}^{\sigma}_{p\vec{n}}(\pazocal{C}[c]\geq
n^{1+\epsilon^{\prime}}\mid\mathit{mecs}{=}M_{1},\dots,M_{i-1})+\sum_{q\in
Q}R_{q}\prob{}^{\sigma^{\prime}}_{qn^{1+\epsilon^{\prime}}}(\pazocal{C}_{M_{i}^{\mathbf{w}_{i-1}}}[c]\geq
n^{1+\hat{\epsilon}})\leq Z_{n}+kn^{y}$

And since $\lim_{n\rightarrow\infty}Z_{n}+kn^{y}=0$, and
$\epsilon^{\prime},\hat{\epsilon}$ can be arbitrarily small, we can find
values for them for arbitrary $\epsilon>0$. Thus $n$ is a tight estimate of
$\pazocal{C}[c]$ for type $M_{1},\dots,M_{i}$.

##  Appendix B Proofs for Section 5

######  Lemma B.1.

Given a one-dimesional VASS MDP, deciding existence of an increasing BSCC
$\mathbb{B}$ of $\pazocal{A}_{\sigma}$ for some
$\sigma\in\Sigma_{\mathrm{MD}}$ can be done in $\mathbf{P}$.

######  Proof B.2.

If such BSCC exists, then it gives us a solution $\mathbf{x}$ with
$\sum_{(p,\mathbf{u},q)\in T}\mathbf{x}((p,\mathbf{u},q))\mathbf{u}(c)>0$ for
(I). The solution is such that if $\mathbf{w}$ is the invariant distribution
on states of $\mathbb{B}$ under $\sigma$, then for each transition
$(p,\mathbf{u},q)$ contained in $\mathbb{B}$,
$\mathbf{x}((p,\mathbf{u},q))=\mathbf{w}(p)$ if $p\in Q_{n}$ is a non-
deterministic state, and
$\mathbf{x}((p,\mathbf{u},q))=\mathbf{w}(p)P((p,\mathbf{u},q))$ if $p\in
Q_{p}$ is a probabilistic state, while $\mathbf{x}(t)=0$ for each $t$ that is
not contained in $\mathbb{B}$. And every solution $\mathbf{x}$ of (I) such
that $\sum_{(p,\mathbf{u},q)\in T}\mathbf{x}((p,\mathbf{u},q))\mathbf{u}(c)>0$
can be used to extract a strategy with expected positive effect on the counter
(Appendix A: Lemma A.11). But this is only possible if there exists an
increasing BSCC $\mathbb{B}$ of $\pazocal{A}_{\sigma}$ for some
$\sigma\in\Sigma_{\mathrm{MD}}$, as these are the extremal values of any
strategy.333Here we rely on well-known results about finite-state MDPs [20].

######  Lemma B.3.

Given a one-dimensional VASS MDP, if there exists an increasing BSCC
$\mathbb{B}$ of $\pazocal{A}_{\sigma}$ for some
$\sigma\in\Sigma_{\mathrm{MD}}$, then $\pazocal{C}[c]$ and $\pazocal{L}$ are
unbounded in type $M$ such that $\mathbb{B}\subseteq M$. Furthermore, let
$M[t]$ be the MEC containing the transition $t$. If $M[t]$ exists and
$\mathbb{B}\subseteq M[t]$, then $\pazocal{T}[t]$ is unbounded for type
$M[t]$. Additionally, $\pazocal{T}[t]$ is also unbounded for each type
$\beta=M_{1},\dots,M_{k}$ such that there exist $j\leq i$ such that
$M_{i}=M[t]$ and $\mathbb{B}\subseteq M_{j}$.

The computation under $\sigma$ from any state of $\mathbb{B}$ has a tendency
to increase the counter, and as $n$ goes towards $\infty$ the probability of
the computation terminating goes to $0$.444For formal proof see e.g. [2]
(Lemma 6) Therefore both $\pazocal{C}[c]$ and $\pazocal{L}$ are unbounded for
type $M$ with $\mathbb{B}\subseteq M$. Furthermore, if $\mathbb{B}\subseteq
M[t]$, then $t$ can be iterated infinitely often with high probability by
periodically “deviating” from $\sigma$ by temporarily switching to some other
strategy which never leaves $M[t]$ and has positive chance of using $t$.
Clearly this can be done in such a way that the overall strategy still has the
tendency to increase the counter. Therefore in such case $\pazocal{T}[t]$ is
unbounded for type $M[t]$. The last part of the theorem comes from the fact
that we can first pump the counter in $M_{j}$ to an arbitrarily large value,
before moving to $M[t]$ where we then can iterate any strategy on $M[t]$ that
has positive chance of using $t$.

######  Lemma B.4.

Given a one-dimensional VASS MDP, if there exists an unbounded-zero BSCC
$\mathbb{B}$ of $\pazocal{A}_{\sigma}$ for some
$\sigma\in\Sigma_{\mathrm{MD}}$, then
$\pazocal{L}_{\mathrm{exp}}\in\Omega(n^{2})$ and $n^{2}$ is a lower estimate
of $\pazocal{L}$ for type $M$ such that $\mathbb{B}\subseteq M$. Furthermore,
if $\mathbb{B}$ contains the transition $t$, then also
$\pazocal{T}_{\mathrm{exp}}[t]\in\Omega(n^{2})$ and $n^{2}$ is a lower
estimate of $\pazocal{T}[t]$ for type $M$ such that $\mathbb{B}\subseteq M$.

This follows follows directly from the results of [2] (Section 3.3).

######  Lemma B.5.

Given a one-dimensional VASS MDP, if there exists an bounded-zero BSCC
$\mathbb{B}$ of $\pazocal{A}_{\sigma}$ for some
$\sigma\in\Sigma_{\mathrm{MD}}$, then $\pazocal{L}$ is unbounded for type $M$
such that $\mathbb{B}\subseteq M$. Furthermore, if $\mathbb{B}$ contains $t$
then also $\pazocal{T}[t]$ is unbounded for type $M$ such that
$\mathbb{B}\subseteq M$.

######  Proof B.6.

Since $\mathbb{B}$ is bounded-zero, it must hold that there is no non-zero
cycle in $\mathbb{B}$. Therefore the effect of every path of $\mathbb{B}$ is
bounded by some constant. As such, the computation under $\sigma$ started from
any state of $\mathbb{B}$ can never terminate if the initial counter value is
sufficiently large.

######  Lemma B.7.

It is decidable in polynomial time if a one-dimensional VASS MDP
$\pazocal{A}$, that contains no increasing BSCC of $\pazocal{A}_{\sigma}$ for
any $\sigma\in\Sigma_{\mathrm{MD}}$, whether $\pazocal{A}$ contains a bounded-
zero BSCC $\mathbb{B}$ of $\pazocal{A}_{\sigma}$ for some
$\sigma\in\Sigma_{\mathrm{MD}}$.

######  Proof B.8.

Since there is no class increasing BSCC of an MD strategy, there can be no
solution $\mathbf{x}$ to (I) with $\sum_{(p,\mathbf{u},q)\in
T}\mathbf{x}((p,\mathbf{u},q))\mathbf{u}(c)>0$ as any such solution can be
used to extract a strategy with expected positive effect on the counter
(Appendix A: Lemma A.11). Therefore from Lemma 4.2, we have that there exists
a ranking function $rank$, defined by a maximal solution of (II) (see Section
4), such that the effect of any transition from a nondeterministic state has
non-positive effect on $rank$, and the expected effect of a single
computational step taken from a probabilistic state is non-positive on $rank$.
Furthermore, $rank$ depends on the counter value. Therefore any BSCC which
contains any transition whose effect on $rank$ can be non-zero cannot be
bounded-zero. If such transition were from non-deterministic state, then it
could only decrease the rank, and as $rank$ can never be increased in
expectation, this would lead to a positive chance of a cycle with negative
effect on $rank$ and thus also on the counter. And if the transition were from
a probabilistic state, then as the expectation is non-positive, there would be
a non-zero probability of a transition with negative effect on $rank$ being
chosen. Therefore any bounded-zero BSCC can contain only those transitions
that never change $rank$.

On the other hand, any BSCC $\mathbb{B}$ of $\pazocal{A}_{\sigma}$ for some
$\sigma\in\Sigma_{\mathrm{MD}}$, which contains only transitions that never
change $rank$ must be bounded-zero, as that means the effect of any cycle in
$\mathbb{B}$ must be $0$ (as any non-zero cycle would have necessarily changed
$rank$ in at least one of its transitions).

Therefore it is sufficient to decide whether there exists a BSCC $\mathbb{B}$
of $\pazocal{A}_{\sigma}$ for some $\sigma\in\Sigma_{\mathrm{MD}}$, containing
only those transitions that do not change $rank$. We can do this by analyzing
each MEC one by one. For each MEC we first compute $rank$ using the system
(II) (see Section 4), then proceed by first removing all transitions that can
change $rank$, and then iteratively removing non-deterministic states that do
not have any outgoing transition left, and probabilistic states for which we
removed any outgoing transition, until we reach a fixed point. If there exists
a bounded-zero BSCC $\mathbb{B}$ of $\pazocal{A}_{\sigma}$ for some
$\sigma\in\Sigma_{\mathrm{MD}}$, then all transitions of $\mathbb{B}$ will
remain in the fixed point as they can never be removed. On the other hand once
we reach the fixed point, it holds that for any state $p$ that is left there
either exists a “safe” outgoing transition if $p\in Q_{n}$ or all outgoing
transitions are “safe” if $p\in Q_{p}$, and these “safe” transitions end in a
“safe” state. With state being “safe” if it is left in fixed point, and
transitions being “safe” if their effect on $rank$ is $0$. Thus we can simply
select any MD strategy on the states/transitions that are left and it must
have a bounded-zero BSCC. And if the fixed point is empty, then there can be
no bounded-zero BSCC $\mathbb{B}$ of $\pazocal{A}_{\sigma}$ for some
$\sigma\in\Sigma_{\mathrm{MD}}$. Clearly this can be done in polynomial time.

######  Note B.9.

One might ask whether the restriction on one-dimensional VASS MDPs not
containing an increasing BSCC of $\pazocal{A}_{\sigma}$ for some
$\sigma\in\Sigma_{\mathrm{MD}}$, is necessary in Lemma B.7. The answer is yes,
as Lemma B.27 shows that deciding existence of a bounded-zero BSCC of
$\pazocal{A}_{\sigma}$ for some $\sigma\in\Sigma_{\mathrm{MD}}$, is
$\mathbf{NP}$-complete for general one-dimensional VASS MDPs.

######  Lemma B.10.

Given a one-dimensional VASS MDP $\pazocal{A}$, if there is no increasing or
bounded-zero BSCC of $A_{\sigma}$ for any $\sigma\in\Sigma_{\mathrm{MD}}$,
then $n^{2}$ is an upper estimate of $\pazocal{L}$ for every type.

######  Lemma B.11.

Given a one-dimensional VASS MDP $\pazocal{A}$, if there is no increasing BSCC
of $A_{\sigma}$ for any $\sigma\in\Sigma_{\mathrm{MD}}$, then $n$ is an upper
estimate of $\pazocal{C}[c]$ for every type.

To prove these two Lemmata, we need to consider a certain overapproximation of
$\pazocal{A}$, which in some sense is in multiple states at the same time.
This overapproximation will allow us to view any computation on $\pazocal{A}$
as if with very high probability, the computation was at each step _choosing_
one of finitely many (depending only on $\pazocal{A}$) random walks/cycles,
whose effects correspond to their corresponding BSCC (increasing, bounded-
zero, unbounded-zero, decreasing). That is if there is no increasing or
bounded-zero BSCC of $A_{\sigma}$ for any $\sigma\in\Sigma_{\mathrm{MD}}$,
then the expected effect of these random walks can only either be negative
(decreasing), or $0$ but with non-zero variance (unbounded-zero). This then
allows us to provide some _structure_ to the VASS MDP which will then allow us
to prove these lemmata. A key concept to defining this overapproximation is
that of an MD-decomposition, which roughly states that for each path on a VASS
MDP, we can _color_ each transition using one of finitely many colors, such
that the sub-path corresponding to each color is a path under some MD strategy
associated with that color. We then show that we can _color_ any path on
$\pazocal{A}$ using a finite set of colors, and that this _coloring_ can be
made “on-line”, that is a color can be assigned _uniquely_ (in some sense) to
each transition at the time this transition is taken in the computation.

######  Lemma (5.4).

For every VASS MDP $\pazocal{A}$, there exist
$\pi_{1},\dots,\pi_{k}\in\Sigma_{\mathrm{MD}}$, $p_{1},\dots,p_{k}\in Q$, and
a function $Decomp{A}$ such that the following conditions are satisfied for
every finite path $\alpha$:

  * •

$Decomp{A}(\alpha)$ returns an MD-decomposition of $\alpha$ under
$\pi_{1},\dots,\pi_{k}$ and $p_{1},\ldots,p_{k}$.

  * •

$Decomp{A}(\alpha)=Decomp{A}(\alpha_{..\mathit{len}(\alpha)-1})\;\circ\;\gamma^{1}\circ\cdots\circ\gamma^{k}$,
where exactly one of $\gamma^{i}$ has positive length (the $i$ is called the
_mode_ of $\alpha$).

  * •

If the last state of $\alpha_{..\mathit{len}(\alpha)-1}$ is probabilistic,
then the mode of $\alpha$ does not depend on the last transition of $\alpha$.

######  Proof B.12.

Proof by induction on the number of outgoing transitions from non-
deterministic states in $\pazocal{A}$.

Base case: Every non-deterministic state has exactly one outgoing transition.
Then there exists only a single strategy $\pi$ and it is MD. Therefore let
$k=|Q|$, $\pi_{1}=\dots=\pi_{k}=\pi$, and $p_{1},\dots,p_{k}$ be all the
distinct states of $\pazocal{A}$. Then let $Decomp{A}(\epsilon)=\epsilon$, and
for a path $\alpha$ with initial state $p_{i}$ let
$Decomp{A}(\alpha)=Decomp{A}(\alpha_{..\mathit{len}(\alpha)-1})\circ\gamma^{1}\circ\gamma^{2}\circ\dots\circ\gamma^{k}$
such that $\gamma^{j}=p_{j}$ for $j\neq i$ and $\gamma^{i}=q,\mathbf{u},r$
where $\alpha=p_{i},\dots,q,\mathbf{u},r$.

Induction step: Assume every VASS MDP $\pazocal{A}^{\prime}$ with less then
$i$ outgoing transitions from non-deterministic states satisfies the lemma,
and let $\pazocal{A}$ have exactly $i$ outgoing transitions from non-
deterministic states.

If $\pazocal{A}$ contains no non-deterministic state $p\in Q_{n}$ with
$|\mathit{Out}(p)|\geq 2$ then base case applies. Otherwise, let us fix some
state $p\in Q_{n}$ with $|\mathit{Out}(p)|\geq 2$, and let
$t_{r},t_{g}\in\mathit{Out}(p)$ be such that $t_{r}\neq t_{g}$. Let
$\pazocal{A}_{r}$ and $\pazocal{A}_{g}$ be VASS MDPs obtained from
$\pazocal{A}$ by removing $t_{g}$ and $t_{r}$, respectively.

For any path $\alpha$, we define a _red/green-decomposition_ of $\alpha$ on
$\pazocal{A}$ as $\alpha=g_{1}\circ r_{1}\circ g_{2}\circ r_{2}\circ\dots\circ
g_{\ell}\circ r_{\ell}$ (all of positive length except potentially $g_{1}$ and
$r_{\ell}$) satisfying the following:

  * •

for every $1\leq i<\ell$, the last state of $g_{i}$ is $p$;

  * •

if $\mathit{len}(r_{\ell})>0$ then the last state of $g_{\ell}$ is $p$;

  * •

for every $1\leq i<\ell$, the last state of $r_{i}$ is $p$;

  * •

for every $1<i\leq\ell$, the first state of $g_{i}$ is $p$ and the first
transition of $g_{i}$ is $t_{g}$;

  * •

for every $1\leq i\leq\ell$, the first state of $r_{i}$ is $p$ and the first
transition of $r_{i}$ is $t_{r}$;

  * •

$g_{\alpha}=g_{1}\circ\cdots\circ g_{\ell}$ is a path on $\pazocal{A}_{g}$.

  * •

$r_{\alpha}=r_{1}\circ\cdots\circ r_{\ell}$ is a path on $\pazocal{A}_{r}$.

Clearly every path on $\pazocal{A}$ has a unique red/green-decomposition that
can be computed online.

Now let $Decomp_{\pazocal{A}_{g}}$ and $Decomp_{\pazocal{A}_{r}}$,
$\pi_{1}^{g},\dots,\pi_{k_{g}}^{g}$ and $\pi_{1}^{r},\dots,\pi_{k_{r}}^{r}$,
$p_{1}^{g},\dots,p_{k_{g}}^{g}$ and $p_{1}^{r},\dots,p_{k_{r}}^{r}$, $k_{g}$
and $k_{r}$ be the $Decomp$ functions, MD strategies, states and $k$ values
for $\pazocal{A}_{g}$ and $\pazocal{A}_{r}$, respectively. Note that their
existence follows from the induction assumption. Then let $k=k_{g}+k_{r}$,
$\pi_{1}=\pi_{1}^{g},\pi_{2}=\pi_{2}^{g},\dots,\pi_{k_{g}}=\pi_{k_{g}}^{g},\pi_{k_{g}+1}=\pi_{1}^{r},\pi_{k_{g}+2}=\pi_{2}^{r},\dots,\pi_{k_{g}+k_{r}}=\pi_{k_{r}}^{r}$,
$p_{1}=p_{1}^{g},p_{2}=p_{2}^{g},\dots,p_{k_{g}}=p_{k_{g}}^{g},p_{k_{g}+1}=p_{1}^{r},p_{k_{g}+2}=p_{2}^{r},\dots,p_{k_{g}+k_{r}}=p_{k_{r}}^{r}$.
We now define $Decomp{A}(\epsilon)=\epsilon$ and
$Decomp{A}(\alpha)=Decomp{A}(\alpha_{..\mathit{len}(\alpha)-1})\circ\gamma^{1}\circ\gamma^{2}\circ\dots\circ\gamma^{k}$
such that if $t=(q,\mathbf{u},r)$ is the last transition of $\alpha$, and
$\alpha=g_{1}\circ r_{1}\circ g_{2}\circ r_{2}\dots g_{\ell}\circ r_{\ell}$ is
the red/green-decomposition of $\alpha$ on $\pazocal{A}$, it holds:

  * •

if $\mathit{len}(r_{\ell})=0$, then let $i$ be the
$Decomp_{\pazocal{A}_{g}}$-mode of $g_{\alpha}=g_{1}\circ\cdots\circ
g_{\ell}$. Then we put $\gamma^{j}=p_{j}$ for each $j\neq i$, and
$\gamma^{i}=q,\mathbf{u},r$;

  * •

if $\mathit{len}(r_{\ell})>0$, then let $i$ be the
$Decomp_{\pazocal{A}_{r}}$-mode of $r_{\alpha}=r_{1}\circ\cdots\circ
r_{\ell}$. Then we put $\gamma^{j}=p_{j}$ for each $j\neq k_{g}+i$, and
$\gamma^{k_{g}+i}=q,\mathbf{u},r$;

From Lemma 5.4 we can view any strategy $\sigma$ on $\pazocal{A}$ as if
$\sigma$ were choosing "which of the $k$ MD strategies to advance" at each
computational step. That is, let $\alpha$ be some path produced by a
computation under a strategy $\sigma$, then the "MD strategy to advance"
chosen by $\sigma$ after $\alpha$ is the MD strategy $\pi_{i}$ where $i$ is
such that

  * •

if the last state $p$ of $\alpha$ is probabilistic, then $i$ is the
$Decomp{A}$-mode of the path $\alpha,\mathbf{u},q$, for any
$(p,\mathbf{u},q)\in\mathit{Out}(p)$ (note that $i$ does not depend on which
transition of $\mathit{Out}(p)$ is chosen);

  * •

if the last state $p$ of $\alpha$ is non-deterministic, then let
$t=(p,\mathbf{u},q)\in\mathit{Out}(p)$ be the transition chosen by $\sigma$ in
$\alpha$. Then $i$ is the $Decomp{A}$-mode of the path $\alpha,\mathbf{u},q$.

Each of these MD strategies $\pi_{i}$ can be expressed using a Markov chain
$\mathscr{M}_{i}$ which is initialized in state $p_{i}$. Whenever an MD
strategy gets chosen, then the corresponding Markov chain makes one step.
Naturally, there are some restrictions on which of the indexes can be chosen
at a given time, namely a strategy can only choose an index $i$ such that
$\mathscr{M}_{i}$ is currently in the same state as the Markov chain which was
selected last. However, for our purposes we will consider _pointing
strategies_ that are allowed to choose any index, regardless of the current
situation. We shall call a VASS MDP where such _pointing strategies_ are
allowed, while also adding a special “die” transition that causes instant
termination an _extended VASS MDP_.

Formally speaking, let $\pi_{1},\dots,\pi_{k}$ and $p_{1},\dots,p_{k}$ be the
MD strategies and states from Lemma 5.4 associated with $Decomp{A}$. An
_extended VASS MDP_ associated to the 1-dimensional VASS MDP $\pazocal{A}$ is
the 2-dimensional VASS MDP
$\pazocal{A}^{\prime}=\left(Q^{\prime},(Q_{n}^{\prime},Q_{p}^{\prime}),T^{\prime},P^{\prime}\right)$
where $Q^{\prime}=Q^{k}\times\\{0,1,\dots,k\\}$,
$Q_{n}^{\prime}=Q^{k}\times\\{0\\}$, $Q_{p}=Q^{k}\times\\{1,\dots,k\\}$, and

  * •

$T^{\prime}=T_{n}^{\prime}\cup T_{p}^{\prime}\cup T_{die}^{\prime}$ where

    * –

$T_{n}^{\prime}=\\{((p_{1},\dots,p_{k},0)),(0,0),(p_{1},\dots,p_{k},i)\mid(p_{1},\dots,p_{k})\in
Q^{k},i\in\\{1,\dots,k\\}\\}$;

    * –

$T_{p}^{\prime}=\\{((p_{1},\dots,p_{k},i),(\mathbf{u}_{i},0),(p_{1},\dots,p_{i-1},q_{i},p_{i+1},\dots,p_{k},0))\mid(p_{1},\dots,p_{k})\in
Q^{k},i\in\\{1,\dots,k\\},\textit{ and either
}\pi_{i}(p_{i})=(p_{i},\mathbf{u}_{i},q_{i})\textit{ or both of }p_{i}\in
Q_{p}\textit{ and }(p_{i},\mathbf{u}_{i},q_{i})\in T\\}$;

    * –

$T_{die}^{\prime}=\\{(p,(0,-1),p)\mid p\in Q_{n}^{\prime}\\}$;

  * •

$P^{\prime}(((p_{1},\dots,p_{k},i),(\mathbf{u}_{i},0),(p_{1},\dots,p_{i-1},q_{i},p_{i+1},\dots,p_{k},0)))=\begin{cases}1&\mbox{if
}p_{i}\in Q_{n}\\\ P((p_{i},\mathbf{u}_{i},q_{i}))&\mbox{if }p_{i}\in
Q_{p}\end{cases}$

We call strategies on the extended VASS MDP _pointing strategies_. Note that
each strategy on a VASS MDP has an equivalent pointing strategy. Whenever a
pointing strategy $\sigma$ chooses a transition
$((p_{1},\dots,p_{k},0),(0,0),(p_{1},\dots,p_{k},i))$, then we say $\sigma$
pointed at the Markov chain $\mathscr{M}_{i}$. Note that in the following we
only consider computations on the extended VASS MDP initiated in the initial
state $(p_{1},\dots,p_{k},0)$, and with the second counter being set to $0$,
so to simplify the notation, we will write only instead of .

Given a sequence of strategies $\sigma_{1},\sigma_{2},\dots$ we will define a
sequence of pointing strategies
$\sigma_{1}^{\delta},\sigma_{2}^{\delta},\dots$ such that each
$\sigma_{n}^{\delta}$ in some sense “behaves as” $\sigma_{n}$, but at the same
time it “precomputes” the individual Markov chains. Since a formal description
of $\sigma_{n}^{\delta}$ would be overly complicated, we will give only a high
level description of $\sigma_{n}^{\delta}$. The sequence
$\sigma_{1}^{\delta},\sigma_{2}^{\delta},\dots$ is parameterized by
$0<\delta<1$. To help us define the behavior of $\sigma_{n}^{\delta}$, we
assume $\sigma_{n}^{\delta}$ “remembers” (it can always compute these from the
input) some paths $\gamma_{1},\dots,\gamma_{k},\alpha$. At the beginning these
are all initialized to $\gamma_{1}=\dots=\gamma_{k}=\alpha=\epsilon$.

A computation under $\sigma_{n}^{\delta}$ operates as follows: First
$\sigma_{n}^{\delta}$ internally selects $i\in\\{1,\dots,k\\}$ that
$\sigma_{n}$ would select after $\alpha$; that is $i$ is the $Decomp{A}$-mode
of $\alpha^{\prime}$, where $\alpha^{\prime}$ is such that if the last state
$p$ of $\alpha$ is probabilistic then $\alpha^{\prime}$ is $\alpha$ extended
by a single transition, and if $p$ is nondeterministic then
$\alpha^{\prime}=\alpha,\mathbf{u},q$ is $\alpha$ extended by the transition
$(p,\mathbf{u},q)$ where $(p,\mathbf{u},q)$ is the transition chosen by
$\sigma_{n}$ in $\alpha$ (i.e. $(p,\mathbf{u},q)$ is chosen at random using
the probabilistic distribution $\sigma_{n}(\alpha)$). Then
$\sigma_{n}^{\delta}$ asks if $\gamma_{i}\neq\epsilon$, if yes then it skips
to step 2), otherwise it first performs step 1) before moving to step 2):

  1. 1)

Let $(p_{1},\dots,p_{k},0)$ be the current state of $\pazocal{A}^{\prime}$.
Then in each non-deterministic state $\sigma_{n}^{\delta}$ keeps pointing at
$\mathscr{M}_{i}$ until either, if $p_{i}$ is not a state of a BSCC of
$M_{i}$, it reaches a state
$(p_{1},\dots,p_{i-1},q_{i},p_{i+1},\dots,p_{k},0)$ where $q_{i}$ is a state
of a BSCC of $M_{i}$ while, or if $p_{i}$ is a state of a BSCC of
$\mathscr{M}_{i}$ then $\sigma_{n}^{\delta}$ stops pointing at
$\mathscr{M}_{i}$ with probability $1/2$ each time the computation returns to
$(p_{1},\dots,p_{k},0)$.

In both cases, if this takes more then $2n^{\delta}$ steps then
$\sigma_{n}^{\delta}$ terminates using the “die” transitions (i.e.
$\sigma_{n}^{\delta}$ keeps reducing the second counter until termination
using the transitions from $T_{die}^{\prime}$). After this ends,
$\sigma_{n}^{\delta}$ sets $\gamma_{i}$ to the path generated by the
probabilistic transitions along this iterating (note that this can be seen as
a path on $\mathscr{M}_{i}$).

  2. 2)

Let $\gamma_{i}=p_{1},\mathbf{u}_{1},p_{2}\dots p_{\ell}$. Since $\ell>1$ we
have all the information needed to know which index $\sigma_{n}$ would have
chosen in it’s next step. Let $\alpha^{\prime}=\alpha,\mathbf{u}_{1},p_{2}$ be
$\alpha$ extended by the transition $(p_{1},\mathbf{u}_{1},p_{2})$. Then
$\sigma_{n}^{\delta}$ replaces $\alpha$ with $\alpha^{\prime}$, and
$\gamma_{i}$ with the path $p_{2}\dots p_{\ell}$ obtained by removing the
first transition from $\gamma_{i}$.

At this point this process repeats, until $\alpha$ is a terminating path for
initial counter value $n$ on $\pazocal{A}$, at which point
$\sigma^{\delta}_{n}$ terminates using the transitions from
$T_{die}^{\prime}$.

Let $l=k\cdot u$, where $u$ is the maximal possible change of the counter per
single transition. When started in the initial state $(p_{1},\dots,p_{k},0)$,
we can view $\sigma_{n}^{\delta}$ as if we were computing as per $\sigma_{n}$,
but occasionally we made some “extra” (precomputed) steps in some of the
Markov chains. These “extra” steps correspond exactly to the paths
$\gamma_{1},\dots,\gamma_{k}$, and since probability of these being longer
then $kn^{\delta}$ decreases exponentially with $n$, the probability. that
$\sigma_{n}^{\delta}$ started with initial counter values $(n+ln^{\delta},0)$
terminates before $\sigma_{n}$ would have for initial counter value $n$ in the
first $n^{2+\epsilon}$ steps, goes to $0$ as $n$ goes to $\infty$, for each
$\epsilon>0$. Therefore, if it were to hold that $\sigma_{n}$ can perform more
then $n^{2+\epsilon}$ steps with probability at least $a>0$ for some
$\epsilon>0$ and for infinitely many $n$, conditioned that
$\mathit{mecs}{=}\beta$ for some $\beta$ (note that $\beta$ does not depend on
$n$), then it holds $\limsup_{n\rightarrow\infty}$.

Similarly, the counter value of the first counter $c$ of
$\pazocal{A}^{\prime}$, when computing under $\sigma_{n}^{\delta}$ from
initial value $n+ln^{\delta}$ is at each point at most $n+ln^{\delta}$ plus
the effect of the paths $\gamma_{1},\dots,\gamma_{k}$, and $\alpha$. As the
length of all of $\gamma_{1},\dots,\gamma_{k}$ is at most $kn^{\delta}$, their
total effect on the counter at each point can be at most $ln^{\delta}$. And
$\alpha$ is the path generated by a computation of $\sigma_{n}$. Therefore, if
it were to hold that $\sigma_{n}$ can pump the counter to more then
$n^{1+\epsilon}$ with probability at least $a>0$ for some $\epsilon>0$ and for
infinitely many $n$, conditioned that $\mathit{mecs}{=}\beta$ for some $\beta$
(note that $\beta$ does not depend on $n$), then it holds
$\limsup_{n\rightarrow\infty}$.

Therefore the following two lemmatta imply Lemmata B.10 and B.11.

######  Lemma B.13.

If $\pazocal{A}$ is a one-dimensional VASS MDP such that there is no
increasing BSCC of $A_{\sigma}$ for any $\sigma\in\Sigma_{\mathrm{MD}}$, then

$\limsup_{n\rightarrow\infty}$

for each $0<\delta<\epsilon<1$.

######  Lemma B.14.

If $\pazocal{A}$ is a one-dimensional VASS MDP such that there is no
increasing or bounded-zero BSCC of $A_{\sigma}$ for any
$\sigma\in\Sigma_{\mathrm{MD}}$, then

$\limsup_{n\rightarrow\infty}$

for each $0<\delta<\epsilon<1$.

######  Proof B.15.

Let us begin with a proof for Lemma B.14. For simplification, let us assume
that if the first counter of $\pazocal{A}^{\prime}$ becomes negative while
iterating in some Markov chain $\mathscr{M}_{j}$ before it hits the target
state of $\mathscr{M}_{j}$, that is while performing step 1) as per the
description of $\sigma_{n}^{\delta}$, then the computation does not terminate
and instead it continues until this target state is reached at which point the
computation terminates if the counter is still negative. Clearly this can only
prolong the computation. Therefore, each Markov chain $\mathscr{M}_{j}$
contributes to computation of $\sigma_{n}^{\delta}$ by at most a single path
$\alpha_{j}$ (to reach a BSCC), and then of cycles over some state of a BSCC
of $\mathscr{M}_{j}$. Let $X_{i}^{j}$ denote the effect of the $i$-th cycle of
$\mathscr{M}_{j}$ performed under the computation of $\sigma_{n}^{\delta}$. As
each BSCC of $A_{\sigma}$ for any $\sigma\in\Sigma_{\mathrm{MD}}$ is either
unbounded-zero or decreasing, it holds that either
$\mathbb{E}^{\sigma_{n}^{\delta}}(X_{i}^{j})=0$ while
$Var^{\sigma_{n}^{\delta}}(X_{i}^{j})>0$ (unbounded-zero), or
$\mathbb{E}^{\sigma_{n}^{\delta}}(X_{i}^{j})<0$ (decreasing).

It also holds that
$\mathbb{E}^{\sigma_{n}^{\delta}}(\mathit{len}(\alpha_{j}))=b_{j}$ for some
constant $b_{j}$, and as the length of each $\alpha_{i}$ is bounded by
$n^{\delta}$, the maximal possible effect of all $\alpha_{1},\dots,\alpha_{k}$
on the counter is $ln^{\delta}$. The maximal length of each cycle is bounded
by $n^{\delta}$, therefore we can upper bound the expected length of all
cycles of $\mathscr{M}_{j}$ as $n^{\delta}$ times the expected number of such
cycles. Clearly the expected number of cycles corresponding to decreasing
BSCCs are at most linear as each such cycle moves expectation closer to $0$,
and there is no way to move the expectation away from $0$ by more then a
constant.

To bound the expected number of cycles corresponding to class unbounded-zero
BSCCs, we shall use the following lemma that is proven in appendix B.1.

######  Lemma B.16.

Let $\pazocal{A}$ be a one-dimensional VASS MDP, and let $X_{1},X_{2},\dots$
be random variables s.t. each $X_{i}$ corresponds to the effect of a path on
some unbounded-zero BSCC $\mathbb{B}$ of $\pazocal{A}_{\sigma}$ for some
$\sigma\in\Sigma_{\mathrm{MD}}$, that starts in some state $p$ of $\mathbb{B}$
and terminates with probability $1/2$ every time $p$ is reached again. Let