The reachability problem for Petri nets is not elementary

DOI10.1145/3313276.3316369MaRDI QIDQ5212744zbMATH OpenOpenAlexFDO

Authors Wojciech Czerwiński, Sławomir Lasota, Ranko Lazić, Jérôme Leroux, Filip Mazowiecki

Publication date 30 January 2020

Published in Proceedings of the 51st Annual ACM SIGACT Symposium on Theory of Computing (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1809.07115, http://wrap.warwick.ac.uk/120117/1/WRAP-reachability-problem-Petri-nets-not-elementary-Lazic-2019.pdf

zbMATH Keywords

Petri netsreachability problemsvector addition systems

Mathematics Subject Classification ID

Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Analysis of algorithms and problem complexity (68Q25) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: Petri nets, also known as vector addition systems, are a long established model of concurrency with extensive applications in modelling 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 the currently best published upper bound is non-primitive recursive Ackermannian of Leroux and Schmitz from LICS 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, that are known to admit reductions from the Petri nets reachability problem, are also not elementary. Thirdly, it makes obsolete the currently best lower bounds for the reachability problems for two key extensions of Petri nets: with branching and with a pushdown stack.

Recommendations

• The Reachability Problem for Petri Nets Is Not Elementary
• An Algorithm for the General Petri Net Reachability Problem
• Decidability of the Petri net reachability problem
• SOME COMPLEXITY RESULTS FOR RINGS OF PETRI NETS
• What makes Petri nets harder to verify: stack or data?

Cited in

(41)

• Reachability in live and safe free-choice Petri nets is NP-complete
• What makes Petri nets harder to verify: stack or data?
• The complexity of verifying population protocols
• Flat Petri nets (invited talk)
• Finding cut-offs in leaderless rendez-vous protocols is easy
• Leafy automata for higher-order concurrency
• Directed reachability for infinite-state systems
• Strategic reasoning with a bounded number of resources: the quest for tractability
• Structural liveness of Petri nets is \textsc{ExpSpace}-hard and decidable
• A lower bound for the coverability problem in acyclic pushdown VAS
• Recent advances on reachability problems for valence systems (invited talk)
• An upper bound for the reachability problem of safe, elementary hornets
• Deciding fast termination for probabilistic VASS with nondeterminism
• Coverability, termination, and finiteness in recursive Petri nets
• The Reachability Problem for Petri Nets Is Not Elementary
• On Affine Reachability Problems
• Multi-Dimensional Long-Run Average Problems for Vector Addition Systems with States
• scientific article; zbMATH DE number 7559493 (Why is no real title available?)
• scientific article; zbMATH DE number 7559494 (Why is no real title available?)
• scientific article; zbMATH DE number 7559502 (Why is no real title available?)
• scientific article; zbMATH DE number 7559504 (Why is no real title available?)
• Non axiomatisability of positive relation algebras with constants, via graph homomorphisms
• PSPACE-completeness of the soundness problem of safe asymmetric-choice workflow nets
• Open Petri nets
• Acceleration for Petri nets
• On functions weakly computable by pushdown Petri nets and related systems
• Long-Run Average Behavior of Vector Addition Systems with States
• Continuous One-counter Automata
• A Note on C² Interpreted over Finite Data-Words
• Set augmented finite automata over infinite alphabets
• Coverability in 2-VASS with one unary counter is in NP
• Separators in continuous Petri nets
• Property directed reachability for generalized Petri nets
• Lower bounds for the reachability problem in fixed dimensional VASSes
• Flattability of priority vector addition systems
• New lower bounds for reachability in vector addition systems
• Asymptotic complexity estimates for probabilistic programs and their VASS abstractions
• Geometry of reachability sets of vector addition systems
• Improved lower bounds for reachability in vector addition systems
• Reachability in symmetric VASS
• Algorithmic randomness in continuous-time Markov chains

This page was built for publication: The reachability problem for Petri nets is not elementary

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5212744)