The Library
The reachability problem for petri nets is not elementary
Tools
Tools
Tools
Czerwinski, Wojciech, Lasota, Slawomir , Lazic, Ranko, Leroux, Jérôme and Mazowiecki, Filip (2021) The reachability problem for petri nets is not elementary. Journal of the ACM, 68 (1). 7. doi:10.1145/3422822 ISSN 0004-5411.
|
PDF
WRAP-Reachability-problem-petri-nets-is-not-elementary-Lazic-2020.pdf - Accepted Version - Requires a PDF viewer. Download (1426Kb) | Preview |
Official URL: https://doi.org/10.1145/3422822
Abstract
Petri nets, also known as vector addition systems, are a long established model of concurrency with extensive applications in modeling and analysis of hardware, software, and database systems, as well as chemical, biological, and business processes. The central algorithmic problem for Petri nets is reachability: whether from the given initial configuration there exists a sequence of valid execution steps that reaches the given final configuration. The complexity of the problem has remained unsettled since the 1960s, and it is one of the most prominent open questions in the theory of verification. Decidability was proved by Mayr in his seminal STOC 1981 work, and, currently, the best published upper bound is non-primitive recursive Ackermannian of Leroux and Schmitz from Symposium on Logic in Computer Science 2019. We establish a non-elementary lower bound, i.e., that the reachability problem needs a tower of exponentials of time and space. Until this work, the best lower bound has been exponential space, due to Lipton in 1976. The new lower bound is a major breakthrough for several reasons. Firstly, it shows that the reachability problem is much harder than the coverability (i.e., state reachability) problem, which is also ubiquitous but has been known to be complete for exponential space since the late 1970s. Secondly, it implies that a plethora of problems from formal languages, logic, concurrent systems, process calculi, and other areas, which are known to admit reductions from the Petri nets reachability problem, are also not elementary. Thirdly, it makes obsolete the current best lower bounds for the reachability problems for two key extensions of Petri nets: with branching and with a pushdown stack.
| Item Type: | Journal Article | |||||||||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Alternative Title: | ||||||||||||||||||||||
| Subjects: | Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software | |||||||||||||||||||||
| Divisions: | Faculty of Science, Engineering and Medicine > Science > Computer Science | |||||||||||||||||||||
| Library of Congress Subject Headings (LCSH): | Petri nets, Machine theory, Computational complexity | |||||||||||||||||||||
| Journal or Publication Title: | Journal of the ACM | |||||||||||||||||||||
| Publisher: | Association for Computing Machinery, Inc. | |||||||||||||||||||||
| ISSN: | 0004-5411 | |||||||||||||||||||||
| Official Date: | February 2021 | |||||||||||||||||||||
| Dates: |
|
|||||||||||||||||||||
| Volume: | 68 | |||||||||||||||||||||
| Number: | 1 | |||||||||||||||||||||
| Article Number: | 7 | |||||||||||||||||||||
| DOI: | 10.1145/3422822 | |||||||||||||||||||||
| Status: | Peer Reviewed | |||||||||||||||||||||
| Publication Status: | Published | |||||||||||||||||||||
| Reuse Statement (publisher, data, author rights): | "© ACM, 2020. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in Journal of the ACM, 68(1), Dec 2020 http://doi.acm.org/10.1145/3422822 | |||||||||||||||||||||
| Access rights to Published version: | Restricted or Subscription Access | |||||||||||||||||||||
| Date of first compliant deposit: | 12 October 2020 | |||||||||||||||||||||
| Date of first compliant Open Access: | 17 March 2021 | |||||||||||||||||||||
| RIOXX Funder/Project Grant: |
|
|||||||||||||||||||||
| Related URLs: |
Request changes or add full text files to a record
Repository staff actions (login required)
 |
View Item |
Downloads
Downloads per month over past year
