BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//University of Liverpool Computer Science Seminar System//v2//EN
BEGIN:VEVENT
DTSTAMP:20260525T223018Z
UID:Seminar-verification-689@lxserverM.csc.liv.ac.uk
ORGANIZER:CN=Patrick Totzke:MAILTO:totzke@liverpool.ac.uk
DTSTART:20191015T110000
DTEND:20191015T120000
SUMMARY:Verification Series
DESCRIPTION:Patrick Totzke: Timed Basic Parallel Processes\n\nI will talk about two fun constructions for reachability analysis of one-clock timed automata, which lead to concise logical characterizations in existential fragment of Linear Arithmetic.\n\nThe first one describes "punctual" reachability relations: reachability in exact time t. It uses a coarse interval abstraction and counting of resets via Parikh-Automata.\n\nThe other is a "sweep line" construction to compute optimal time to reach in reachability games played on one-clock TA.\n\nTogether, these can be used to derive a (tight) NP complexity upper bound for the coverability and reachability problems in an interesting subclass of Timed Petri Nets, which naturally lends itself to parametrised safety checking of concurrent, real-time systems. This contrasts with known super-Ackermannian completeness, and undecidability results for unrestricted Timed Petri nets.\n\nThis is joint work with Lorenzo Clemente and Piotr Hofman, and was  presented at CONCUR'19.\nFull details are available at https://arxiv.org/abs/1907.01240\n\nhttps://www.csc.liv.ac.uk/research/seminars/abstract.php?id=689
LOCATION:
END:VEVENT
END:VCALENDAR