BEZDĚK, Peter, Nikola BENEŠ, Jiří BARNAT a Ivana ČERNÁ. LTL Model Checking of Parametric Timed Automata. In Petr Hliněný, Zdeněk Dvořák, Jiří Jaroš, Jan Kofroň, Jan Kořenek, Petr Matula, Karel Pala. MEMICS 2014. Brno, Czech Republic: NOVPRESS, 2014, s. 28-39. ISBN 978-80-214-5022-6. |
Další formáty:
BibTeX
LaTeX
RIS
@inproceedings{1204495, author = {Bezděk, Peter and Beneš, Nikola and Barnat, Jiří and Černá, Ivana}, address = {Brno, Czech Republic}, booktitle = {MEMICS 2014}, editor = {Petr Hliněný, Zdeněk Dvořák, Jiří Jaroš, Jan Kofroň, Jan Kořenek, Petr Matula, Karel Pala}, keywords = {Linear Temporal Logic; Parameter Synthesis; Parametric Timed Automata; Automata-based Model Checking}, howpublished = {tištěná verze "print"}, language = {eng}, location = {Brno, Czech Republic}, isbn = {978-80-214-5022-6}, pages = {28-39}, publisher = {NOVPRESS}, title = {LTL Model Checking of Parametric Timed Automata}, year = {2014} }
TY - JOUR ID - 1204495 AU - Bezděk, Peter - Beneš, Nikola - Barnat, Jiří - Černá, Ivana PY - 2014 TI - LTL Model Checking of Parametric Timed Automata PB - NOVPRESS CY - Brno, Czech Republic SN - 9788021450226 KW - Linear Temporal Logic KW - Parameter Synthesis KW - Parametric Timed Automata KW - Automata-based Model Checking N2 - 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. ER -
BEZDĚK, Peter, Nikola BENEŠ, Jiří BARNAT a Ivana ČERNÁ. LTL Model Checking of Parametric Timed Automata. In Petr Hliněný, Zdeněk Dvořák, Jiří Jaroš, Jan Kofroň, Jan Kořenek, Petr Matula, Karel Pala. \textit{MEMICS 2014}. Brno, Czech Republic: NOVPRESS, 2014, s.~28-39. ISBN~978-80-214-5022-6.
|