一句话：证明带恶魔非确定性的 VASS 的终止复杂性是否属于固定 Grzegorczyk 层可在多项式时间判定，并揭示层级增长间隙。
论文研究 VASS（向量加法系统）的终止复杂性 L：对每个 n，L(n) 是从所有计数器不超过 n 的配置出发的最长不停机计算长度。作者针对带恶魔非确定性的 VASS，证明对每个固定 k，判定 L 是否属于 Grzegorczyk 层级第 k 层 G_k 可在多项式时间内完成。进一步，若 L 属于 G_k，则 L 的增长至少与 G_{k+1} 的生成函数 F_{k+1} 一样快。因此，对每个终止的 VASS，可用最小的 k 使 L∈G_k 来合理刻画其终止复杂性的增长速度。
The termination complexity of a given VASS is a function L assigning to every n the length of the longest non-terminating computation initiated in a configuration with all counters bounded by n. We show that for every VASS with demonic nondeterminism and every fixed k, the problem whether L ϵ Gk, where Gk is the k-th level in the Grzegorczyk hierarchy, is decidable in polynomial time. Furthermore, we show that if L ϵ G, then L grows at least as fast as the generator Fk+1 of Gk+1. Hence, for every terminating VASS, the growth of L can be reasonably characterized by the least k such that L ϵ Gk.
DOI 原文 ·
@inproceedings{paperbot5496,
title = {Efficient Analysis of VASS Termination Complexity},
author = {Antonín Kučera and Jérôme Leroux and Dominik Velan},
booktitle = {LICS},
year = {2020},
doi = {10.1145/3373718.3394751}
}