zbMATH — the first resource for mathematics

Linear parametric model checking of timed automata. (English) Zbl 0978.68094
Margaria, Tiziana (ed.) et al., Tools and algorithms for the construction and analysis of systems. 7th international conference, TACAS 2001, held as part of the joint European conferences on theory and practice of software, ETAPS 2001, Genova, Italy, April 2-6, 2001. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2031, 189-203 (2001).
Summary: We present an extension of the model checker 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).
For the entire collection see [Zbl 0960.00058].

68Q60 Specification and verification (program logics, model checking, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
HyTech; TREX
Full Text: Link