VASS程序多项式终止复杂性的判定
Deciding Polynomial Termination Complexity for VASS Programs
摘要：
我们表明，对于每一个固定的$k\geq 3$，一个给定的恶魔VASS的终止/计数器复杂度是否是$\mathcal{O}(n^k)$，$Ω(n^{k})$，和$Θ(n^{k})$的问题是NP完全，NP完全，DP完全，分别。我们还为$k\leq 2$对这些问题的复杂性进行了分类。这表明，多项式时间算法设计的强连接恶魔VASS在以前的作品不能扩展到一般情况下。然后，我们证明了VASS对策的相同问题是PSPACE完全的。同样，我们也对$k\leq 2$的复杂性进行了分类。有趣的是，易于处理的恶魔VASS和VASS游戏的子类，通过绑定某些结构参数，这开辟了道路，应用程序在程序分析，尽管提出了较低的复杂性界限。
英文摘要：
We show that for every fixed $k\geq 3$, the problem whether the termination/counter complexity of a given demonic VASS is $\mathcal{O}(n^k)$, $Ω(n^{k})$, and $Θ(n^{k})$ is coNP-complete, NP-complete, and DP-complete, respectively. We also classify the complexity of these problems for $k\leq 2$. This shows that the polynomial-time algorithm designed for strongly connected demonic VASS in previous works cannot be extended to the general case. Then, we prove that the same problems for VASS games are PSPACE-complete. Again, we classify the complexity also for $k\leq 2$. Interestingly, tractable subclasses of demonic VASS and VASS games are obtained by bounding certain structural parameters, which opens the way to applications in program analysis despite the presented lower complexity bounds.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
