LTL Model Checking of Parametric Timed Automata

Varování

Publikace nespadá pod Filozofickou 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í	2014
Druh	Článek ve sborníku
Konference	MEMICS 2014
Fakulta / Pracoviště MU	Fakulta informatiky
Citace
Obor	Informatika
Klíčová slova	Linear Temporal Logic; Parameter Synthesis; Parametric Timed Automata; Automata-based Model Checking
Popis	The parameter synthesis problem for timed automata is undecidable in general even for very simple reachability properties. In this paper we introduce restrictions on parameter valuations under which the parameter synthesis problem is decidable for LTL properties. The proposed problem could be solved using an explicit enumeration of all possible parameter valuations. However, we introduce a symbolic zone-based method for synthesising bounded integer parameters of parametric timed automata with an LTL specification. Our method extends the ideas of the standard automata-based approach to LTL model checking of timed automata. Our solution employs constrained parametric difference bound matrices and a suitable notion of extrapolation.
Související projekty:	Zaměstnáním čerstvých absolventů doktorského studia k vědecké excelenci Rozsáhlé výpočetní systémy: modely, aplikace a verifikace III.