BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//labri.fr//NONSGML kigkonsult.se iCalcreator 2.41.92//
CALSCALE:GREGORIAN
METHOD:PUBLISH
UID:b409d580-bbc6-45b6-a6e2-427d5a597111
X-WR-CALNAME:[MTV] Mathieu Hilaire (LaBRI) - Serializability in Parametric 
 Timed Automata\, Resilience and Home-Space for WSTS
X-WR-TIMEZONE:Europe/Paris
BEGIN:VTIMEZONE
TZID:Europe/Paris
TZUNTIL:20270328T010000Z
BEGIN:STANDARD
TZNAME:CET
DTSTART:20241027T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
RDATE:20251026T030000
RDATE:20261025T030000
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20250330T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
RDATE:20260329T020000
END:DAYLIGHT
END:VTIMEZONE
BEGIN:VEVENT
UID:b409d580-bbc6-45b6-a6e2-427d5a597111
DTSTAMP:20260426T083153Z
CLASS:PUBLIC
DESCRIPTION:In the first half of the talk\, I will talk about the EXPSPACE 
 lower bound for PTA reachability developed during my phd thesis.\n\nParame
 tric timed automata (PTA) have been introduced by Alur\, Henzinger\, and V
 ardi as an\nextension of timed automata in which clocks can be compared ag
 ainst parameters. The reachability problem asks for the existence of an as
 signment of the parameters to the non-negative integers such that reachabi
 lity holds in the underlying timed automaton. The reachability problem for
  PTA is long known to be undecidable\, already over three parametric clock
 s.\nA few years ago\, Bundala and Ouaknine proved that for PTA over two pa
 rametric clocks and one\nparameter the reachability problem is decidable a
 nd also showed a lower bound for the complexity class PSPACE^NEXP. Our mai
 n result is that the reachability problem for parametric timed automata ov
 er two parametric clocks and one parameter is EXPSPACE-complete.\nFor the 
 EXPSPACE lower bound we make use of deep results from complexity theory\, 
 namely\na serializability characterization of EXPSPACE (in turn based on B
 arrington’s Theorem) and a\nlogspace translation of numbers in Chinese Rem
 ainder Representation to binary representation due to Chiu\, Davida\, and 
 Litow. It is shown that with small PTA over two parametric clocks and one 
 parameter one can simulate serializability computations. The EXPSPACE uppe
 r bound proof and its technical details will not be discussed in this talk
 .\n\nThen\, I will talk about the more general problem of resilience.\nRes
 ilience of unperfect systems is a key property for improving safety by ins
 uring that if a system could go into a bad state in Bad then it can also l
 eave this bad state and reach a safe state in Safe. We consider six types 
 of resilience (one of them being equivalent to the home-space property) de
 fined by an upward-closed set or a downward-closed set Safe\, and by the e
 xistence of a bound on the length of minimal runs starting from a set Bad 
 and reaching Safe (where Bad is generally the complementary of Safe).\nWe 
 first show that all resilience problems are undecidable for effective Well
  Structured Transition Systems (WSTS) with strong compatibility. We then s
 how that resilience is decidable for Well Behaved Transition Systems (WBTS
 ) and for WSTS with adapted effectiveness hypotheses. Most of the resilien
 ce properties are shown decidable for other classes like WSTS with the dow
 nward compatibility\, VASS\, lossy counter machines\, reset-VASS\, integer
  VASS and continuous VASS.\n\n\nImport automatique depuis https://framagen
 da.org/remote.php/dav/public-calendars/D3yqF7nwys9amfyY?export par sync_ic
 als_to_drupal.py pour M2F
DTSTART;TZID=Europe/Paris:20250515T130000
DTEND;TZID=Europe/Paris:20250515T140000
LOCATION:LaBRI 178
SEQUENCE:0
SUMMARY:[MTV] Mathieu Hilaire (LaBRI) - Serializability in Parametric Timed
  Automata\, Resilience and Home-Space for WSTS
TRANSP:OPAQUE
END:VEVENT
END:VCALENDAR
