Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Efficient Analysis of Polynomial Asymptotic Estimates for VASS MDPs

Michal Ajdarów

TL;DR

The paper addresses the problem of understanding polynomial asymptotic growth for termination and counter-related measures in strongly connected VASS MDPs, where both nondeterministic and probabilistic transitions occur. By combining the cMD (counterless-memoryless) decomposition with AKCONCUR23 insights and a pair of constraint systems, it achieves a dichotomy: the relevant complexities are either tight polynomials n^k (with k ≤ 2^d·3^{|T|}) or exponential 2^n, and it proves these cases are decidable in polynomial time with the exponent k computable likewise. It further provides a complete classification for strongly connected VASS Markov chains, showing that each measure is either unbounded or has tight bounds of n or n^2, decidable in polynomial time. Additionally, the work introduces fixed-probability bounds as an intuitive alternative to asymptotic estimates, enriching the interpretability of results. Overall, the contributions advance the tractability of asymptotic analyses for multi-dimensional VASS processes and probabilistic programs with unbounded resources, enabling precise complexity characterizations and practical decision procedures.

Abstract

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 \(ε>0 \) and all sufficiently large \(n\) it holds that the complexity of the VASS MDP lies between \(n^{k-ε} \) and \(n^{k+ε} \) with probability at least \(1-ε\), or it holds for all \(ε>0 \) and all sufficiently large \(n\) that the complexity of the VASS MDP is at least \(2^{n^{1-ε}} \) with probability at least \(1-ε\). 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.

Efficient Analysis of Polynomial Asymptotic Estimates for VASS MDPs

TL;DR

The paper addresses the problem of understanding polynomial asymptotic growth for termination and counter-related measures in strongly connected VASS MDPs, where both nondeterministic and probabilistic transitions occur. By combining the cMD (counterless-memoryless) decomposition with AKCONCUR23 insights and a pair of constraint systems, it achieves a dichotomy: the relevant complexities are either tight polynomials n^k (with k ≤ 2^d·3^{|T|}) or exponential 2^n, and it proves these cases are decidable in polynomial time with the exponent k computable likewise. It further provides a complete classification for strongly connected VASS Markov chains, showing that each measure is either unbounded or has tight bounds of n or n^2, decidable in polynomial time. Additionally, the work introduces fixed-probability bounds as an intuitive alternative to asymptotic estimates, enriching the interpretability of results. Overall, the contributions advance the tractability of asymptotic analyses for multi-dimensional VASS processes and probabilistic programs with unbounded resources, enabling precise complexity characterizations and practical decision procedures.

Abstract

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 , 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 , where is the dimension and the number of transitions of the VASS MDP, such that for all and all sufficiently large it holds that the complexity of the VASS MDP lies between and with probability at least , or it holds for all and all sufficiently large that the complexity of the VASS MDP is at least with probability at least . We show that it is decidable which case holds and the 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.

Paper Structure

This paper contains 29 sections, 47 theorems, 56 equations, 2 figures, 3 tables.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. VASS Markov Decision Processes
  4. Asymptotic Complexity Measures for VASS MDPs
  5. Complexity of VASS Computations
  6. Asymptotic Estimates
  7. Strongly Connected VASS MDPs
  8. Informal Description
  9. Constraint systems \ref{['fig-systems']} and \ref{['fig-systems']}
  10. Formal Description
  11. VASS Markov Chains
  12. Conclusions
  13. Additional Definitions
  14. Technical Lemmas
  15. Operations on Multi-components
  16. ...and 14 more sections

Key Result

Theorem 5

Let $f:\mathbb{R}\rightarrow\mathbb{R}$ be such that $\lim_{n\rightarrow\infty} \frac{f( n)}{f( n^{1+\epsilon})}=0$ for every $\epsilon>0$. Then:

Figures (2)

  • Figure 1: A probabilistic program with infinite expected running time for every $N\geq 1$, and its $1$-dimensional VASS MDP model $\pazocal{A}$.
  • Figure 2: Constraint systems defined for a given VASS MDP $\pazocal{A} = \left(Q, (Q_n,Q_p),T,P \right)$ with counters $\mathit{Count}$.

Theorems & Definitions (54)

  • Definition 1
  • Remark 2
  • Remark 3
  • Definition 4
  • Theorem 5
  • Theorem 6
  • Lemma 7: Cited from AKCONCUR23
  • Lemma 8
  • Lemma 9
  • Remark 10
  • ...and 44 more