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