Improved Ackermannian lower bound for the Petri nets reachability problem

  • 2022-01-13 18:02:07
  • SÅ‚awomir Lasota
  • 0

Abstract

Petri nets, equivalently presentable as vector addition systems with states,are an established model of concurrency with widespread applications. Thereachability problem, where we ask whether from a given initial configurationthere exists a sequence of valid execution steps reaching a given finalconfiguration, is the central algorithmic problem for this model. Thecomplexity of the problem has remained, until recently, one of the hardest openquestions in verification of concurrent systems. A first upper bound has beenprovided only in 2015 by Leroux and Schmitz, then refined by the same authorsto non-primitive recursive Ackermannian upper bound in 2019. The exponentialspace lower bound, shown by Lipton already in 1976, remained the only known forover 40 years until a breakthrough non-elementary lower bound byCzerwi{\'n}ski, Lasota, Lazic, Leroux and Mazowiecki in 2019. Finally, amatching Ackermannian lower bound announced this year by Czerwi{\'n}ski andOrlikowski, and independently by Leroux, established the complexity of theproblem. Our primary contribution is an improvement of the former construction, makingit conceptually simpler and more direct. On the way we improve the lower boundfor vector addition systems with states in fixed dimension (or, equivalently,Petri nets with fixed number of places): while Czerwi{\'n}ski and Orlikowskiprove $F_k$-hardness (hardness for $k$th level in Grzegorczyk Hierarchy) indimension $6k$, our simplified construction yields $F_k$-hardness already indimension $3k+2$.

 

Quick Read (beta)

loading the full paper ...