The reachability problem for Petri nets is not elementary

Autor: Ranko Lazić, Filip Mazowiecki, Jérôme Leroux, Wojciech Czerwiński, Sławomir Lasota
Přispěvatelé: University of Warsaw (UW), University of Warwick [Coventry], Laboratoire Bordelais de Recherche en Informatique (LaBRI), Université de Bordeaux (UB)-Centre National de la Recherche Scientifique (CNRS)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB), ANR-17-CE40-0028,BRAVAS,IDEAL-BASED ALGORITHMS FOR VASSES AND WELL-STRUCTURED SYSTEMS(2017), Max Planck Institute for Software Systems (MPI-SWS)
Jazyk: angličtina
Rok vydání: 2019
Předmět:
FOS: Computer and information sciences
Computer Science - Logic in Computer Science
Formal Languages and Automata Theory (cs.FL)
Computer science
Reachability problem
Concurrency
Process calculus
vector addition systems
Computer Science - Formal Languages and Automata Theory
Petri nets
0102 computer and information sciences
02 engineering and technology
01 natural sciences
Upper and lower bounds
QA76
Artificial Intelligence
Reachability
0202 electrical engineering
electronic engineering
information engineering
[INFO]Computer Science [cs]
reachability problems
Time complexity
ComputingMilieux_MISCELLANEOUS
Discrete mathematics
020207 software engineering
Petri net
Logic in Computer Science (cs.LO)
Decidability
010201 computation theory & mathematics
Hardware and Architecture
Control and Systems Engineering
Bounded function
020201 artificial intelligence & image processing
Software
Information Systems
Zdroj: Proceedings of the 51st Annual {ACM} {SIGACT} Symposium on Theory of Computing, {STOC} 2019, Phoenix, AZ, USA, June 23-26, 2019
Proceedings of the 51st Annual Symposium on Theory of Computing, 2019, Phoenix, AZ, USA, June 23-26, 2019, Jun 2019, Phoenix, United States. pp.24-33, ⟨10.1145/3313276.3316369⟩
JACM
Journal of the ACM (JACM)
Journal of the ACM (JACM), Association for Computing Machinery, 2021, 68 (1), pp.7. ⟨10.1145/3422822⟩
STOC
ISSN: 0004-5411
1557-735X
DOI: 10.1145/3313276.3316369⟩
Popis: 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.
Comment: Final version of STOC'19
Databáze: OpenAIRE
Externí odkaz: