LTL Model Checking of Parametric Timed Automata

Investor logo

Warning

This publication doesn't include Faculty of Arts. 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:

You are running an old browser version. We recommend updating your browser to its latest version.