BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//labri.fr//NONSGML kigkonsult.se iCalcreator 2.41.92//
CALSCALE:GREGORIAN
METHOD:PUBLISH
UID:ac4674ad-fb47-4496-a841-92ba469ac6f6
X-WR-CALNAME:[MTV] Mathieu Hilaire (U. Clermont-Ferrand) - Reachability in 
 Two-Parametric Timed Automata with One Parameter Is EXPSPACE-Complete
X-WR-TIMEZONE:Europe/Paris
BEGIN:VTIMEZONE
TZID:Europe/Paris
TZUNTIL:20251026T010000Z
BEGIN:STANDARD
TZNAME:CET
DTSTART:20231029T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
RDATE:20241027T030000
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20230326T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
RDATE:20240331T020000
RDATE:20250330T020000
END:DAYLIGHT
END:VTIMEZONE
BEGIN:VEVENT
UID:ac4674ad-fb47-4496-a841-92ba469ac6f6
DTSTAMP:20260920T175422Z
CLASS:PUBLIC
DESCRIPTION:Parametric timed automata are an extension of timed automata in
  which clocks can be compared against parameters. The reachability problem
  asks for the existence of an assignment of the parameters to the naturals
  such that reachability holds in the underlying timed automaton. We prove 
 that the reachability problem for two-parametric timed automata with one p
 arameter is EXPSPACE-complete. For the EXPSPACE lower bound\,  we make use
  of deep results from complexity theory\, namely a serializability charact
 erization of EXPSPACE (in turn based on Barrington’s Theorem) and a logspa
 ce translation of numbers in Chinese remainder representation to binary re
 presentation. For the EXPSPACE upper bound\, we first give a careful expon
 ential time reduction from parametric timed automata over two parametric c
 locks and one parameter to a (slight subclass of) parametric one-counter a
 utomata over one parameter based on a minor adjustment of a construction d
 ue to Bundala and Ouaknine.
DTSTART;TZID=Europe/Paris:20240321T130000
DTEND;TZID=Europe/Paris:20240321T140000
LOCATION:salle 178 & https://u-bordeaux-fr.zoom.us/j/83965459705
SEQUENCE:0
SUMMARY:[MTV] Mathieu Hilaire (U. Clermont-Ferrand) - Reachability in Two-P
 arametric Timed Automata with One Parameter Is EXPSPACE-Complete
TRANSP:OPAQUE
END:VEVENT
END:VCALENDAR
