Robust model-checking of linear-time properties in timed automata

Formal verification of timed systems is well understood, but their implementation is still challenging. Raskin et al. have recently brought out a model of parameterized timed automata in which the transitions might be slightly delayed or expedited. This model is used to prove that a timed system is implementable with respect to a safety property, by proving that the parameterized model robustly satisfies the safety property. We extend here the notion of implement ability to the broader class of linear-time properties, and provide PSPACE algorithms for the robust model-checking of Buchi-like and LTL properties. We also show how those algorithms can be adapted in order to verify bounded-response-time properties.