13:00
14:00

[MTV] Mathieu Hilaire (U. Clermont-Ferrand) - Reachability in Two-Parametric Timed Automata with One Parameter Is EXPSPACE-Complete

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 parameter is EXPSPACE-complete. For the EXPSPACE lower bound, we make use of deep results from complexity theory, namely a serializability characterization of EXPSPACE (in turn based on Barrington’s Theorem) and a logspace translation of numbers in Chinese remainder representation to binary representation. For the EXPSPACE upper bound, we first give a careful exponential time reduction from parametric timed automata over two parametric clocks and one parameter to a (slight subclass of) parametric one-counter automata over one parameter based on a minor adjustment of a construction due to Bundala and Ouaknine.

salle 178 & https://u-bordeaux-fr.zoom.us/j/83965459705