论文标题
固定尺寸向量添加系统中的可达到性
Reachability in fixed dimension vector addition systems with states
论文作者
论文摘要
可及性问题是基于与状态（VASS）的矢量添加系统进行正式验证的中心决策问题，该系统等效于Petri网，并构成了最研究和应用的并发模型之一。 VAS的可及性也可以与许多计算机科学领域的许多问题相互还原。尽管取得了最近的进步，但可及性问题的复杂性仍然尚未确定，并且与见证可达性的最短vass运行的长度密切相关。 我们考虑固定尺寸的瓦斯，并获得三个主要结果。对于前两个，我们假设输入中的整数以一单元给出，并且给定VASS的控制图是平坦的（即没有嵌套周期的）。我们在维度3中获得了一个vass家族，其最短的可及性证人的跑步是指数级的，我们表明可及性问题在维度7中。在LICS 2015和Englert等人中。在LICS 2016中，并贡献了第一个结构，该建筑将三维扁平气体与2维vass区分开。 我们的第三个结果是通过新型的整数分数产品系列，表明4维vass可能会达到指定的最短最短可达性，目击者的跑步。以前已知的最小维度是14。
The reachability problem is a central decision problem for formal verification based on vector addition systems with states (VASS), which are equivalent to Petri nets and form one of the most studied and applied models of concurrency. Reachability for VASS is also inter-reducible with a plethora of problems from a number of areas of computer science. In spite of recent progress, the complexity of the reachability problem remains unsettled, and it is closely related to the lengths of shortest VASS runs that witness reachability. We consider VASS of fixed dimension, and obtain three main results. For the first two, we assume that the integers in the input are given in unary, and that the control graph of the given VASS is flat (i.e., without nested cycles). We obtain a family of VASS in dimension 3 whose shortest reachability witnessing runs are exponential, and we show that the reachability problem is NP-hard in dimension 7. These results resolve negatively questions that had been posed by the works of Blondin et al. in LICS 2015 and Englert et al. in LICS 2016, and contribute a first construction that distinguishes 3-dimensional flat VASS from 2-dimensional VASS. Our third result, by means of a novel family of products of integer fractions, shows that 4-dimensional VASS can have doubly exponentially long shortest reachability witnessing runs. The smallest dimension for which this was previously known is 14.
