Seminal results establish that the coverability problem for Vector Addition Systems with States (VASS) is in EXPSPACE (Rackoff, '78) and is EXPSPACE-hard already under unary encodings (Lipton, '76). More precisely, Rosier and Yen later utilise Rackoff's bounding technique to show that if coverability holds then there is a run of length at most $n^{2^{\mathcal{O}(d \log d)}}$, where $d$ is the dimension and $n$ is the size of the given unary VASS. Earlier, Lipton showed that there exist instances of coverability in $d$-dimensional unary VASS that are only witnessed by runs of length at least $n^{2^{\Omega(d)}}$. Our first result closes this gap. We improve the upper bound by removing the twice-exponentiated $\log(d)$ factor, thus matching Lipton's lower bound. This closes the corresponding gap for the exact space required to decide coverability. This also yields a deterministic $n^{2^{\mathcal{O}(d)}}$-time algorithm for coverability. Our second result is a matching lower bound, that there does not exist a deterministic $n^{2^{o(d)}}$-time algorithm, conditioned upon the Exponential Time Hypothesis. When analysing coverability, a standard proof technique is to consider VASS with bounded counters. Bounded VASS make for an interesting and popular model due to strong connections with timed automata. Withal, we study a natural setting where the counter bound is linear in the size of the VASS. Here the trivial exhaustive search algorithm runs in $\mathcal{O}(n^{d+1})$-time. We give evidence to this being near-optimal. We prove that in dimension one this trivial algorithm is conditionally optimal, by showing that $n^{2-o(1)}$-time is required under the $k$-cycle hypothesis. In general fixed dimension $d$, we show that $n^{d-2-o(1)}$-time is required under the 3-uniform hyperclique hypothesis.
翻译:经典结果已经证明,针对带状态向量加法系统(VASS)的覆盖问题处于EXPSPACE(Rackoff,' 78)中,甚至在一元编码下也已经是EXPSPACE-hard(Lipton,' 76)。更精确地说,Rosier和Yen后来利用Rackoff的边界技术表明,如果覆盖性成立,则存在长度不超过$n^{2^{\mathcal{O}(d \log d)}}$的运行,其中$d$是给定一元VASS的维度,$n$是其大小。此前,Lipton表明,存在$d$维一元VASS的覆盖示例,只有至少长度为$n^{2^{\Omega(d)}}$的运行才能看到。我们的第一个结果弥合了这个差距。通过消除两次指数化的$\log(d)$因子,我们改进了上界,从而与Lipton的下界相匹配。这样完成了决定覆盖性所需的确切空间的相应差距。这还产生了可确定的$n^{2^{\mathcal{O}(d)}}$时间算法以实现覆盖性。我们的第二个结果是匹配的下界,即不存在确定性$n^{2^{o(d)}}$时间算法,条件是指数时间假设成立。在分析覆盖性时,一种标准的证明技术是考虑具有有界计数器的VASS。有界VASS由于其与定时自动机的强连接而成为一种有趣和流行的模型。然而,在这里,我们研究计数器边界与VASS大小成线性的自然设置。在这里,微不足道的穷举搜索算法的运行时间为$\mathcal{O}(n^{d+1})$。我们给这个时间复杂度提供了证据。我们证明,在仅有一个维度的情况下,这个微不足道的算法在$k$-cycle假设下表现出条件最优性,因为我们证明在3-uniform hyperclique假设下,在一般的固定维数d中,需要$n^{d-2-o(1)}$-时间才能完成。