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 primary 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$, our simplified construction yields $F_k$-hardness already in dimension $3k+2$.
翻译:彼得罗网(Petrinet)与各州的矢量加增系统完全相似,是具有广泛应用性的固定货币模型。 能否到达的问题,我们从一个特定的初始配置中询问是否存在一个有效的执行步骤序列,达到某个最终配置,这是该模型的中心算法问题。 直到最近,问题的复杂性仍然是并行系统核查中最难解决的问题之一。直到2015年才提供了第一个上层约束,由Leroux和Schmitz提供,然后由同一位作者改进为2019年非原始的Ackermannian递归的高级约束。利普顿(Lipton)已经于1976年显示的指数性下限空间仍然是唯一已知的40多年,直到Czerwi_n}ski、Lasota、Lazic、Lerouux和Mazowieecki。最后,由Czermannian低层(Czerwi_n}和Orickowski)宣布,然后由Leroudoux 确定问题的复杂程度。我们的主要贡献是简化的硬度水平,而我们之前的固定的固定水平是更简单的固定的。