License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.STACS.2022.46
URN: urn:nbn:de:0030-drops-158561
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/15856/
Go to the corresponding LIPIcs Volume Portal

Lasota, Sławomir

Improved Ackermannian Lower Bound for the Petri Nets Reachability Problem

pdf-format:
LIPIcs-STACS-2022-46.pdf (0.8 MB)

Abstract

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ński, Lasota, Lazic, Leroux and Mazowiecki in 2019. Finally, a matching Ackermannian lower bound announced this year by Czerwiń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ński and Orlikowski prove F_k-hardness (hardness for kth level in Grzegorczyk Hierarchy) in dimension 6k, our simplified construction yields F_k-hardness already in dimension 3k+2.

BibTeX - Entry

@InProceedings{lasota:LIPIcs.STACS.2022.46,
  author =	{Lasota, S{\l}awomir},
  title =	{{Improved Ackermannian Lower Bound for the Petri Nets Reachability Problem}},
  booktitle =	{39th International Symposium on Theoretical Aspects of Computer Science (STACS 2022)},
  pages =	{46:1--46:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-222-8},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{219},
  editor =	{Berenbrink, Petra and Monmege, Benjamin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/15856},
  URN =		{urn:nbn:de:0030-drops-158561},
  doi =		{10.4230/LIPIcs.STACS.2022.46},
  annote =	{Keywords: Petri nets, reachability problem, vector addition systems}
}

Keywords: Petri nets, reachability problem, vector addition systems
Collection: 39th International Symposium on Theoretical Aspects of Computer Science (STACS 2022)
Issue Date: 2022
Date of publication: 09.03.2022

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI