VASS MDP 多项式渐近估计的高效分析

带状态的向量加法系统上的马尔可夫决策过程（VASS MDP）是一种有限状态模型，结合了非确定性和概率行为，并附加了可在每次状态转换中递增或递减的非负整数计数器。VASS MDP 可用作具有许多可判定性质的概率程序的抽象。在本文中，我们开发了分析 VASS MDP 渐近行为的技术。即，对于每个大小为 n 的初始配置，我们考虑到达某个计数器为负的配置所需的转换次数。我们证明，对于一个强连通的 VASS MDP，要么存在一个整数 k ≤ 2^d · 3^{|T|}（其中 d 为维度，|T| 为 VASS MDP 的转换数），使得对所有 ε > 0 和所有充分大的 n，VASS MDP 的复杂度以至少 1−ε 的概率介于 n^{k−ε} 和 n^{k+ε} 之间；要么对所有 ε > 0 和所有充分大的 n，VASS MDP 的复杂度以至少 1−ε 的概率至少为 2^{n^{1−ε}}。我们证明哪种情形成立是可判定的，且 k 可以在关于所考虑 VASS MDP 大小的多项式时间内计算。我们还为 VASS 马尔可夫链提供了完整的渐近复杂度分类。