13:00
14:00

In the first half of the talk, I will talk about the EXPSPACE lower bound for PTA reachability developed during my phd thesis.

Parametric timed automata (PTA) have been introduced by Alur, Henzinger, and Vardi as 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 non-negative integers such that reachability holds in the underlying timed automaton. The reachability problem for PTA is long known to be undecidable, already over three parametric clocks.
A few years ago, Bundala and Ouaknine proved that for PTA over two parametric clocks and one
parameter the reachability problem is decidable and also showed a lower bound for the complexity class PSPACE^NEXP. Our main result is that the reachability problem for parametric timed automata over two parametric clocks and 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 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 upper bound proof and its technical details will not be discussed in this talk.

Then, I will talk about the more general problem of resilience.
Resilience of unperfect systems is a key property for improving safety by insuring that if a system could go into a bad state in Bad then it can also leave 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) defined by an upward-closed set or a downward-closed set Safe, and by the existence 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).
We first show that all resilience problems are undecidable for effective Well Structured Transition Systems (WSTS) with strong compatibility. We then show that resilience is decidable for Well Behaved Transition Systems (WBTS) and for WSTS with adapted effectiveness hypotheses. Most of the resilience properties are shown decidable for other classes like WSTS with the downward compatibility, VASS, lossy counter machines, reset-VASS, integer VASS and continuous VASS.

LaBRI 178