Open AccessLinear Parametric Model Checking of Timed Automata
Author(s) -
Thomas Hune,
Judi Romijn,
Mariëlle Stoelinga,
Frits Vaandrager
Publication year - 2001
Publication title -
brics report series
Language(s) - English
Resource type - Journals
eISSN - 1601-5355
pISSN - 0909-0878
DOI - 10.7146/brics.v8i5.20459
Subject(s) - decidability , undecidable problem , correctness , automaton , parametric statistics , model checking , discrete mathematics , computer science , state space , timed automaton , mathematics , algorithm , theoretical computer science , statistics
We present an extension of the model checker Uppaal capable of synthesizing 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).