一句话：为 VASS 终止时间的渐近复杂度提供多项式时间判定与分类，并给出最优多项式次数计算。
论文研究带状态向量加法系统（VASS）终止时间的渐近界，重点关注多项式界。作者首先给出多项式时间算法判定 VASS 是否具有线性渐近复杂度，并证明非线性时至少为二次。随后按循环的定量性质对 VASS 分类，指出这些性质中的奇点是导致非多项式复杂度的关键；若无奇点，终止复杂度必为 Θ(n^k)，其中 k≤d（d 为 VASS 维数），并可在多项式时间内算出最优 k。对一般 VASS，同一算法基于构造 ranking function 的完备技术，可给出有效下界 Ω(n^k)。结果依赖于对 VASS 动态几何的新认识。
Vector Addition Systems with States (VASS) provide a well-known and fundamental model for the analysis of concurrent processes, parameterized systems, and are also used as abstract models of programs in resource bound analysis. In this paper we study the problem of obtaining asymptotic bounds on the termination time of a given VASS. In particular, we focus on the practically important case of obtaining polynomial bounds on termination time. Our main contributions are as follows: First, we present a polynomial-time algorithm for deciding whether a given VASS has a linear asymptotic complexity. We also show that if the complexity of a VASS is not linear, it is at least quadratic. Second, we classify VASS according to quantitative properties of their cycles. We show that certain singularities in these properties are the key reason for non-polynomial asymptotic complexity of VASS. In absence of singularities, we show that the asymptotic complexity is always polynomial and of the form Θ(nk), for some integer k ≤ d, where d is the dimension of the VASS. We present a polynomial-time algorithm computing the optimal k. For general VASS, the same algorithm, which is based on a complete technique for the construction of ranking functions in VASS, produces a valid lower bound, i.e., a k such that the termination complexity is Ω(nk). Our results are based on new insights into the geometry of VASS dynamics, which hold the potential for further applicability to VASS analysis.
@inproceedings{paperbot4341,
title = {Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS},
author = {Tomáš Brázdil and Krishnendu Chatterjee and Antonín Kučera and Petr Novotný and Dominik Velan and Florian Zuleger},
booktitle = {LICS},
year = {2018},
doi = {10.1145/3209108.3209191}
}