Linear Parametric Model Checking of Timed Automata

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

January 2001


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.