Robust model-checking of linear-time properties in timed automata. (English) Zbl 1145.68464

Bouyer, Patricia; Markey, Nicolas; Reynier, Pierre-Alain

Correa, José R. (ed.) et al., LATIN 2006: Theoretical informatics. 7th Latin American symposium, Valdivia, Chile, March 20–24, 2006. Proceedings. Berlin: Springer (ISBN 3-540-32755-X/pbk). Lecture Notes in Computer Science 3887, 238-249 (2006).

Summary: 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 Büchi-like and LTL properties. We also show how those algorithms can be adapted in order to verify bounded-response-time properties.
For the entire collection see [Zbl 1096.68003].

MSC:

68Q60	Specification and verification (program logics, model checking, etc.)
68Q45	Formal languages and automata

Keywords:

implementability; robust verification; timed systems

Software:

Uppaal