Skip to content Skip to navigation
University of Warwick
  • Study
  • |
  • Research
  • |
  • Business
  • |
  • Alumni
  • |
  • News
  • |
  • About

University of Warwick
Publications service & WRAP

Highlight your research

  • WRAP
    • Home
    • Search WRAP
    • Browse by Warwick Author
    • Browse WRAP by Year
    • Browse WRAP by Subject
    • Browse WRAP by Department
    • Browse WRAP by Funder
    • Browse Theses by Department
  • Publications Service
    • Home
    • Search Publications Service
    • Browse by Warwick Author
    • Browse Publications service by Year
    • Browse Publications service by Subject
    • Browse Publications service by Department
    • Browse Publications service by Funder
  • Help & Advice
University of Warwick

The Library

  • Login
  • Admin

The reachability problem for Petri nets is not elementary

Tools
- Tools
+ Tools

Czerwiński, Wojciech, Lasota, Sławomir, Lazic, Ranko, Leroux, Jerome and Mazowiecki, Filip (2019) The reachability problem for Petri nets is not elementary. In: STOC 2019, Phoenix, AZ, USA, 23-26 Jun 2019. Published in: Proceedings of the 51st Annual ACM SIGACT Symposium on Theory of Computing pp. 24-33. ISBN 9781450367059. doi:10.1145/3313276.3316369

[img]
Preview
PDF
WRAP-reachability-problem-Petri-nets-not-elementary-Lazic-2019.pdf - Accepted Version - Requires a PDF viewer.

Download (1153Kb) | Preview
Official URL: http://dx.doi.org/10.1145/3313276.3316369

Request Changes to record.

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.

Item Type: Conference Item (Paper)
Subjects: Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software
Divisions: Faculty of Science > Computer Science
Library of Congress Subject Headings (LCSH): Petri nets, Computable functions
Series Name: STOC: ACM Symposium on Theory of Computing
Journal or Publication Title: Proceedings of the 51st Annual ACM SIGACT Symposium on Theory of Computing
Publisher: ACM
ISBN: 9781450367059
Book Title: Proceedings of the 51st Annual ACM SIGACT Symposium on Theory of Computing - STOC 2019
Official Date: 20 June 2019
Dates:
DateEvent
20 June 2019Available
10 April 2019Accepted
Page Range: pp. 24-33
DOI: 10.1145/3313276.3316369
Status: Peer Reviewed
Publication Status: Published
Publisher Statement: © Owner/Author | ACM 2019. This is the author's version of the work. It is posted here for your personal use. Not for redistribution. The definitive Version of Record was published in Proceedings of the 51st Annual ACM SIGACT Symposium on Theory of Computing, http://dx.doi.org/10.1145/3313276.3316369.
Access rights to Published version: Restricted or Subscription Access
RIOXX Funder/Project Grant:
Project/Grant IDRIOXX Funder NameFunder ID
683080H2020 European Research Councilhttp://dx.doi.org/10.13039/100010663
2016/21/D/ST6/01376Narodowe Centrum Naukihttp://dx.doi.org/10.13039/501100004281
2017/27/B/ST6/0209Narodowe Centrum Naukihttp://dx.doi.org/10.13039/501100004281
ANR-10-IDEX-03-02[ANR] Agence Nationale de la Recherchehttp://dx.doi.org/10.13039/501100001665
ANR-17-CE40-0028[ANR] Agence Nationale de la Recherchehttp://dx.doi.org/10.13039/501100001665
RF-2017-579Leverhulme Trusthttp://dx.doi.org/10.13039/501100000275
Conference Paper Type: Paper
Title of Event: STOC 2019
Type of Event: Conference
Location of Event: Phoenix, AZ, USA
Date(s) of Event: 23-26 Jun 2019

Request changes or add full text files to a record

Repository staff actions (login required)

View Item View Item

Downloads

Downloads per month over past year

View more statistics

twitter

Email us: wrap@warwick.ac.uk
Contact Details
About Us