Linear Parametric Model Checking of Timed Automata

Thomas S. Hune
Judi Romijn
Mariëlle Stoelinga
Frits W. Vaandrager

January 2001

Abstract:

We present an extension of the model checker UPPAAL capable of synthesize linear parameter constraints for the correctness of parametric timed automata. The symbolic representation of the (parametric) state-space is shown to be correct. A second contribution of this paper is the identification of a subclass of parametric timed automata (L/U automata), for which the emptiness problem is decidable, contrary to the full class where it is know to be undecidable. Also we present a number of lemmas enabling the verification effort to be reduced for L/U automata in some cases. We illustrate our approach by deriving linear parameter constraints for a number of well-known case studies from the literature (exhibiting a flaw in a published paper)

Available as PostScript, PDF.

 

Last modified: 2003-06-08 by webmaster.