Deciding Fast Termination for Probabilistic VASS with Nondeterminism

TL;DR

This paper investigates the problem of determining whether probabilistic vector addition systems with states (pVASS) with nondeterminism have linear expected termination time, providing polynomial-time decidability results and a quadratic lower bound dichotomy.

Contribution

The paper introduces techniques for checking fast termination in pVASS with nondeterminism and establishes a polynomial-time decision procedure for linear expected termination time.

Findings

Decidability of linear expected termination time in certain pVASS classes.

A polynomial-time algorithm for checking fast termination.

A quadratic lower bound for non-linear expected termination times.

Abstract

A probabilistic vector addition system with states (pVASS) is a finite state Markov process augmented with non-negative integer counters that can be incremented or decremented during each state transition, blocking any behaviour that would cause a counter to decrease below zero. The pVASS can be used as abstractions of probabilistic programs with many decidable properties. The use of pVASS as abstractions requires the presence of nondeterminism in the model. In this paper, we develop techniques for checking fast termination of pVASS with nondeterminism. That is, for every initial configuration of size n, we consider the worst expected number of transitions needed to reach a configuration with some counter negative (the expected termination time). We show that the problem whether the asymptotic expected termination time is linear is decidable in polynomial time for a certain natural class of pVASS with nondeterminism. Furthermore, we show the following dichotomy: if the asymptotic expected termination time is not linear, then it is at least quadratic, i.e., in $\Omega(n^2)$.

Equations

$${\mathcal{L}}_a(n)$$

$${\mathcal{L}}_d(n)$$

$$\underset{n\to \infty }{\lim }\underset{p\in Q,\sigma \in \Sigma }{\sup }\left\{{\mathcal{P}}_{pn}^{\sigma }[Term\ge n^{2-\epsilon }]\right\}=1\text{vspace}-1mm$$

$$\sup \{{\mathbb{E}}_p^{\sigma }[\mathrm{MP}]\mid \sigma \in \Sigma ,p\in Q\}=\kappa <0\text{vspace}-2mm$$

$$i=\sum _{p\in \mathcal{B},p\stackrel{u}{\to }q}\eta (p)\cdot P(p\stackrel{u}{\to }q)\cdot u\text{vspace}-2mm$$

$$\underset{L(n)\cdot a_1}{\underbrace{j_1,\dots ,j_1}},s_1,\underset{L(n)\cdot a_2}{\underbrace{j_2,\dots ,j_2}},s_2,\cdots ,\underset{L(n)\cdot a_{\ell }}{\underbrace{j_{\ell },\dots ,j_{\ell }}},s_{\ell }\text{vspace}-2mm$$

$$\underset{L(n)}{\underbrace{(-\frac{1}{2},\frac{1}{2}),\dots ,(-\frac{1}{2},\frac{1}{2})}},s_1,\underset{L(n)}{\underbrace{(\frac{1}{2},-\frac{1}{2}),\dots ,(\frac{1}{2},-\frac{1}{2})}},s_2\text{vspace}-2mm$$

$$L(n)=\lfloor n/(\ell \cdot \xi -\sum _{j=1}^{\ell }{a}_j\cdot \underset{\mathcal{A}}{\min }+1)\rfloor .\text{vspace}-3mm$$

$${\pi }_1^1,{\tau }_1^1,\dots ,{\pi }_{\ell }^1,{\tau }_{\ell }^1,{\pi }_1^2,{\tau }_1^2,\dots ,{\pi }_{\ell }^2,{\tau }_{\ell }^2,\dots \dots {\pi }_1^{L(n)},{\tau }_1^{L(n)},\dots ,{\pi }_{\ell }^{L(n)},{\tau }_{\ell }^{L(n)},\hat{\pi }$$

$$\underset{n\to \infty }{\lim }\underset{p\in Q,\sigma \in \Sigma }{\inf }\left\{{\mathcal{P}}_{pn}^{\sigma }[Term\ge n^{2-\epsilon }]\right\}=1\text{vspace}-1mm$$

$$x\text{ subject to}$$

$$z_q$$

$$\sup \{{\mathbb{E}}_p^{\sigma }[\mathrm{MP}]\mid \sigma \in \Sigma ,p\in Q\}$$

$${\mathbb{E}}_p^{\sigma }[Dec]=\sum _{i=1}^{\infty }i\cdot {\mathcal{P}}_p^{\sigma }[Dec=i]\le c$$

$${\mathcal{P}}_p^{\sigma }[Dec=i]\le {\mathcal{P}}_p^{\sigma }[m^{(i)}-m^{(0)}\ge \mu -i\cdot \bar{x}]\le {\mathcal{P}}_p^{\sigma }[m^{(i)}-m^{(0)}\ge -(i\cdot \bar{x}/2)]$$

$${\mathcal{P}}_p^{\sigma }[m^{(i)}-m^{(0)}\ge -(i\cdot \bar{x}/2)]\le \exp \left(\frac{-i^2\cdot {\bar{x}}^2}{8\cdot i\cdot {\varrho }^2}\right)=a^i$$

$$m_{i,j}^{(k)}=\{\begin{array}{ll}{C}^{(k)}+y_j(p^{(k)})& \text{if }{C}^{(k)}\ge -cn\text{ for all }0\le k^{\prime }<k;\\ m_{i,j}^{(k-1)}& \text{otherwise}\end{array}$$

$$P(m_{i,j}^{(L^2(n))}\le -cn+\Vert y\Vert +1)\le P(m_{i,j}^{(L^2(n))}-m_{i,j}^{(0)}\le -(c-1)n)\le \exp \left(-(c-1{)}^2/\alpha \right)$$

$$\underset{n\to \infty }{\lim }{\mathcal{P}}_{pn}^{{\eta }_{n^{1/1+\gamma }}}[Term\ge n^{2-\epsilon }]=1.$$

$$\underset{r\to \infty }{\lim }{\mathcal{P}}_{p_1(r\cdot n)}^{{\eta }_n}[Term\ge L(n{)}^2]$$

$$=\underset{n\to \infty }{\lim }{\mathcal{P}}_{p_{1}n}^{{\eta }_{n^{1/(1+\gamma )}}}[Term\ge L(n^{1/(1+\gamma )}{)}^2].$$

$$L(n^{1/(1+\gamma )}{)}^2\ge n^{2/(1+\gamma )}/c=n^{2-2\gamma /(1+\gamma )}/c.$$

$$n^{2-2\gamma /(1+\gamma )}/c\ge n^{2-3\gamma /(1+\gamma )}.$$

$$x\text{ subject to}$$

$$z_q$$

$$\inf \{{\mathbb{E}}_p^{\sigma }[\mathrm{MP}]\mid \sigma \in \Sigma ,p\in Q\}.$$

$$m^{(i)}=\{\begin{array}{ll}{C}^{(i)}+{\bar{z}}_{S^{(i)}}-i\cdot \bar{x}& C^{(j)}>0\text{ for all j},0\le j<i,\\ m^{(i-1)}& \text{otherwise}\end{array}$$

$$P(m_j^{(t)}-m_j^{(0)}\le -n+Z_j)\le \exp (-(n-Z_j{)}^2/t\alpha )$$

$$P(m_j^{(t)}-m_j^{(0)}\le -n+Z)\le \exp (-(n-Z_j{)}^2/t\alpha )\le \exp (-n^2/4t\alpha ).$$

$$d\cdot \exp (-c/4\alpha )<1$$

$$\underset{n\to \infty }{\lim }P(m_j^{(t)}-m_j^{(0)}\le -n+Z_j)\le \underset{n\to \infty }{\lim }\exp (-(n-Z_j{)}^2/n^{2-\epsilon }\alpha )=0.$$

Full text

1 Introduction

Probabilistic Programs & VASS Probabilistic systems play an important role in various areas of computing such as machine learning [26], network protocol design [25], robotics [45], privacy and security [5], and many others. For this reason, verification of probabilistic systems receives a considerable attention of the verification community. As in the classical (non-probabilistic) setting, in probabilistic verification one typically constructs a suitable abstract model over-approximating the real behaviour of the system. In the past, the verification research was focused mostly on finite-state probabilistic models [4] as well as some special infinite-state classes, such as probabilistic one-counter [11] or pushdown automata [21, 24]. However, the recent proliferation of general, Turing-complete probabilistic programming languages (PPLs) necessitates the use of more complex models, that can encompass multiple potentially unbounded numerical variables.

In the classical setting, one of the standard formalisms used for program abstraction are vector addition systems with states (VASS) [32]. Intuitively, a VASS is a finite directed graph where every edge is assigned a vector of integer counter updates of a fixed dimension $d$. A configuration $p\mathbb{v}$ is specified by a current state $p$ and a vector of current counter values $\mathbb{v}$. The computation proceeds by moving along the edges in the graph and performing the respective updates on the counters. Since VASS themselves are not Turing-complete, they have many decidable properties, and they have been successfully used as program abstractions in termination and complexity analysis [44] as well as for reasoning about parallel programs [23, 32] and parameterized systems [6, 2]. Applying such an abstraction to a probabilistic program yields a probabilistic VASS (pVASS), which allows for a probabilistic choice of a transition in some states. Moreover, during the abstraction, certain complex programming constructs such as if-then-else branching are replaced with nondeterministic choice. To ensure that the abstraction over-approximates the possible behaviour, we typically interpret the nondeterminism as demonic, i.e., the choice is resolved by adversarial environment. However, in certain settings it makes sense to consider angelic nondeterminism, to be resolved by a yet-to-be-designed controller (e.g., a scheduling mechanism in a queuing system).

Termination Complexity One of the fundamental problems in program analysis is to evaluate a given program’s runtime. In the classical setting, this problem emerges in various flavours, ranging from worst-case execution time-analysis [47, 13] in real-time systems to obtaining bounds on the number of execution steps [27], analysing asymptotic [16], or amortized complexity [28]. VASS-based abstractions were successfully used in the latter scenario [44].

Recently, several approaches to reason about the expected runtime of probabilistic programs were developed [31, 40]. The analysis is much more demanding than in the classical case. For instance, deciding whether the expected runtime is finite is harder (i.e. higher in the arithmetic hierarchy) than deciding whether a probabilistic program terminates with probability one [30]. Additional obstacle is the inherent non-compositionality of expected runtimes. The work [31] gives an example of two programs, $P_{1}$, and $P_{2}$, which both consist of a single loop (i.e. they have a strongly connected control flow graph) and whose expected runtime is linear in the magnitude of initial variable valuations; but running $P_{2}$ after $P_{1}$ yields the program $P_{1};P_{2}$ whose expected runtime is infinite.

These intricacies spawn fundamental questions about probabilistic models, which we aim to address: Is there a sufficiently powerful probabilistic formalism where a fast (i.e., linear-time) termination from an arbitrary initial configuration is decidable? Can the decision procedure proceed by analysing individual strongly-connected components and composing the results? Can we provide a lower bound on the expected runtime in the case that it is not linear? These questions were previously considered in the non-probabilistic setting, namely in the domain of VASS [10]. In this paper, we investigate them in the probabilistic context.

Our Setting We show that the above questions can be answered affirmatively in the domain in pVASS with nondeterminism, which are Markov decision processes over VASS where the nondeterministic choice is resolved either demonically (i.e. the nondeterminism tries to prolong the computation) or angelically. We consider a basic variant of VASS termination: the zero termination, where the computation stops when some counter becomes negative. The termination complexity of a given pVASS is a function $\mathcal{L}\colon\mathbb{N}\rightarrow\mathbb{N}\cup\{\infty\}$ assigning to every $n$ the maximal/minimal (in the demonic/angelic case) expected length of a computation initiated in a configuration of size $n$ (the size of $p\mathbb{v}$ is defined as the maximal component of $\mathbb{v}$), where the maximum/minimum is taken over all the strategies of the environment (we consider unrestricted, i.e., history-dependent and randomized, strategies).

Our Results For strongly connected pVASS which contain either a demonic or an angelic non-determinism (but not both) we show that

The problem whether $\mathcal{L}\in\mathcal{O}(n)$ is decidable in polynomial time. 2. 2.

If $\mathcal{L}\not\in\mathcal{O}(n)$, then $\mathcal{L}\in\Omega(n^{2})$. 3. 3.

If $\mathcal{L}\not\in\mathcal{O}(n)$, then for every $\varepsilon>0$, the probability of all computations of length at least $n^{2-\varepsilon}$ converges to one as $n\rightarrow\infty$, (in the demonic case, this requires the environment to use appropriate strategies).

According to 2., $\mathcal{L}\not\in\mathcal{O}(n)$ implies that $\mathcal{L}$ is “at least quadratic”. However, 3.  does not follow from 2. (a more detailed discussion is postponed to Section 3).

We also show that the above results hold in general VASS with angelic nondeterminism, while in the demonic setting they extend to a restricted class pVASS whose maximal end-component (MEC) decomposition yields a directed acyclic graph (DAG), in which case 1. can be solved compositionally by analysing individual MECs. Finally, we show that in pVASS whose MEC-decomposition is not DAG-like, the demonic complexity cannot be decided by analysis of individual MECs, since such VASS can emulate the non-compositional example of [31].

The results build on analogous results for non-probabilistic VASS established in [10], combining them with a novel probabilistic analysis.

Paper Organization. After presenting preliminaries in Section 2, we focus on the demonic case which contains the main technical contributions. Subsection 3.1 provides an intuitive outline of our techniques. Subsection 3.2 develops the algorithm for proving linear termination complexity and shows its soundness (i.e. that a yes-answer indeed proves $\mathcal{L}_{d}(n)\in\mathcal{O}(n)$). Subsection 3.3 deals with the quadratic lower bound, showing the completeness of our algorithm, and Subsection 3.4 discusses extension of the results to the angelic case. Finally, in Section 4 we extend the techniques to DAG-like VASS MDPs and discuss the difficulties arising in general VASS. Missing proofs are provided in the appendix.

Related Work. The termination problems (counter-termination, control-state termination) for classical VASS as well as the related problems of boundedness and coverability have been studied very intensively in the last decades, see, e.g., [38, 42, 20, 22, 7]. The complexity of the termination problem with fixed initial configuration is EXPSPACE complete [38, 48, 3]. The more general reachability problem is also decidable [39, 35, 33], but computationally hard [38, 19]. The best known upper bound is Ackermannian [37] (see [43] for an overview of hyper-Ackermannian complexity hierarchies).

The problem of existence of infinite computations in VASS has been also studied in the literature. Polynomial-time algorithms have been presented in [14, 46] using results of [34]. In the more general context of games played on VASS, even deciding the existence of infinite computation is coNP-complete [14, 46], and various algorithmic approaches based on hyperplane-separation technique have been studied in [15, 29, 18].

The study on asymptotic termination complexity of non-probabilistic VASS, initiated in [10] was continued in [36], where the existence of some $k$ such that $\mathcal{L}\in\mathcal{O}(n^{k})$ was also shown decidable in polynomial time.

Concerning expected runtime analysis, we note the work [17] which presents a sound (but incomplete) technique for obtaining near-linear asymptotic bounds on recurrence relations arising from certain types of probabilistic programs.

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 $\mathcal{O}(f(n))$ and $\Omega(f(n))$ 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(n)\in\mathcal{O}(f(n))$ and $h(n)\in\Omega(f(n))$, we write $h(n)\in\Theta(f(n))$.

Let $A$ be a finite index set. The vectors of $\mathbb{R}^{A}$ are denoted by bold letters such as $\mathbb{u},\mathbb{v},\mathbb{z},\ldots$. The component of $\mathbb{v}$ of index $i\in A$ is denoted by $\mathbb{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 $\mathbb{n}$ to denote the constant vector where all components are equal to $n$. The scalar product of $\mathbb{v},\mathbb{u}\in\mathbb{R}^{d}$ is denoted by $\mathbb{v}\cdot\mathbb{u}$, i.e., $\mathbb{v}\cdot\mathbb{u}=\sum_{i=1}^{d}\mathbb{v}(i)\cdot\mathbb{u}(i)$. 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, $\mathbb{v}<\mathbb{u}$ if $\mathbb{v}(i)<\mathbb{u}(i)$ for every index $i$.

2.1 Markov Decision Processes

Definition 1

Let $L$ be a set of labels. A Markov decision process (MDP) with $L$-labeled transitions is a tuple $\mathcal{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 L\times Q$ is a finite set of labeled transitions such that every $q\in Q$ has at least one outgoing transition, and $P$ is a function assigning to each $(p,\ell,q)\in T$ where $p\in Q_{p}$ a positive rational probability so that, for every $p\in Q_{p}$, $\sum_{(p,\ell,q)\in T}P(p,\ell,q)=1$.

A state $q$ is an immediate successor of a state $p$ if there is a transition $(p,\ell,q)$ for some $\ell\in L$. A finite path in $\mathcal{A}$ of length $n$ is a finite sequence of the form $p_{0},\ell_{1},p_{1},\ell_{2},p_{2},\ldots,\ell_{n},p_{n}$ where $n\geq 0$ and $(p_{i},\ell_{i+1},p_{i+1})\in T$ for all $0\leq i<n$. If $n\geq 1$ and $p_{0}=p_{n}$, then $\pi$ is a cycle. An MDP is strongly connected if for each pair of distinct states $p,q$ there is a finite path from $p$ to $q$. An infinite path in $\mathcal{A}$ is an infinite sequence $p_{0},\ell_{1},p_{1},\ell_{2},p_{2},\ldots$ such that $p_{0},\ell_{1},p_{1},\ldots,\ell_{n},p_{n}$ is a finite path for every $n\geq 0$. For a finite sequence of the form $\pi=p_{0},\ell_{1},p_{1},\ell_{2},p_{2},\ldots,\ell_{n},p_{n}$ and a finite or infinite sequence of the form $\varrho=q_{0},\kappa_{1},q_{1},\kappa_{2},\ldots$, where $\pi$ and $\varrho$ are not necessarily paths in $\mathcal{A}$, we use $\pi\odot\varrho$ to denote the concatenated sequence $p_{0},\ell_{1},\ldots,\ell_{n},p_{n},\kappa_{1},q_{1},\kappa_{2},\ldots$ (we do not require $p_{n}=q_{0}$). If $\pi,\varrho$ are both paths in $\mathcal{A}$ and $p_{n}=q_{0}$, then $\pi\odot\varrho$ is also a path in $\mathcal{A}$.

A strategy is a function $\sigma$ assigning to every finite path $p_{0},\ell_{1},p_{1},\ldots,\ell_{n},p_{n}$ ending in a nondeterministic state a probability distribution over the outgoing transitions of $p_{n}$. A strategy is Markovian (M) if it depends only on the last state $p_{n}$, and deterministic (D) if it always selects some successor state with probability one. The set of all strategies is denoted by $\Sigma$ (the underlying $\mathcal{A}$ is always clearly determined by the context). Every initial state $p\in Q$ and every strategy $\sigma$ determine the probability space over infinite paths initiated in $p$ in the standard way, and we use $\mathcal{P}^{\sigma}_{p}$ to denote the associated probability measure.

2.2 Probabilistic VASS with Nondeterminism

Definition 2

Let $d\in\mathbb{N}$. A $d$-dimensional probabilistic VASS with non-determinism (VASS MDP) is an MDP where the set of labels is $\mathbb{Z}^{d}$.

Let $\mathcal{A}=\left(Q,(Q_{n},Q_{p}),T,P\right)$ be a $d$-dimensional VASS MDP. The encoding size of $\mathcal{A}$ is denoted by $|\!|\mathcal{A}|\!|$, where the integers representing counter updates are written in binary. A configuration of $\mathcal{A}$ is a pair $p\mathbb{v}$, where $p\in Q$ and $\mathbb{v}\in\mathbb{Z}^{d}$. If some component of $\mathbb{v}$ is negative, then $p\mathbb{v}$ is terminal. The set of all configurations of $\mathcal{A}$ is denoted by $\mathit{C}(\mathcal{A})$. The size of $p\mathbb{v}\in\mathit{C}(\mathcal{A})$ is $|\!|p\mathbb{v}|\!|=|\!|\mathbb{v}|\!|=\max\{|\mathbb{v}(i)|:1\leq i\leq d\}$. Given $n\in\mathbb{N}$, we say that $p\mathbb{v}$ is $n$-bounded if $|\!|p\mathbb{v}|\!|\leq n$.

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

Recall that every strategy $\sigma$ and every $p\in Q$ determine a probability space over infinite paths initiated in $p$ with probability measure $\mathcal{P}_{p}^{\sigma}$. Similarly, $\sigma$ determines the unique probability space over all computations initiated in a given $p\mathbb{v}$, and we use $\mathcal{P}^{\sigma}_{p\mathbb{v}}$ to denote the associated probability measure, and $\mathbb{E}^{\sigma}_{p\mathbb{v}}[\mathit{Term}]$ denotes the expected value of $\mathit{Term}$.

The angelic/demonic termination complexity of $\mathcal{A}$ are the functions $\mathcal{L}_{a},\mathcal{L}_{d}\colon\mathbb{N}\rightarrow\mathbb{R}\cup\{\infty\}$ defined as follows, where $\mathit{C}_{n}(\mathcal{A})$ is the set of all $p\mathbb{v}\in\mathit{C}(\mathcal{A})$ such that $|\!|p\mathbb{v}|\!|=n$:

[TABLE]

We say that the expected angelic/demonic termination time of $\mathcal{A}$ is linear if $\mathcal{L}_{a}(n)\in\mathcal{O}(n)$ and $\mathcal{L}_{d}(n)\in\mathcal{O}(n)$, respectively.

3 Linearity of Demonic Termination Time

In this paper, we prove the following theorem:

Theorem 3.1

The problem whether the expected termination time of a given strongly connected VASS MDP $\mathcal{A}$ is linear is decidable in polynomial time. If the expected termination time of $\mathcal{A}$ is not linear, then $\mathcal{L}_{d}(n)\in\Omega(n^{2})$. Furthermore, for every $\varepsilon>0$ we have that

[TABLE]

The last part of Theorem 3.1 deserves some comments. Recall $\mathcal{L}_{d}(n)\in\Omega(n^{2})$ if there is $b>0$ such that $\mathcal{L}_{d}(n)\geq b\cdot n^{2}$ for all sufficiently large $n$. We prove $\mathcal{L}_{d}(n)\in\Omega(n^{2})$ by showing the existence of $\delta,c>0$ such that $\mathcal{P}_{p\mathbb{n}}^{\sigma}[\mathit{Term}\geq n^{2}/c]\geq\delta$ for all sufficiently large $n$, where $\sigma$ is a suitable strategy depending on $p\mathbb{n}$ (then, we can put $b=\delta/c$). Hence, $\mathcal{L}_{d}(n)\in\Omega(n^{2})$ does not imply that $\sup_{\sigma\in\Sigma,p\in Q}\ \left\{\mathcal{P}_{p\mathbb{n}}^{\sigma}[\mathit{Term}\geq n^{2}/c]\ \right\}$ converges to $1$ as $n\rightarrow\infty$ (for some constant $c$). The last part of Theorem 3.1 shows that for an arbitrarily small $\varepsilon>0$, we have that $\sup_{\sigma\in\Sigma,p\in Q}\ \left\{\mathcal{P}_{p\mathbb{n}}^{\sigma}[\mathit{Term}\geq n^{2-\varepsilon}]\ \right\}$ does converge to $1$ as $n\rightarrow\infty$. The question whether the convergence holds for $\varepsilon=0$ remains open.

3.1 Outline of Techniques

The proof of Theorem 3.1 is non-trivial, and it is based on combining the existing techniques with new analysis invented in this paper. We use VASS MDPs $\mathcal{A}_{1}$ and $\mathcal{A}_{2}$ of Fig. 1 as running examples to illustrate our techniques.

A polynomial-time algorithm deciding asymptotic linearity of termination time for purely non-deterministic VASS (where the set $Q_{p}$ is empty) was given in [10]. Theorem 3.1 generalizes this result to VASS MDPs. We start by recalling the results of [10] and sketching the main ideas behind the proof of Theorem 3.1. These ideas are then elaborated in subsequent sections.

Consider a purely non-deterministic VASS $\mathcal{A}$ of dimension $d$. A cycle $p_{0},\mathbb{u}_{1},p_{1},\ldots,\mathbb{u}_{n},p_{n}$ of $\mathcal{A}$ is simple if all $p_{1},\ldots,p_{n-1}$ are pairwise different. The total effect of a simple cycle, i.e., the sum $\sum_{i=1}^{n}\mathbb{u}_{i}$, is called an increment. Clearly, there are only finitely many increments $\mathbb{i}_{1},\ldots,\mathbb{i}_{k}$. In [10], it was shown that the termination time of $\mathcal{A}$ is linear iff all increments are contained in an open half-space whose normal $\mathbb{w}$ is strictly positive in every component. The “if” direction is immediate, relying on a straightforward “ranking” argument. The “only if” part is more elaborate. In [10], it was shown that if the increments are not contained in an open half-space with positive normal, then for all sufficiently large $n$, there is a non-terminating computation initiated in $p\mathbb{n}$ whose length is at least $n^{2}/c$ for some constant $c$. This computation consists of simple cycles and auxiliary short paths used to “switch” from one control state to another.

Now let $\mathcal{A}$ be a VASS MDP with $d$ counters. Here, instead of simple cycles and their increments, we use the vectors of expected counter changes per transition induced by MD strategies in their BSCCs. More precisely, for each of the finitely many MD strategies $\sigma$ and every BSCC $\mathcal{B}$ of the finite-state Markov chain $\mathcal{A}_{\sigma}$ obtained by “applying” $\sigma$ to $\mathcal{A}$, we consider the unique vector $\mathbb{i}$ of expected counter changes per transition (note that $\mathbb{i}$ is the same for almost all infinite computations initiated in a state of $\mathcal{B}$). Thus, we obtain a finite set of vectors $\mathbb{i}_{1},\ldots,\mathbb{i}_{k}$ together with the associated set of tuples $(\sigma_{1},\mathcal{B}_{1}),\dots,(\sigma_{k},\mathcal{B}_{k})$ where each $\sigma_{i}$ is an MD strategy and $\mathcal{B}_{i}$ is a BSCC of $\sigma_{i}$ (note that we can have $\sigma_{i}=\sigma_{j}$ for $i\neq j$ since MD strategies might have multiple BSCCs). Similarly as in [10], we check whether all $\mathbb{i}_{1},\ldots,\mathbb{i}_{k}$ are contained in an open half-space whose normal $\mathbb{w}$ is strictly positive in every component. This is achievable in polynomial time by using the results of [8]. If such a $\mathbb{w}$ exists, we can conclude $\mathcal{L}_{d}(n)\in\mathcal{O}(n)$. This is because the “extremal” vectors of expected counter changes per transition are obtained by MD strategies111Here we rely on well-known results about finite-state MDPs [41]., and hence the expected shift in the direction opposite to $\mathbb{w}$ per transition stays bounded away from zero even for general strategies. We than use a submartingale-based argument to show that the expected termination time is linear. This proves the first part of Theorem 3.1.

Example 1

For the VASS MDP $\mathcal{A}_{2}$ of Fig. 1, there are three different increments $\mathbb{i}_{1}=(-1,\frac{1}{2})$, $\mathbb{i}_{2}=(\frac{1}{2},-1)$, and $\mathbb{i}_{3}=(-1,-1)$. Hence, we can choose $\mathbb{w}=(1,1)$ as a positive normal satisfying $\mathbb{i}_{1}\cdot\mathbb{w}<0$, $\mathbb{i}_{2}\cdot\mathbb{w}<0$, and $\mathbb{i}_{3}\cdot\mathbb{w}<0$. For the VASS MDP $\mathcal{A}_{1}$ of Fig. 1, there are three different increments $\mathbb{i}_{1}=(-\frac{1}{2},\frac{1}{2})$, $\mathbb{i}_{2}=(\frac{1}{2},-\frac{1}{2})$, and $\mathbb{i}_{3}=(-1,-1)$, hence no positive normal $\mathbb{w}$ satisfying $\mathbb{i}_{1}\cdot\mathbb{w}<0$ and $\mathbb{i}_{2}\cdot\mathbb{w}<0$ exists.

Now suppose there is no such $\mathbb{w}$. Recall that for purely non-deterministic VASS, a sufficiently long non-terminating computation initiated in $p\mathbb{n}$ consisting of simple cycles and short “switching” paths was constructed in [10]. Since $\mathbb{i}_{1},\ldots,\mathbb{i}_{k}$ are no longer effects of simple cycles or any fixed finite executions, it is not immediately clear how to proceed and we need to use new techniques. The arguments of [10] used to construct a sufficiently long non-terminating computation are purely geometric, and they do not depend on the fact that increments are total effects of simple cycles. Hence, by using the same construction, we obtain a sufficiently long sequence of vectors consisting of $\mathbb{i}_{1},\ldots,\mathbb{i}_{k}$ and some auxiliary elements representing switches between control states. We call this sequence a scheme, because it does not correspond to any real computation of $\mathcal{A}$ in general. When the constructed scheme is initiated in $p\mathbb{n}$, the resulting trajectory never crosses any axis. Also note that for every fixed $r\in\mathbb{N}$, we can create an extra $(r-1)\cdot n$ space between the trajectory and the axes by shifting the initial point from $p\mathbb{n}$ to $p(r\cdot\mathbb{n})$, which does not influence our asymptotic bounds. Now, we analyze what happens if the constructed scheme is followed from $p(r\cdot\mathbb{n})$. Here, following a vector $\mathbb{i}_{j}$ means to execute the transition selected by $\sigma_{j}$, and following a “switch” from $p$ to $q$ means to execute a strategy which eventually reaches $q$ with probability one (we use a strategy minimizing the expected number steps needed to reach $q$). Using concentration bounds of martingale theory, we show that the probability of all executions deviating from the scheme by more than $r\cdot n$ is bounded by $1-\delta$ for some fixed $\delta>0$ (assuming $n$ is sufficiently large), which yields the $\mathcal{L}_{d}(n)\in\Omega(n^{2})$ lower bound of Theorem 3.1. The last part of Theorem 3.1 is proven by a more detailed analysis of the established bounds.

Let us note that the underlying martingale analysis is not immediate, since the previous work which provides the basis for this analysis (such as [11]) typically assume that the analysed strategies are memoryless in the underlying finite state space. In contrast, strategies arising of schemes are composed of multiple memoryless strategies, with the switching rules depending on the size of the initial configuration. Hence, we take a compositional approach, analysing each constituent strategy separately using known techniques and composing the results via a new approach.

3.2 The Algorithm

In this section we prove the first part of Theorem 3.1. Our analysis uses results on multi-mean-payoff MDPs. Recall that if $\mathcal{M}$ is an MDP with transitions labelled by elements of $\mathbb{R}^{d}$ (for some dimension $d$), then a mean-payoff of an infinite path $\pi=p_{0},\mathbb{u}_{1},p_{1},\mathbb{u}_{2},\ldots$ of $\mathcal{A}$ is $\mathrm{MP}(\pi)=\liminf_{n\rightarrow\infty}\frac{1}{n}\sum_{i=1}^{n}\mathbb{u}_{i}$. We say that a given vector $\mathbb{v}$ is achievable for $\mathcal{A}$ if there exist a strategy $\sigma$ and $p\in Q$ such that $\mathbb{E}_{p}^{\sigma}[\mathrm{MP}]\geq\mathbb{v}$. Now we recall some results on mean-payoff MDPs [8] used as tools in this section.

(a)

There is a finite set $\mathcal{R}$ of vectors such that the set of all achievable vectors is precisely the set of all $\mathbb{v}$ such that $\mathbb{v}\leq\mathbb{u}$ for some $\mathbb{u}\in\mathcal{R}^{*}$, where $\mathcal{R}^{*}$ is the convex hull of $\mathcal{R}$.

(b)

The problem whether a given rational $\mathbb{v}$ is achievable is decidable in polynomial time.

Furthermore, we need the following result about finite-state MDPs.

Lemma 1

Let $\mathcal{M}=\left(Q,(Q_{n},Q_{p}),T,P\right)$ be a strongly connected MDP with labels from $\mathbb{Q}$ such that

[TABLE]

Let $\mathit{Dec}$ be a function assigning to every infinite path $\pi=p_{0},u_{1},p_{1},u_{2},\ldots$ of $\mathcal{M}$ the least $m$ such that $\sum_{i=1}^{m}u_{i}\leq-1$. If there is no such $m$, then $\mathit{Dec}(\pi)=\infty$. Then there exists a constant $c$ depending only on $\mathcal{M}$ such that for every $p\in Q$ and $\sigma\in\Sigma$ we have that $\mathbb{E}_{p}^{\sigma}[\mathit{Dec}]\leq c$.

Now we show how to prove the first part of Theorem 3.1 using the results above. Let $\mathcal{A}=\left(Q,(Q_{n},Q_{p}),T,P\right)$ be a strongly connected VASS MDP. For each of the finitely many MD strategies $\sigma$ we can consider a finite-state Markov chain $\mathcal{A}_{\sigma}$ obtained from $\mathcal{A}$ by fixing in every $q\in Q_{n}$ the probability of transitioning to the unique successor specified by $\sigma(q)$ to 1. For each such $\mathcal{A}_{\sigma}$ and each its BSCC $\mathcal{B}$ we consider the unique vector $\mathbb{i}$ defined by

[TABLE]

where $\eta$ is the invariant (stationary) distribution over the states of $\mathcal{B}$ (note that $\mathbb{i}=\mathbb{E}_{p}^{\sigma}[\mathrm{MP}]$ for every $p\in\mathcal{B}$). Thus, we obtain a finite set of increments $\mathbb{i}_{1},\ldots,\mathbb{i}_{k}$ together with the associated MD strategies $\sigma_{1},\ldots,\sigma_{k}$ and the BSCCs $\mathcal{B}_{1},\ldots,\mathcal{B}_{k}$.

Lemma 2

If there exists a vector $\mathbb{w}>\mathbb{0}$ such that $\mathbb{i}_{j}\cdot\mathbb{w}<0$ for every $1\leq j\leq k$, then there exists $\kappa<0$ such that $\mathbb{w}\cdot\mathbb{E}_{p}^{\sigma}[\mathrm{MP}]\leq\kappa$ for every $p\in Q$ and $\sigma\in\Sigma$.

Proof

Let $\kappa=\max\{\mathbb{i}_{j}\cdot\mathbb{w}\mid 1\leq j\leq k\}$. Consider a $\mathbb{Q}$-labelled MDP $\mathcal{M}$ obtained from $\mathcal{A}$ by replacing each counter update vector $\mathbb{u}$ with the number $\mathbb{u}\cdot\mathbb{w}$. Note that every strategy $\sigma$ for $\mathcal{A}$ can be seen as a strategy for $\mathcal{M}$, and vice versa. For a given $\sigma\in\Sigma$, we write $\mathbb{E}_{p}^{\sigma,\mathcal{A}}[\mathrm{MP}]$ and $\mathbb{E}_{p}^{\sigma,\mathcal{M}}[\mathrm{MP}]$ to denote the expected value of $\mathrm{MP}$ in $\mathcal{A}$ and $\mathcal{M}$, respectively. Note that for every $\sigma\in\Sigma$ we have that $\mathbb{E}_{p}^{\sigma,\mathcal{M}}[\mathrm{MP}]=\mathbb{w}\cdot\mathbb{E}_{p}^{\sigma,\mathcal{A}}[\mathrm{MP}]$.

For every $p\in Q$, there is an optimal MD strategy $\hat{\sigma}$ maximizing the expected mean payoff in $\mathcal{M}$. Since $\mathbb{E}_{p}^{\hat{\sigma},\mathcal{M}}[\mathrm{MP}]$ is a convex combination of increments, we obtain $\mathbb{E}_{p}^{\hat{\sigma},\mathcal{M}}[\mathrm{MP}]\leq\kappa$. Now let $\sigma$ be an arbitrary strategy. Since $\mathbb{E}_{p}^{\sigma,\mathcal{M}}[\mathrm{MP}]\leq\mathbb{E}_{p}^{\hat{\sigma}}[\mathrm{MP}]\leq\kappa$, we obtain $\mathbb{E}_{p}^{\sigma,\mathcal{M}}[\mathrm{MP}]=\mathbb{w}\cdot\mathbb{E}_{p}^{\sigma,\mathcal{A}}[\mathrm{MP}]\leq\kappa$. ∎

A direct corollary to Lemma 1 and Lemma 2 is the following:

Lemma 3

If there exists a vector $\mathbb{w}>\mathbb{0}$ such that $\mathbb{i}_{j}\cdot\mathbb{w}<0$ for every $1\leq j\leq k$, then $\mathcal{L}_{d}(n)\in\mathcal{O}(n)$ holds for $\mathcal{A}$.

The next lemma leads to a sound algorithm for proving of linear termination complexity.

Lemma 4

The vector $\mathbb{0}$ is achievable for $\mathcal{A}$ iff there is no $\mathbb{w}>\mathbb{0}$ such that $\mathbb{i}_{j}\cdot\mathbb{w}<0$ for every $1\leq j\leq k$.

Proof

If $\mathbb{0}$ is achievable, there exist $\sigma\in\Sigma$ and $p\in Q$ such that $\mathbb{E}_{p}^{\sigma}[\mathrm{MP}]\geq\mathbb{0}$. Suppose there is $\mathbb{w}>\mathbb{0}$ such that $\mathbb{i}_{j}\cdot\mathbb{w}<0$ for every $1\leq j\leq k$. By Lemma 2, $\mathbb{E}_{p}^{\sigma}[\mathrm{MP}]\cdot\mathbb{w}<0$, which is a contradiction.

Now suppose $\mathbb{0}$ is not achievable. Consider the (convex and compact) set $\mathcal{R}^{*}$ of claim (a). Since $\mathbb{0}$ is not achievable, the set $\mathcal{R}^{*}$ has the empty intersection with the (convex) set of all vectors with non-negative components. By the hyperplane separation theorem, there exists a hyperplane with normal $\mathbb{w}>\mathbb{0}$ such that $\mathbb{v}\cdot\mathbb{w}<0$ for all $\mathbb{v}\in\mathcal{R}^{*}$. Since every increment $\mathbb{i}$ is achievable, there is $\mathbb{v}\in\mathcal{R}^{*}$ such that $\mathbb{i}\leq\mathbb{v}$. Hence, $\mathbb{i}\cdot\mathbb{w}<0$. ∎

Hence, to check linear termination complexity, our algorithm simply checks whether $\mathbb{0}$ is achievable for $\mathcal{A}$. The previous lemma shows that this approach is sound. In the next subsection, we show that if there is no $\mathbb{w}>\mathbb{0}$ such that $\mathbb{i}_{j}\cdot\mathbb{w}<0$ for every $1\leq j\leq k$, then the expected termination time of $\mathcal{A}$ is at least quadratic. This shows that our algorithm is also complete, i.e. a decision procedure for linear termination of strongly connected demonic VASS MDPs.

3.3 Quadratic Lower Bound

For the rest of this section, we fix a strongly connected VASS MDP $\mathcal{A}=\left(Q,(Q_{n},Q_{p}),T,P\right)$. Let $\mathbb{i}_{1},\ldots,\mathbb{i}_{k}$ be the increments, and $\sigma_{1},\ldots,\sigma_{k}$ and $\mathcal{B}_{1},\ldots,\mathcal{B}_{k}$ the associated MD strategies and BSCCs introduced in Section 3.2.

Suppose that there does not exist a normal vector $\mathbb{w}>\mathbb{0}$ such that $\mathbb{i}_{i}\cdot\mathbb{w}<0$ for every $1\leq i\leq k$. By [10, Lemma 3.2]222Technically, Lemma 3.2 in [10] assumes $\mathbb{i}_{j}\in\mathbb{Z}^{d}$ for every $1\leq j\leq k$. Here, $\mathbb{i}_{j}\in\mathbb{Q}^{d}$. We can multiply all increments of by the least common multiple of all denominators and apply Lemma 3.2 afterwards., there exist a subset of increments $\mathbb{j}_{1},\ldots,\mathbb{j}_{\ell}$ and positive integer coefficients $a_{1},\ldots,a_{\ell}$ such that $\sum_{i=1}^{\ell}a_{i}\mathbb{j}_{i}\geq\mathbb{0}$. We use this subset to construct a so-called scheme.

Scheme The definition of a scheme is parameterized by a certain function $L:\mathbb{N}\rightarrow\mathbb{N}$. This function is defined later, for now it suffices to know that $L(n)\in\Theta(n)$. For every $n\in\mathbb{N}$, we define the scheme for $n$, which is a concatenation of $L(n)$ identical $n$-cycles, where each $n$-cycle is defined as follows:

[TABLE]

The subsequence $\mathbb{j}_{i},\ldots,\mathbb{j}_{i},s_{i}$ of the $j$-th cycle is called the $i$-th segment of the $j$-th $n$-cycle. Since the length of each $n$-cycle is $\Theta(n)$, the length of the scheme for $n$ is $\Theta(n^{2})$.

Example 2

Recall the VASS MDP $\mathcal{A}_{1}$ of Fig. 1. Here, we put $\mathbb{j}_{1}=(-\frac{1}{2},\frac{1}{2})$, $\mathbb{j}_{2}=(\frac{1}{2},-\frac{1}{2})$, and $a_{1}=a_{2}=1$. So, the cycle for $n$ is

[TABLE]

Note that the scheme does not necessarily correspond to any finite path in $\mathcal{A}$, even if the switches are disregarded. However, the scheme for $n$ determines a unique strategy $\eta_{n}$ for $\mathcal{A}$ defined below.

From Schemes to Strategies. For every $p\in Q$, we fix an MD strategy $\gamma_{p}$ such that for every $q\in Q$, the $\mathcal{P}_{q}^{\gamma_{p}}$ probability of visiting $p$ from $q$ is equal to one. Furthermore, we fix some state $p_{i}\in\mathcal{B}_{i}$ for every $1\leq i\leq\ell$.

For all finite paths that are not initiated in $p_{1}$, the strategy $\eta_{n}$ is defined arbitrarily. Otherwise, $\eta_{n}$ starts by simulating the strategy $\sigma_{1}$ for precisely $L(n)\cdot a_{1}$ steps. Then, $\eta_{n}$ remembers the state $q^{1}_{1}$ in which the simulation of $\sigma_{1}$ ended, and changes to simulating $\gamma_{p_{2}}$ until the state $p_{2}$ of $\mathcal{B}_{2}$ is reached. After reaching $p_{2}$, the strategy $\eta_{n}$ simulates $\sigma_{2}$ for precisely $L(n)\cdot a_{2}$ steps. Then, it again remembers the final state $q^{1}_{2}$ and starts to simulate $\gamma_{p_{3}}$ until $p_{3}$ is reached, and so on, until the simulation of $\sigma_{\ell}$ corresponding to the $\ell$-th segment of the first $n$-cycle is completed. Then, $\eta_{n}$ starts to simulate the switch $s_{\ell}$ of the first $n$-cycle, i.e., the strategy $\gamma_{q_{1}^{1}}$. This completes the simulation of the first $n$-cycle. In general, the $j$-th $n$-cycle (for $2\leq j\leq L(n)$) is simulated in the same way, the only difference is that every switch $s_{i}$ is simulated by $\gamma_{q_{i}^{j-1}}$ where $q_{i}^{j-1}$ is the state entered when terminating the simulation of $\sigma_{(i+1)\mod\ell}$ in the $(j{-}1)$-th $n$-cycle. This goes on until all $n$-cycles of the scheme are simulated. After that, $\eta_{n}$ behaves arbitrarily.

Lower Bound. We now show that the family of strategies $\{\eta_{n}\mid n\in\mathbb{N}\}$ witnesses the quadratic complexity. First we define $L(n)$. From standard results on MDPs [41] we know that for every $p$, the expected number of steps we keep playing $\gamma_{p}$ before hitting $p$ is finite and dependent only on $\mathcal{A}$. Hence, there exists a constant $\xi$ depending only on $\mathcal{A}$ such that also the expected change of every counter incurred while simulating $\gamma_{p}$ is bounded by $\xi$. Now let $\min_{\mathcal{A}}=\min\{\mathbb{u}(i)\mid(p,\mathbb{u},q)\in T\}$, i.e., $\min_{\mathcal{A}}$ is the minimal counter update over all transitions, and let

[TABLE]

The function $L(n)$ has been chosen so that, for all sufficiently large $n$, if the scheme for $n$ is “executed” from the point $\mathbb{n}$, i.e., if we follow the vectors of the scheme, where each switch is replaced with the vector $(\xi,\ldots,\xi)$, then the resulting trajectory never crosses any axis (recall that $\sum_{i=1}^{\ell}a_{i}\mathbb{j}_{i}\geq\mathbb{0}$).

Example 3

A trajectory for the scheme of Example 2 is shown in Fig. 3. Here, $\xi=-1$, because performing every switch takes just one transition with expected change of the counters equal to $(-1,-1)$.

Definition 3

Let $\pi=p_{0},\mathbb{u}_{1},p_{1},\mathbb{u}_{2},\ldots,p_{j}$ be a finite alternating sequence of states and vectors of $\mathbb{Q}^{d}$ (not necessarily a finite path in $\mathcal{A}$), and $m\in\mathbb{N}$. We say that $\pi$ is $m$-safe if, for every $1\leq i\leq j$, we have that $\sum_{k=1}^{i}\mathbb{u}_{k}\geq-\mathbb{m}$. Furthermore, we say that an infinite sequence $\pi=p_{0},\mathbb{u}_{1},p_{1},\mathbb{u}_{2},\ldots$ is $m$ safe-until $k$ if its prefix $p_{0},\mathbb{u}_{1},p_{1},\mathbb{u}_{2},\ldots,p_{k}$ is $m$-safe.

Now consider an infinite path $\pi=q_{0},\mathbb{u}_{1},q_{1},\mathbb{u}_{2},\ldots$ in $\mathcal{A}$ initiated in $p_{1}$. Then almost all such $\pi$’s (w.r.t. the probability measure $\mathcal{P}_{p_{1}}^{\eta_{n}}$) can be split into a concatenation of sub-paths

[TABLE]

where $\pi_{i}^{j}$ is a path with precisely $L(n)\cdot a_{i}$ transitions (resulting from simulation of $\sigma_{i}$), $\tau_{i}^{j}$ is a switching path performing the switch $s_{i}$ of the $j$-th cycle, and $\hat{\pi}$ is the remaining infinite suffix of $\pi$. Note that for every $1\leq i\leq\ell$, the paths $\pi^{1}_{i},\pi^{2}_{i},\ldots,\pi^{L(n)}_{i}$ can be concatenated and form a single path in $\mathcal{A}$ of length $L^{2}(n)$. This follows from the way of scheduling the switching strategies $\gamma_{p}$ in $\eta_{n}$. Writing $\pi=\varrho\odot\hat{\pi}$ (where $\hat{\pi}$ is the suffix of $\pi$ defined above), we denote by $\mathit{SimLen}(\pi)$ the length of $\varrho$. Note that $\mathit{SimLen}(\pi)\geq L^{2}(n)$ for almost all $\pi$.

We now focus on proving the following lemma:

Lemma 5

For every $\delta>0$ there exist $r,n_{0}\in\mathbb{N}$ such that for all $n\geq n_{0}$, the $\mathcal{P}_{p_{1}}^{\eta_{n}}$ probability of all infinite paths $\pi$ initiated in $p_{1}$ that are $r\cdot n$-safe until $\mathit{SimLen}(\pi)$ is at least $1-\delta$. Moreover, the $n_{0}$ is independent of $\delta$.

The lemma guarantees that if the strategy $\eta_{n}$ is executed in a configuration $p_{1}(r\cdot\mathbb{n})$, where $n\geq n_{0}$, then $\mathcal{P}_{p_{1}(r\cdot\mathbb{n})}^{\eta_{n}}[\mathit{Term}\geq L(n)^{2}]\geq 1-\delta$. This implies $\mathcal{L}(n)\in\Omega(n^{2})$. Hence, it remains to prove the lemma.

Proof of Lemma 5. We separately bound the probabilities of “large counter deviations” while simulating the $\sigma_{i}$’s and the switching strategies. To this end, for every $1\leq i\leq\ell$ let $\pi_{i}=p_{0},\mathbb{v}_{1},p_{1},\mathbb{v}_{2},\ldots$ be the finite path of length $L^{2}(n)$ obtained by concatenating all $\pi^{1}_{i},\pi^{2}_{i},\ldots,\pi^{L(n)}_{i}$. Furthermore, let $\mathit{Ipath}^{i}(\pi)$ the sequence obtained from $\pi_{i}$ by replacing every $\mathbb{v}_{k}$ with $\mathbb{v}_{k}-\mathbb{j}_{i}$. Intuitively, $\mathit{Ipath}^{i}(\pi)$ is $\pi_{i}$ where the transition effects are “compensated” by subtracting the expected change in the counter values per transition. We prove the following:

Lemma 6

For every $\delta>0$, there exist $c,n_{0}\in\mathbb{N}$ such that for all $n\geq n_{0}$ it holds \mathcal{P}_{p_{1}}^{\eta_{n}}(\{\pi\mid\mathit{Ipath}^{i}(\pi)\text{ is c\cdot n-safe}\})\geq 1-\delta. Moreover, the $n_{0}$ does not depend on $\delta$.

In the proof of Lemma 6, we use the martingale defined for stochastic one-counter automata in [11]. Intuitively, if $\mathit{Ipath}^{i}(\pi)$ is $n$ safe, then it must be $n$ safe in every counter. Hence, we can consider each counter one by one, abstract the other counters, and estimate the probability of being $n$ safe in each of these one-counter automata.

Similarly, we need to estimate the probability of deviating from the trajectory by performing the switches. Let $\mathit{Spath}(\pi)$ be the concatenation of all $\tau_{i}^{j}$ where $1\leq i\leq\ell$ and $1\leq j\leq L(n)$ preserving their order. We prove the following:

Lemma 7

For every $\delta>0$, there exist $c,n_{0}\in\mathbb{N}$ such that for all $n\geq n_{0}$ it holds \mathcal{P}_{p_{1}}^{\eta_{n}}(\{\pi\mid\mathit{Spath}^{i}(\pi)\text{ is c\cdot n-safe}\})\geq 1-\delta. Moreover, the $n_{0}$ does not depend on $\delta$.

Clearly, if $\mathit{Ipath}^{i}(\pi)$ is $c_{1}\cdot n$-safe for all $1\leq i\leq\ell$ and $\mathit{Spath}(\pi)$ is $c_{2}\cdot n$-safe, then $\pi$ is $(c_{1}+c_{2})\cdot(\ell{+}1)\cdot n$-safe until $\mathit{SimLen}(\pi)$. Hence, Lemma 5 is a simple consequence of Lemma 6 and Lemma 7.

Probability of Quadratic Behaviour. Now we indicate how to prove the last part of Theorem 3.1. Directly from Lemma 5, we have that $\lim_{r\to\infty}\mathcal{P}_{p_{1}(r\cdot\mathbb{n})}^{\eta_{n}}[\mathit{Term}\geq L(n)^{2}]=1$. However, observe that if $r$ is not a fixed constant, we cannot say that the size of the initial configuration is linear in $n$. Taking $r=n^{\gamma}$ for a suitable $\gamma>0$, we may rewrite the limit in the following way: $\lim_{r\to\infty}\mathcal{P}_{p_{1}(r\cdot\mathbb{n})}^{\eta_{n}}[\mathit{Term}\geq L(n)^{2}]=\lim_{n\to\infty}\mathcal{P}_{p_{1}(\mathbb{n}^{1+\gamma})}^{\eta_{n}}[\mathit{Term}\geq L(n)^{2}]=\lim_{n\to\infty}\mathcal{P}_{p_{1}\mathbb{n}}^{\eta_{n^{1/(1+\gamma)}}}[\mathit{Term}\geq L(n^{1/(1+\gamma)})^{2}]$. It can be shown that $L(n^{1/(1+\gamma)})^{2}>n^{2-\varepsilon}$, for every sufficiently large $n$, thus obtaining the last part of the Theorem 3.1.

3.4 Linearity of Angelic Termination Time

For angelic nondeterminism, we have a similar result as in the demonic one.

Theorem 3.2

The problem whether the expected angelic termination time of a given strongly connected VASS MDP $\mathcal{A}$ is linear is decidable in polynomial time. If the expected angelic termination time of $\mathcal{A}$ is not linear, then $\mathcal{L}_{a}(n)\in\Omega(n^{2})$. Furthermore, for every $\epsilon>0$ we have that

[TABLE]

Proof (Sketch)

We analyse each counter, i.e., we consider $d$ one-dimensional VASS MDPs obtained by projecting the labelling function of $\mathcal{A}$.

If it is possible to terminate in one of these one-dimensional VASS MDPs in expected linear time, then the corresponding strategy achieves linear termination also in $\mathcal{A}$. On the other hand, if this is not possible, then every one-counter has infinite angelic termination complexity. This does not mean that the $\mathcal{A}$ has infinite angelic termination complexity. However, we show that there exists a constant $c>0$ such that for sufficiently large initial configuration, the probability of runs terminating before $n^{2}/c$ transitions is sufficiently small for every one-counter. By union bound, the probability of runs terminating before $n^{2}/c$ in $\mathcal{A}$ is $1-\delta$ for some $\delta>0$. Thus, $\mathcal{L}_{a}(n)\in\Omega(n^{2})$. The last part of the theorem is proved similarly to the demonic case. ∎

4 General VASS MDPs & Conclusion

We now drop the assumption that the VASS is strongly connected. Recall that an end-component in an MDP is a set $M$ of states that is closed (i.e., for $q\in Q_{n}\cap M$ at least one outgoing transition goes to $M$, while for $q\in Q_{p}\cap M$ all the outgoing transitions must end in $M$) and strongly connected. A maximal end component (MEC) is an EC which is not contained in any larger EC. A decomposition of an MDP into MECs can be computed in polynomial time by standard algorithms [1], and each MEC of a VASS MDP induces a strongly connected VASS sub-MDP which can be analyzed as shown in previous sections. We can construct a graph whose vertices correspond to MECs of an MDP and there is an edge from $M$ to some other $M^{\prime}$ if and only if $M^{\prime}$ is reachable from $M$. If the only cycles in this graph are self-loops, we say that the original MDP is DAG-like. MECs corresponding to “leafs” of the graph (i.e. MECs that cannot be exited) are called bottom MECs.

Theorem 4.1

Theorem 3.1 holds also for DAG-like VASS MDPs, while Theorem 3.2 holds for all VASS MDPs. In particular, a DAG-like VASS MDP $\mathcal{A}$ has $\mathcal{L}_{d}(n)\in\mathcal{O}(n)$ if and only if each MEC of $\mathcal{A}$ induces a (strongly connected) VASS MDP in which $\mathcal{L}_{d}(n)\in\mathcal{O}(n)$; and $\mathcal{A}$ has $\mathcal{L}_{a}(n)\in\mathcal{O}(n)$ iff each bottom MEC of $\mathcal{A}$ has $\mathcal{L}_{a}(n)\in\mathcal{O}(n)$. Otherwise, the termination complexity of $\mathcal{A}$ is in $\Omega(n^{2})$.

Proof (Sketch)

We sketch the proof for the demonic case where there are no self-loops in the MEC graph. Then no MEC can be re-entered once left. Moreover, there is a constant $c$ s.t. whenever we enter a MEC with a counter valuation $\mathbb{v}$, the expected time to either terminate or exit the MEC, as well as the expected size of the counter valuation at the time of termination/exiting are bounded by $c\cdot|\!|\mathbb{v}|\!|$. Hence, a straightforward induction on the number of MECs shows that the expected maximal counter value as well as the expected termination time are bounded by $c^{|Q|}\cdot n$ from any initial configuration of size $n$. Since $|Q|$ does not depend on $n$, we get the result.

For non-DAG-like VASS MDPs, the situation gets much more complicated. Consider the MDP in Figure 3. There are three MECs, each a singleton ($\{p_{1}\}$, $\{p_{2}\}$, $\{f\}$). Clearly all these three MECs have a linear termination complexity. Now consider the following demonic strategy starting in configuration $p_{1}(0,n)$: select the loop until we get the configuration $p_{1}(2n,0)$; then transition to $p_{2}$ and play its loop until we get into $p_{2}(0,4n)$; then transition to $r$ and if the randomness takes us back to $p_{1}$, play the loop again until we get $p_{1}(8n,0)$, etc. ad infinitum. Clearly, the strategy eventually ends up in $f$ where it terminates. However, the expected termination time is at least $\frac{3}{4}\sum_{i=0}^{\infty}(\frac{1}{4})^{i}\cdot 4^{i+1}=3\sum_{i=0}^{\infty}(\frac{4}{4})^{i}=\infty.$

Hence, proving the linear termination complexity in general VASS does not reduce to analysing individual MECs. Moreover, it crucially depends on the concrete probabilities in transient (non-MEC) states: in Figure 3, the termination time would be finite (and linear) if the transition from $r$ to $f$ had probability $<\frac{1}{4}$. The transient behaviour of MDPs can be of course rather complex and it is not even clear whether the linear demonic termination complexity is even decidable for VASS MDPs with general structure. We see this as a very intriguing, yet complex, direction for future work.

Appendix 0.A Proofs

We start by recalling basic notions of martingale theory. A stochastic process $m^{(0)},m^{(1)},m^{(2)},\ldots$ is a martingale if the following holds for all $i\in\mathbb{N}$:

• •

$\mathbb{E}[m^{(i)}]<\infty$,

• •

$\mathbb{E}[m^{(i+1)}\mid m^{(i)},\ldots m^{(0)}]=m^{(i)}$.

By weakening the second condition into $\mathbb{E}[m^{(i+1)}\mid m^{(i)},\ldots m^{(0)}]\geq m^{(i)}$, we obtain a submartingale.

If $m^{(0)},m^{(1)},m^{(2)},\ldots$ is a (sub)martingale such that $|m^{(i+1)}-m^{(i)}|\leq d$ almost surely for all $i\in\mathbb{N}$, then the Azuma-Hoeffding inequality says that, for every $t>0$,

• •

$\mathcal{P}[m^{(i)}-m^{(0)}\geq t]\ \leq\ \exp(-t^{2}/2id^{2})$          if $m^{(0)},m^{(1)},m^{(2)},\ldots$ is a martingale,

• •

$\mathcal{P}[m^{(i)}-m^{(0)}\leq-t]\ \leq\ \exp(-t^{2}/2id^{2})$        if $m^{(0)},m^{(1)},m^{(2)},\ldots$ is a submartingale.

0.A.1 A proof of Lemma 1

We start by recalling the results of [41]. Let $\mathcal{N}=\left(Q,(Q_{n},Q_{p}),T,P\right)$ be a strongly connected $\mathbb{Q}$-labeled MDP. Consider the following linear program:

[TABLE]

This linear program is feasible, and the minimal value of $x$ is equal to

[TABLE]

Let $\bar{x},\bar{z}_{p}$ be the components of an optimal solution, and let $p\in Q$ be some fixed initial state. For every $i\in\mathbb{N}$, let $S^{(i)}$ and $C^{(i)}$ be functions assigning to every infinite path $\pi=p_{0},\mathbb{u}_{1},p_{1},\mathbb{u}_{2},\ldots$ initiated in $p$ the state $p_{i}$ and the sum $\sum_{j=1}^{i}\mathbb{u}_{j}$, respectively (we put $C^{(0)}(\pi)=0$). Let $\sigma\in\Sigma$ be an arbitrary strategy. Almost identical computation as in [9, 12] gives that the stochastic process $m^{(0)},m^{(1)},\ldots$, where $m^{(i)}=C^{(i)}+\bar{z}_{S^{(i)}}-i\cdot\bar{x}$, is a supermartingale (over the probability space determined by $\sigma$).

Our aim is to show that there exists $a\in(0,1)$ and $i_{0}\in\mathbb{N}$ depending only on $\mathcal{M}$ such that for an arbitrary strategy $\sigma$, every $p\in Q$, and all $i\geq i_{0}$ we have that $\mathcal{P}_{p}^{\sigma}[\mathit{Dec}=i]\leq a^{i}$. From this we immediately obtain

[TABLE]

for some constant $c$ depending only on $\mathcal{M}$.

Now consider the supermartingale of the first paragraph applied to infinite paths in $\mathcal{M}$ (under the strategy $\sigma$). Let $\pi=p_{0},\mathbb{u}_{1},p_{1},\mathbb{u}_{2},\ldots$ be an infinite path such that $\mathit{Dec}(\pi)=i$. Then $C^{(i)}(\pi)\geq-(1+\delta)$ for some fixed $\delta$ depending only on $\mathcal{M}$, because the rewards are bounded. Furthermore, the maximal difference between $\bar{z}_{p}$ and $\bar{z}_{q}$ for $p,q\in Q$ is also bounded by some constant depending only on $\mathcal{M}$. Hence, $m^{(i)}(\pi)-m^{(0)}(\pi)\geq\mu-i\cdot\bar{x}$ for some constant $\mu$ depending only on $\mathcal{M}$ (recall that $\bar{x}$ is negative). For every $i\geq i_{0}$ where $i_{0}:=-2\mu/\bar{x}$, we obtain $\mu-i\cdot\bar{x}\leq i\cdot\bar{x}/2-i\cdot\bar{x}=-(i\cdot\bar{x}/2)$ where $i\cdot\bar{x}/2<0$. Thus, we obtain

[TABLE]

Since the supermartingale $m^{(0)},m^{(1)},\ldots$ can change in one step at most by a constant $\varrho$ (depending only on $\mathcal{M}$), applying Azuma’s inequality yields

[TABLE]

where $a=\exp(-\bar{x}^{2}/8\varrho^{2})\in(0,1)$, for all $i\geq i_{0}$.

0.A.2 A proof of Lemma 6

We assume a fixed $1\leq i\leq\ell$. Recall the strategy $\sigma_{i}$ and the BSCC $\mathcal{B}_{i}$ associated to the increment $\mathbb{j}_{i}$ (see Section 3.2). For every path $\pi$ initiated in $p_{1}$, let $\mathit{Ipath}^{i}(\pi)=q_{0},\mathbb{v}_{1},q_{1},\mathbb{v}_{2},\dots,q_{L^{2}(n)}$, and for every $1\leq j\leq d$, consider the sequence $\mathit{Ipath}^{i}_{j}(\pi)$ obtained by projecting every $\mathbb{v}_{k}$ to its $j$-th component, i.e., $\mathit{Ipath}^{i}_{j}(\pi)=q_{0},\mathbb{v}_{1}(j),q_{1},\mathbb{v}_{2}(j),\dots,q_{L^{2}(n)}$.

Our aim is to show that, for every $\delta>0$ and every $1\leq j\leq d$, there exist $c,n_{0}\in\mathbb{N}$ such that the $\mathcal{P}_{p_{1}}^{\sigma_{i}}$ probability of all $\pi$ initiated in $p_{1}$ such that $\mathit{Ipath}^{i}_{j}(\pi)$ is $c\cdot n$ safe is at least $1-\delta$. Observe that Lemma 6 is a direct consequence of this claim.

Observe that $\mathcal{B}_{i}$, where the nondeterministic choice is resolved by $\sigma_{i}$, and the counter update vectors are projected to their $j$th component, can be seen as a one-counter automaton. The long-run average change of the counter per transition in this automaton is $\mathbb{j}_{i}(j)$. Recall that $\mathit{Ipath}^{i}(\pi)$ was obtained from the concatenated paths $\pi^{1}_{i},\pi^{2}_{i},\ldots,\pi^{L(n)}_{i}$ by subtracting the increment $\mathbb{j}_{i}$ from each vector occurring in this sequence. Hence, we need to subtract $\mathbb{j}_{i}(j)$ from every counter update on every transition of $\mathcal{B}_{i}$. Thus, we obtain a one-counter automaton $\hat{\mathcal{B}}_{i}$. A trivial but crucial observation is that the long-run average change of the counter per transition in $\hat{\mathcal{B}}_{i}$ is zero.

The $\mathcal{P}_{p_{1}}^{\sigma_{i}}$ probability of all $\pi$ initiated in $p_{1}$ such that $\mathit{Ipath}^{i}_{j}(\pi)$ is not $c\cdot n$ safe is equal to the probability that a run of $\hat{\mathcal{B}}_{i}$ initiated in $q(0)$, where $q$ is the starting state of $\pi^{1}_{i}$, decreases the counter to $-c\cdot n$ or below during the first $L^{2}(n)$ transitions. An upper bound on the latter probability can be established using the martingale for probabilistic one-counter automata introduced in [11] (here we use a slightly modified version of this martingale which better suits our purposes). Due to [11], for every state $p^{(0)}$ of $\hat{\mathcal{B}}_{i}$ and every $c\in\mathbb{N}$, there exists a vector $\mathbb{y}\in[0,\infty)^{|\hat{\mathcal{B}}_{i}|}$ such that the stochastic process defined by

[TABLE]

is a martingale, where $C^{(0)}=0$, $C^{(k)}=\sum_{s=1}^{k}\mathbb{v}_{s}(j)$ is a random variable returning the accumulated counter change after $k$ steps, and $p^{(k)}$ is a random variable returning the control state entered after $k$ steps. Moreover, the vector $\mathbb{y}_{j}$ satisfies $0\leq\|\mathbb{y}_{j}\|\leq 2|\hat{\mathcal{B}}_{i}|/x_{\min}^{|\hat{\mathcal{B}}_{i}|}$, where $x_{\min}$ is the minimum probability used in the transitions of $\hat{\mathcal{B}}_{i}$.

Note that if the accumulated counter change drops to $-c\cdot n$ or below for the first time after exactly $k$ transitions, the martingale does not change its value from this point on, and remains equal to $m^{(k)}_{i,j}$. Let $\mathbb{y}=\max_{j}\|\mathbb{y}_{j}\|$. If $m^{(L^{2}(n))}_{i,j}\geq-cn+\|\mathbb{y}\|$ then the value $C^{(L^{2}(n))}$ is at least $-cn$ for every $k\leq L^{2}(n)$. Hence, the probability that a run of $\hat{\mathcal{B}}_{i}$ initiated in $p_{i}(0)$ decreases the counter to $-cn$ or below during the first $L^{2}(n)$ transitions is less or equal to $P(m^{(L^{2}(n))}_{i,j}\leq-cn+\|\mathbb{y}\|+1)$. Furthermore, for all $n\geq\|\mathbb{y}\|+1+m^{(0)}_{i,j}$ we have that

[TABLE]

by applying Azuma’s inequality, where $\alpha$ is a suitable constant dependent only on $\hat{\mathcal{B}}_{i}$.

The above holds for every $j\in\{1,\ldots,d\}$. Hence, the probability of all $\mathcal{P}_{p_{1}}^{\sigma_{i}}$ probability of all $\pi$ initiated in $p_{1}$ such that $\mathit{Ipath}^{i}(\pi)$ is not $c\cdot n$ safe is less or equal to $d\cdot\mathrm{exp}\left(-(c-1)^{2}/\alpha\right)$ for every sufficiently large $n$. To achieve $d\cdot\mathrm{exp}\left(-(c-1)^{2}/\alpha\right)\leq\delta$, we can put $c=\lceil\sqrt{\alpha(\ln d-\ln\delta)}\rceil+1$.

0.A.3 A proof of Lemma 7

First, we bound the expected number of transitions used in executing one switch. Let $x_{\min}$ be the minimum probability appearing in the VASS MDP, and let $p,q\in Q$. There is a path of length at most $|Q|-1$ which we may follow with probability at least $x_{\min}^{|Q|-1}$. If successful, we are done, otherwise we end up in some state $p^{\prime}$ and again there is some path from $p^{\prime}$ to $q$ of length at most $|Q|-1$ and the probability of traversing this path is still at least $x_{\min}^{|Q|-1}$.

If we use the number $x_{\min}^{|Q|-1}$ as the (lower bound on the) probability of success, the random variable counting the number of attempts until the first success has a geometric distribution. Its expected value is then $1/x_{\min}^{(|Q|-1)}$. Since every attempt uses at most $|Q|-1$ transitions, the expected number of used transitions is bounded from above by $\lambda=(|Q|-1)\cdot 1/x_{\min}^{(|Q|-1)}$.

Let $X$ be the random variable equal to the length of $\mathit{Spath}(\pi)$. Since the number of switches is $L(n)$, the expected value of $\mathit{Spath}(\pi)$ is bounded from above by $\lambda\cdot L(n)$. Let $\delta>0$. Surely $P(X\geq\delta^{-1}\cdot\lambda\cdot L(n))\leq P(X\geq\delta^{-1}\mathbb{E}[X])$. By Markov inequality, we obtain that $P(X\geq\delta^{-1}\mathbb{E}[X])\leq\delta$. Therefore, with probability at most $\delta$, we use more than $\delta^{-1}\cdot\lambda L(n)$ transitions.

The minimal update over all transitions is $\min_{\mathcal{A}}$. If $\min_{\mathcal{A}}\geq 0$, then $c=0$ since no transition can decrease the counters and the set of paths $\pi$ such that $\mathit{Spath}(\pi)$ is 0 safe has probability one. For $\min_{\mathcal{A}}<0$, the set of paths $\pi$ such that $\mathit{Spath}(\pi)$ is $-\min_{\mathcal{A}}\delta^{-1}\lambda\cdot L(n)$ safe has probability at least $1-\delta$. Since $L(n)\leq n$, taking $c=-\min_{\mathcal{A}}\delta^{-1}\lambda$ completes the proof.

0.A.4 A proof of the last part of Theorem 3.1

We show that for every $\varepsilon>0$ we can choose $\gamma>0$ such that

[TABLE]

From Lemma 5, we have that $\lim_{r\to\infty}\mathcal{P}_{p_{1}(r\cdot\mathbb{n})}^{\eta_{n}}[\mathit{Term}\geq L(n)^{2}]=1$. Rewriting the limit, we obtain

[TABLE]

Let $c=\ell\cdot\xi-\sum_{j=1}^{\ell}a_{j}\cdot\min_{\mathcal{A}}+2$. Then $L(n)\geq n/c$ by the definition of $L(n)$ (for $n$ sufficiently large). We need to show that $L(n^{1/(1+\gamma)})^{2}\geq n^{2-\varepsilon}$ for some $\gamma>0$. Surely

[TABLE]

For $n$ sufficiently large, we have $n^{\gamma/(1+\gamma)}/c>1$. Therefore,

[TABLE]

Let $\gamma$ be such that $n^{2-3\gamma/(1+\gamma)}=n^{2-\varepsilon}$, therefore $3\gamma/(1+\gamma)=\varepsilon$. Multiplying by $1+\gamma$ we get $\varepsilon+\varepsilon\gamma-3\gamma=0$. Therefore, $\gamma=\varepsilon/(3-\varepsilon)$. This completes the proof.

0.A.5 A proof of Theorem 3.2

The proof is very similar to the one of Lemma 1. Again, we recall the results of [12] for one-counter machines. We consider the following linear program:

[TABLE]

This linear program is feasible, and the maximal value of $x$ is equal to

[TABLE]

Moreover, we can assume that for all $q\in Q$ we have $\bar{z}_{q}\geq 0$. Direct corollary of [12, Proposition 5,(B)] is the following Lemma:

Lemma 8

Let $(\bar{x},(\bar{z}_{q})_{q\in Q})$ be a solution of the linear program above. If $\bar{x}<0$ then $\mathcal{L}_{a}(n)\in\Theta(n)$.

Moreover, we use (similarly to the proof of Lemma 1) that the stochastic process $m^{(0)},m^{(1)},\dots,$ where

[TABLE]

is a submartingale.

Now we use these results on one-dimensional VASS-MDPs to obtain the proof for $d$-dimensional VASS-MDP $\mathcal{A}$ by simply considering $d$ projections on one counter.

A trivial observation gives the following result.

Lemma 9

Let $\mathcal{A}$ be a $d$-dimensional VASS-MDP, $\mathcal{A}_{1},\dots,\mathcal{A}_{d}$ corresponding one-dimensional VASS-MDPs obtained by projecting the labels onto respective coordinate. If at least one of the one-dimensional VASS-MDPs has linear angelic termination time, then $\mathcal{A}$ has also linear angelic termination time (using the same strategy).

In order to obtain the result for at least quadratic termination, we use the Azuma inequality for all the submartingales obtained from the one-dimensional VASS-MDPs.

Let $m_{j}^{(0)},m_{j}^{(1)}$ be the submartingale for $\mathcal{A}_{j}$, $\bar{Z}_{j}=\max_{q\in Q}\bar{z}_{q}$ obtained from the corresponding linear program (and assuming all values $\bar{z}_{q}$ are non-negative).

Given an initial configuration $p(n,\dots,n)$, the probability that the $j$-th counter decreases below zero in $t$ steps can be bounded from above:

[TABLE]

where $Z_{j}$ and $\alpha$ are constants independent of $n$.

Let $Z=\max_{j=1,\dots,d}Z_{j}$ and $n\geq 2Z$, then:

[TABLE]

Observe that there exists a suitable constant $c>0$ such that

[TABLE]

since $d$ and $\alpha$ are constants (depending only on $\mathcal{A}$). Therefore, taking $t=n^{2}/c$, we obtain that the probability of some counter decreasing below zero is $1-\delta$ for some $\delta>0$, and thus $\mathcal{L}_{a}(n)\in\Omega(n^{2})$.

Let $\varepsilon>0$ and $t=n^{2-\varepsilon}$, then

[TABLE]

This completes the proof of Theorem 3.2.

0.A.6 A proof of Theorem 4.1

We can divide the set of states of $\mathcal{A}$ into the states belonging to some MEC and transient states. We rely on the two following facts:

For every strategy, the expected number of transitions from a transient state to some MEC state can be bounded by a constant $k$ (a number dependent only on $\mathcal{A}$ and not the size of the initial configuration). 2. 2.

The asymptotic complexity of a MEC does not depend on the initial state.

First, we consider the demonic case. In DAG-like VASS-MDP, the only loops in the MEC decomposition are self-loops, i.e., once we leave MEC $M$ and visit a different MEC $M^{\prime}$, we may never return to $M$. Moreover, there is a probability $p<1$ such that for every MEC $M$ and every strategy, we revisit $M$ after leaving it (i.e., execute the self loop on $M$) with probability at most $p$.

For the “if” direction, we assume that the initial state is in a MEC $M$. We compute the upper bound on the expected number of transitions before terminating or arriving into another MEC. Let $Q^{\prime}$ be the states of every MEC different from $M$. We know that if MEC $M$ is linear then there exists $\mathbb{w}_{M}>0$ such that all increments $\mathbb{i}_{1},\dots,\mathbb{i}_{r}$ in $M$ satisfy $\mathbb{i}_{j}\cdot\mathbb{w}_{M}<0$. Let us consider a $\mathbb{Q}$-labeled MDP $\mathcal{A}_{\mathbb{w}}$ obtained from $\mathcal{A}$ by replacing each label $\mathbb{u}\in\mathbb{Z}^{d}$ by $\mathbb{u}\cdot\mathbb{w}_{M}\in\mathbb{Q}$.

Now we construct a supermartingale similar to the one in the proof of Lemma 1. Again, for every $i\in\mathbb{N}$, let $S^{(i)}$ and $C^{(i)}$ be functions assigning to every infinite path $\pi=p_{0},u_{0},p_{1},u_{2},\dots$ in $\mathcal{A}_{\mathbb{w}}$ initiated in $p$ the state $p_{i}$, and the sum $\mathbb{w}\cdot\mathbb{n}+\sum_{j=1}^{i}u_{j}$ (where $\mathbb{n}=(n,n,\dots,n)$ is the initial counter vector in $\mathcal{A}$). Furthermore, let $M.steps(i)$ and $T.steps(i)$ be functions counting for every infinite path $\pi$ the number of transitions in the MEC $M$ and in the transient states before entering a MEC different from $M$ (a transition $t=(q,\mathbb{u},q^{\prime})$ is in $M$ if both $q,q^{\prime}$ are in $M$).

Let $p$ be any initial state and $\sigma$ arbitrary strategy. Then the following sequence of random variables is a supermartingale:

[TABLE]

where $K$ is sufficiently large constant. We want to compute the expected value of $M.steps$. For every $i$ we have:

[TABLE]

We know that $\mathbb{E}_{p}^{\sigma}(T.steps)\leq k$ and $\mathbb{E}_{p}^{\sigma}(\bar{z}_{S^{(i)}})$ is bounded by a constant. Moreover, $m^{(0)}\geq\mathbb{w}\cdot\mathbb{n}+K_{1}$ where $K_{1}$ is a constant depending only on $\mathcal{A}_{\mathbb{w}}$. Using the property of a supermartingale, we obtain

[TABLE]

Since $\bar{x}<0$, we have for every $i\in\mathbb{N}$ that

[TABLE]

therefore $\mathbb{E}_{p}^{\sigma}(M.steps)+\mathbb{E}_{p}^{\sigma}(T.steps)\leq c\cdot n$ for a suitable constant $c$.

The time spent in one MEC can be used to increase some counters that can be used by MECs visited later. However, once we visit MEC $M^{\prime}$, we never return to $M$. We define the height of MEC $M$ to be the length of a longest path in the MEC decomposition from $M$ into a bottom MEC (if MEC $M^{\prime}$ can be visited from $M$, then $M^{\prime}$ has higher height).

Let $\max_{\mathcal{A}}=\max\{\|\mathbb{u}\|;(q,\mathbb{u},q^{\prime})\in T\}$ be the size of maximum counter change per transition.

We assume that for every MEC, the demonic termination complexity is bounded by $rn$ for all $n\in\mathbb{N}$. Let $i$ be the height of the MEC containing the initial state (or $i$ is such that $i-1$ is the height of a reachable MEC with the largest height). By induction on $i$, we prove that the expected termination time is bounded by $(\max_{\mathcal{A}}\cdot r+1)^{i}\cdot n$ for $n$ sufficiently high.

If $i=0$, then $\mathcal{L}_{d}(n)\leq rn$.

Assume that the height of MEC $M$ containing the initial configuration is $i+1$ and and the expected termination time for $i$ is bounded by $(r+1)^{i}\cdot n$ (if we start in some transient state, the expected number of steps into a MEC with height at most $i$ is constant and the induction step holds). We divide every path $\pi=\pi_{1}\pi_{2}$ where $\pi_{1}$ is the part of $\pi$ prior the arrival into the lower MEC. The expected length of $\pi_{1}$ is bounded by $rn$. Therefore, we have the following upper bound on the expected size of counters when arriving into the lower MEC: $n+rn\cdot\max_{\mathcal{A}}=(\max_{\mathcal{A}}\cdot r+1)\cdot n$.

Using induction hypothesis, the expected length of $\pi$ is then $(\max_{\mathcal{A}}\cdot r+1)^{i+1}\cdot n$ which completes the proof.

For the “only if” direction, consider an initial state to be in a MEC with at least quadratic termination complexity. Using the corresponding strategy, we obtain the result.

Now we turn to the angelic case. If all bottom MECs are linear, there exists a strategy reaching one of the MECs in expected constant time. Therefore, the complexity is the same as in the bottom MEC, i.e., linear. If some of the bottom MECs is at least quadratic, then starting in that MEC, we obtain at least quadratic termination complexity.