BEGIN:VCALENDAR
PRODID:-//Columba Systems Ltd//NONSGML CPNG/SpringViewer/ICal Output/3.3-
 M3//EN
VERSION:2.0
CALSCALE:GREGORIAN
METHOD:PUBLISH
BEGIN:VEVENT
DTSTAMP:20210219T110600Z
DTSTART:20210203T140000Z
DTEND:20210203T150000Z
SUMMARY:Atlas Talk: The Reachability Problem for Petri Nets is Not Elemen
 tary
UID:{http://www.columbasystems.com/customers/uom/gpp/eventid/}f1fr-kk5hxh
 3s-10wnew
DESCRIPTION:Join us for the next Computer Science Atlas Talk (online)\n\n
 Join here: https://zoom.us/j/93918368182\n\nSpeaker: Ranko Lazic - Unive
 rsity of Warwick\nhttps://warwick.ac.uk/fac/sci/dcs/people/ranko_lazic/\
 n\nHost: Ian Pratt-Hartmann\n\nTitle: The Reachability Problem for Petri
  Nets is Not Elementary\n \nPetri nets\, also known as vector addition s
 ystems\, are a long established model of concurrency with extensive appl
 ications in modelling and analysis of hardware\, software and database s
 ystems\, as well as chemical\, biological and business processes. The ce
 ntral algorithmic problem for Petri nets is reachability: whether from t
 he given initial con?guration there exists a sequence of valid execution
  steps that reaches the given ?nal con?guration. The complexity of the p
 roblem has remained unsettled since the 1960s\, and it is one of the mos
 t prominent open questions in the theory of veri?cation. Decidability wa
 s 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 breakthrou
 gh for several reasons. Firstly\, it shows that the reachability problem
  is much harder than the coverability (i.e.\, state reachability) proble
 m\, which is also ubiquitous but has been known to be complete for expon
 ential space since the late 1970s. Secondly\, it implies that a plethora
  of problems from formal languages\, logic\, concurrent systems\, proces
 s 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 prob
 lems for two key extensions of Petri nets: with branching and with a pus
 hdown stack.\n \nJoint work with Wojciech Czerwinski\, Slawomir Lasota\,
  Jerome Leroux and Filip Mazowiecki.\n
STATUS:TENTATIVE
TRANSP:TRANSPARENT
CLASS:PUBLIC
END:VEVENT
END:VCALENDAR