LTL Parameter Synthesis of Parametric Timed Automata

Varování

Publikace nespadá pod Ekonomicko-správní fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.

Autoři	BEZDĚK Peter BENEŠ Nikola BARNAT Jiří ČERNÁ Ivana
Rok publikování	2016
Druh	Článek ve sborníku
Konference	Software Engineering and Formal Methods - 14th International Conference, SEFM 2016.
Fakulta / Pracoviště MU	Fakulta informatiky
Citace
www	http://dx.doi.org/10.1007/978-3-319-41591-8_12
Doi	http://dx.doi.org/10.1007/978-3-319-41591-8_12
Obor	Informatika
Klíčová slova	LTL model checking - parameter synthesis - timed automata
Popis	The parameter synthesis problem for parametric timed automata is undecidable in general even for very simple reachability properties. In this paper we introduce restrictions on parameter valua- tions under which the parameter synthesis problem is decidable for LTL properties. The investigated bounded integer parameter synthesis prob- lem could be solved using an explicit enumeration of all possible parame- ter valuations. We propose an alternative symbolic zone-based method for this problem which results in a faster computation. Our technique extends the ideas of the automata-based approach to LTL model check- ing of timed automata. To justify the usefulness of our approach, we provide experimental evaluation and compare our method with explicit enumeration technique.
Související projekty:	Získávání parametrů biologických modelů pomocí techniky ověřování modelů Rozsáhlé výpočetní systémy: modely, aplikace a verifikace V.