Efficient Analysis of Polynomial Asymptotic Estimates for VASS MDPs
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866910862538702848 |
|---|---|
| author | Ajdarów, Michal |
| author_facet | Ajdarów, Michal |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2503_05006 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Efficient Analysis of Polynomial Asymptotic Estimates for VASS MDPs Ajdarów, Michal Formal Languages and Automata Theory 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. |
| title | Efficient Analysis of Polynomial Asymptotic Estimates for VASS MDPs |
| topic | Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2503.05006 |