×

zbMATH — the first resource for mathematics

Bounded model checking for parametric timed automata. (English) Zbl 1350.68183
Jensen, Kurt (ed.) et al., Transactions on Petri Nets and Other Models of Concurrency V. Berlin: Springer (ISBN 978-3-642-29071-8/pbk). Lecture Notes in Computer Science 6900. Journal Subline, 141-159 (2012).
Summary: This paper shows how bounded model checking can be applied to parameter synthesis for parametric timed automata with continuous time. While it is known that the general problem is undecidable even for reachability, we show how to synthesize a part of the set of all the parameter valuations under which the given property holds in a model. The results form a full theory which can be easily applied to parametric verification of a wide range of temporal formulae – we present such an implementation for the existential part of CTL\(_{-\mathrm{X}}\).
For the entire collection see [Zbl 1238.68015].

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
68Q45 Formal languages and automata
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Software:
Moby/DC; Uppaal
PDF BibTeX XML Cite
Full Text: DOI