Resilience of Timed Systems

Imperfections in timed systems has often been addressed as a robustness problem asking whether a timed system preserves some properties despite imperfect time measurement. Robustness, however, considers systems as reliable if there exists even a infinitesimal amount of perturbation for which a system preserves its properties. This paper addresses correctness of timed systems in a different setting called resilience, that considers the behaviors of a system when unspecified timing errors such as missed deadlines occur. Given a fault model that allows transitions to fire later than allowed by their guard, we say that a system is universally resilient if and only if it always returns to a timed behavior of the non-faulty system. It is existentially resilient for a given fault model if and only if it can return to a timed behavior of the non-faulty system. We show that checking universal resilience of timed automata is undecidable, but existential resilience is in EXPSPACE. To obtain decidability and better complexity bounds, we consider untimed versions of the problem as well as known subclasses of timed automata.