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:20200326T115316Z
DTSTART:20200603T130000Z
DTEND:20200603T140000Z
SUMMARY:Cancelled - Seminar: The Reachability Problem for Petri Nets is N
ot Elementary
UID:{http://www.columbasystems.com/customers/uom/gpp/eventid/}qop-k7dgwkv
z-jbmj
DESCRIPTION:Due to the University closure (Coronavirus) this talk is post
poned and we will hold it on a future date. \n\n\n\nJoin us for the next
Computer Science Atlas Talk with speaker Ranko Lazic\, University of Wa
rwick on Wednesday 3 June 2020 at 2pm in Kilburn L.T 1.5\n\nSpeaker Dr R
anko Lazic\nHost: Dr Ian Pratt-Hartmann\n\nPetri nets\, also known as ve
ctor 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 pr
ocesses. 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 comp
lexity 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 Ackerman
nian of Leroux and Schmitz from LICS 2019. We establish a non-elementary
lower bound\, i.e. that the reachability problem needs a tower of expon
entials of time and space. Until this work\, the best lower bound has be
en exponential space\, due to Lipton in 1976. The new lower bound is a m
ajor breakthrough for several reasons. Firstly\, it shows that the reach
ability problem is much harder than the coverability (i.e.\, state reach
ability) problem\, which is also ubiquitous but has been known to be com
plete for exponential space since the late 1970s. Secondly\, it implies
that a plethora of problems from formal languages\, logic\, concurrent s
ystems\, process calculi and other areas\, that are known to admit reduc
tions from the Petri nets reachability problem\, are also not elementary
. Thirdly\, it makes obsolete the currently best lower bounds for the re
achability problems for two key extensions of Petri nets: with branching
and with a pushdown stack.\n\nJoint work with Wojciech Czerwinski\, Sla
womir Lasota\, Jerome Leroux and Filip Mazowiecki.\n
STATUS:TENTATIVE
TRANSP:TRANSPARENT
CLASS:PUBLIC
LOCATION:Lecture theatre 1.5\, Kilburn Building\, Manchester
END:VEVENT
END:VCALENDAR