Different flavours of robustness in timed systems

Timed automata [AD94] form a recognized mathematical formalism for modelling real-time systems, for which a precise semantics is given. Over the decades, efficient verification algorithms and tools have been developed, such as Uppaal or TChecker. It quickly was apparent that timed automata are an idealized model, often inducing unrealistic behaviours: the clock values have arbitrary precision, and events are instantaneous.

To mitigate such unrealistic behaviours, which typically encompass imprecisions in time measurements, notions of robustness must be integrated into timed systems. Under such notions, an execution should resist small delay perturbations. For instance, the duration of an optimal path to a success state should not be strongly impacted by reasonable variations in time measurements.

Several notions of robustness for timed automata have been proposed in the literature. The almost-asap semantics relaxes clock constraints, which are the core reason for idealized behaviours [WDR05]. Topology can also come to the rescue to define robustness based on a metric on sets of executions [GHJ97]. Adversarial perturbations on delays can be introduced to express robustness against a worst-case scenario [BMS15]. Finally, randomization of delays is natural to model unpredictable variations: it can either consist in random perturbations within some chosen interval [ORS14, MPR21] or fully random delays [BBB+14].

Up to our knowledge, these formalisms have been considered mostly independently in the literature, and each has been analyzed with ad hoc techniques. For instance topological games were used to solve the almost-sure model checking of a class of stochastic timed automata [BBB+14], parameterized data structures were developed to represent sets of valuations in timed automata under adversarial perturbations [BMS15], and the algebraic notion of orbit graphs was key to analyzing timed systems under probabilistic perturbations [ORS14].

In this PhD, we propose to explore the relationships between these robustness notions. We will examine how the models and hypotheses differ in order to compare various notions of robustness. More importantly, our objective is to investigate whether techniques can be lifted from one notion to the other, aiming at solving open optimization problems for robust models of timed automata.

A promising first step is to adapt the notion of orbit graphs and their use in analyzing probabilistic variants of robust timed systems [ORS14] in order to come up with a characterization of almost-sure reachability in general stochastic timed automata. This would answer an intriguing open problem: the decidability status of the almost-sure model checking of stochastic timed automata.