LTL Model Checking of Parametric Timed Automata

Warning

This publication doesn't include Faculty of Sports Studies. It includes Faculty of Informatics. Official publication website can be found on muni.cz.

Authors	BEZDĚK Peter BENEŠ Nikola BARNAT Jiří ČERNÁ Ivana
Year of publication	2014
Type	Article in Proceedings
Conference	MEMICS 2014
MU Faculty or unit	Faculty of Informatics
Citation
Field	Informatics
Keywords	Linear Temporal Logic; Parameter Synthesis; Parametric Timed Automata; Automata-based Model Checking
Description	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.
Related projects:	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.