A recent breakthrough by K\"unnemann, Mazowiecki, Sch\"utze, Sinclair-Banks, and Wegrzycki (ICALP, 2023) bounds the running time for the coverability problem in $d$-dimensional vector addition systems under unary encoding to $n^{2^{O(d)}}$, improving on Rackoff's $n^{2^{O(d\lg d)}}$ upper bound (Theor. Comput. Sci., 1978), and provides conditional matching lower bounds. In this paper, we revisit Lazi\'c and Schmitz' "ideal view" of the backward coverability algorithm (Inform. Comput., 2021) in the light of this breakthrough. We show that the controlled strongly monotone descending chains of downwards-closed sets over $\mathbb{N}^d$ that arise from the dual backward coverability algorithm of Lazi\'c and Schmitz on $d$-dimensional unary vector addition systems also enjoy this tight $n^{2^{O(d)}}$ upper bound on their length, and that this also translates into the same bound on the running time of the backward coverability algorithm. Furthermore, our analysis takes place in a more general setting than that of Lazi\'c and Schmitz, which allows to show the same results and improve on the 2EXPSPACE upper bound derived by Benedikt, Duff, Sharad, and Worrell (LICS, 2017) for the coverability problem in invertible affine nets.
翻译:Künnemann、Mazowiecki、Schütze、Sinclair-Banks 与 Wegrzycki 近期的一项突破性成果(ICALP, 2023)将一元编码下 $d$ 维向量加法系统的覆盖性问题的运行时间上界改进为 $n^{2^{O(d)}}$,改进了 Rackoff 的 $n^{2^{O(d\lg d)}}$ 上界(Theor. Comput. Sci., 1978),并给出了条件匹配的下界。本文基于这一突破,重新审视 Lazi\'c 与 Schmitz 提出的后向覆盖性算法的“理想视角”(Inform. Comput., 2021)。我们证明,由 Lazi\'c 与 Schmitz 在 $d$ 维一元向量加法系统上的对偶后向覆盖性算法所导出的 $\mathbb{N}^d$ 上向下闭集受控强单调递减链,其长度同样具有紧凑的 $n^{2^{O(d)}}$ 上界,且该结论可转化为后向覆盖性算法运行时间的相同上界。此外,我们的分析在比 Lazi\'c 与 Schmitz 更一般的框架下展开,这使得我们能够得出相同的结果,并改进 Benedikt、Duff、Sharad 与 Worrell(LICS, 2017)针对可逆仿射网覆盖性问题推导出的 2EXPSPACE 上界。