VASS中快速终止性检测的有效算法
Efficient Algorithms for Checking Fast Termination in VASS
摘要：
带状态的向量加法系统（VASS）由配备有d个计数器的有限状态空间组成，其中在每个转换中，每个计数器递增、递减或保持不变。VASS为分析并发进程、参数化系统提供了一个基本模型，也可作为程序的抽象模型用于边界分析。虽然终止是基本的活性属性，它询问给定模型是否总是终止的定性问题，但更一般的定量问题要求终止步骤的数量。在定量界领域的一个基本问题是获得渐近界的终止时间。大的渐近界，如指数或更高的已经表明，要么有一些错误的建模，或模型是没有用的实践。因此，我们专注于VASS的多项式渐近界。虽然一些众所周知的方法（例如，字典排序函数）对于多项式边界既不可靠也不完整，其他方法仅给出了用于上界的可靠方法。在这项工作中，我们的主要贡献如下：第一，对于线性渐近界，我们提出了一个健全的和完整的方法VASS，而且，我们的算法运行在多项式时间。其次，我们根据循环向量的法线对VASS进行分类。我们表明，在正常的奇异性是渐近界，如指数和非小学VASS的关键原因。在没有奇异性的情况下，我们证明了渐近复杂性界总是多项式的形式$Θ(n^k)$，对于一些k $\leq$ d。我们提出了一个算法，时间复杂度多项式的大小的VASS和指数的维数d，计算最佳k。
英文摘要：
Vector Addition Systems with States (VASS) consists of a finite state space equipped with d counters, where in each transition every counter is incremented, decremented, or left unchanged. VASS provide a fundamental model for analysis of concurrent processes, parametrized systems, and they are also used as abstract models for programs for bounds analysis. While termination is the basic liveness property that asks the qualitative question of whether a given model always terminates or not, the more general quantitative question asks for bounds on the number of steps to termination. In the realm of quantitative bounds a fundamental problem is to obtain asymptotic bounds on termination time. Large asymptotic bounds such as exponential or higher already suggest that either there is some error in modeling, or the model is not useful in practice. Hence we focus on polynomial asymptotic bounds for VASS. While some well-known approaches (e.g., lexicographic ranking functions) are neither sound nor complete with respect to polynomial bounds, other approaches only present sound methods for upper bounds. In this work our main contributions are as follows: First, for linear asymptotic bounds we present a sound and complete method for VASS, and moreover, our algorithm runs in polynomial time. Second, we classify VASS according the normals of the vectors of the cycles. We show that singularities in the normal are the key reason for asymptotic bounds such as exponential and non-elementary for VASS. In absence of singularities, we show that the asymptotic complexity bound is always polynomial and of the form $Θ(n^k)$, for some k $\leq$ d. We present an algorithm, with time complexity polynomial in the size of the VASS and exponential in dimension d, to compute the optimal k.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
