Efficient Analysis of Polynomial Asymptotic Estimates for VASS MDPs

Markov decision process over vector addition system with states (VASS MDP) is a finite state model combining non-deterministic and probabilistic behavior, augmented with non-negative integer counters that can be incremented or decremented during each state transition. VASS MDPs can be used as abstractions of probabilistic programs with many decidable properties. In this paper, we develop techniques for analyzing the asymptotic behavior of VASS MDPs. That is, for every initial configuration of size $n$, we consider the number of transitions needed to reach a configuration with some counter negative. We show that given a strongly connected VASS MDP there either exists an integer $k\leq 2^d\cdot 3^{|T|}$, where $d$ is the dimension and $|T|$ the number of transitions of the VASS MDP, such that for all $\epsilon>0$ and all sufficiently large $n$ it holds that the complexity of the VASS MDP lies between $n^{k-\epsilon}$ and $n^{k+\epsilon}$ with probability at least $1-\epsilon$, or it holds for all $\epsilon>0$ and all sufficiently large $n$ that the complexity of the VASS MDP is at least $2^{n^{1-\epsilon}}$ with probability at least $1-\epsilon$. We show that it is decidable which case holds and the $k$ is computable in time polynomial in the size of the considered VASS MDP. We also provide a full classification of asymptotic complexity for VASS Markov chains.