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

Abstract

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 implementability 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 boundedresponse-time properties. © Springer-Verlag Berlin Heidelberg 2006.