Petri nets, equivalently presentable as vector addition systems with states, are an established model of concurrency with widespread applications. The reachability problem, where we ask whether from a given initial configuration there exists a sequence of valid execution steps reaching a given final configuration, is the central algorithmic problem for this model. The complexity of the problem has remained, until recently, one of the hardest open questions in verification of concurrent systems. A first upper bound has been provided only in 2015 by Leroux and Schmitz, then refined by the same authors to non-primitive recursive Ackermannian upper bound in 2019. The exponential space lower bound, shown by Lipton already in 1976, remained the only known for over 40 years until a breakthrough non-elementary lower bound by Czerwi{\'n}ski, Lasota, Lazic, Leroux and Mazowiecki in 2019. Finally, a matching Ackermannian lower bound announced this year by Czerwi{\'n}ski and Orlikowski, and independently by Leroux, established the complexity of the problem. Our contribution is an improvement of the former construction, making it conceptually simpler and more direct. On the way we improve the lower bound for vector addition systems with states in fixed dimension (or, equivalently, Petri nets with fixed number of places): while Czerwi{\'n}ski and Orlikowski prove $F_k$-hardness (hardness for $k$th level in Grzegorczyk Hierarchy) in dimension $6k$, and Leroux in dimension $4k+5$, our simplified construction yields $F_k$-hardness already in dimension $3k+2$.
翻译:与各州的矢量添加系统完全相似的彼得罗网(Petrinet)是州级的矢量添加系统,是一种成熟的固定货币模式,其应用范围广泛。在最初配置中,我们询问是否存在一个有效的执行步骤序列,从而达到某个最终配置,因此,这种模式的中心算法问题。直到最近,问题的复杂性仍然是并行系统核查中最难解的问题之一。直到2015年才提供了第一个上层约束,由勒鲁和施密茨提供,然后由同一位作者改进为2019年非原始再现的阿克曼尼亚上限。利普顿(Lipton)已经于1976年展示的指数性低空间约束,在40多年后仍是唯一已知的非元素执行步骤,直到2019年Czerwi_nski、Lasota、Lazic、Lerouux和Mazowieecki。最后,由Czerfrumannial $(Czeru) 和 Orliksyalow) 已经独立地确定了问题的复杂程度。我们的贡献是,在前的固定的建筑和固定水平上,我们更简化了固定的固定的系统。