Events at The University of Manchester
  • University home
  • Events
  • Home
  • Exhibitions
  • Conferences
  • Lectures and seminars
  • Performances
  • Events for prospective students
  • Sustainability events
  • Family events
  • All Events

Atlas Talk: The Reachability Problem for Petri Nets is Not Elementary

Dates:3 February 2021
Times:14:00 - 15:00
What is it:Seminar
Organiser:Department of Computer Science
Who is it for:University staff, Adults
Speaker:Ranko Lazic
See travel and contact information
Add to your calendar

More information

  • Computer Science Atlas Talk

Other events

  • In category "Seminar"
  • In group "(CS) Computer Science seminar series"
  • By Department of Computer Science

Join us for the next Computer Science Atlas Talk (online)

Join here: https://zoom.us/j/93918368182

Speaker: Ranko Lazic - University of Warwick https://warwick.ac.uk/fac/sci/dcs/people/ranko_lazic/

Host: Ian Pratt-Hartmann

Title: The Reachability Problem for Petri Nets is Not Elementary

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 con?guration there exists a sequence of valid execution steps that reaches the given ?nal con?guration. 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 veri?cation. 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.

Joint work with Wojciech Czerwinski, Slawomir Lasota, Jerome Leroux and Filip Mazowiecki.

Speaker

Ranko Lazic

Organisation: University of Warwick

Travel and Contact Information

Find event

Contact event

Karon Mee

karon.mee@manchester.ac.uk

Contact us

  • +44 (0) 161 306 6000

Find us

The University of Manchester
Oxford Rd
Manchester
M13 9PL
UK

Connect with the University

  • Facebook page for The University of Manchester
  • X (formerly Twitter) page for The University of Manchester
  • YouTube page for The University of Manchester
  • Instagram page for The University of Manchester
  • TikTok page for The University of Manchester
  • LinkedIn page for The University of Manchester

  • Privacy /
  • Copyright notice /
  • Accessibility /
  • Freedom of information /
  • Charitable status /
  • Royal Charter Number: RC000797
  • Close menu
  • Home
    • Featured events
    • Today's events
    • The Whitworth events
    • Manchester Museum events
    • Jodrell Bank Discovery Centre events
    • Martin Harris Centre events
    • The John Rylands Library events
    • Exhibitions
    • Conferences
    • Lectures and seminars
    • Performances
    • Events for prospective students
    • Sustainability events
    • Family events
    • All events