BEZDĚK, Peter, Nikola BENEŠ, Jiří BARNAT and 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, p. 28-39. ISBN 978-80-214-5022-6.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name LTL Model Checking of Parametric Timed Automata
Authors BEZDĚK, Peter (703 Slovakia, guarantor, belonging to the institution), Nikola BENEŠ (203 Czech Republic, belonging to the institution), Jiří BARNAT (203 Czech Republic, belonging to the institution) and Ivana ČERNÁ (203 Czech Republic, belonging to the institution).
Edition Brno, Czech Republic, MEMICS 2014, p. 28-39, 12 pp. 2014.
Publisher NOVPRESS
Other information
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher Czech Republic
Confidentiality degree is not subject to a state or trade secret
Publication form printed version "print"
RIV identification code RIV/00216224:14330/14:00077081
Organization unit Faculty of Informatics
ISBN 978-80-214-5022-6
Keywords in English Linear Temporal Logic; Parameter Synthesis; Parametric Timed Automata; Automata-based Model Checking
Tags International impact, Reviewed
Changed by Changed by: prof. RNDr. Ivana Černá, CSc., učo 1419. Changed: 13/10/2020 09:25.
Abstract
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.
Links
EE2.3.30.0009, research and development projectName: Zaměstnáním čerstvých absolventů doktorského studia k vědecké excelenci
MUNI/A/0855/2013, interní kód MUName: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace III. (Acronym: FI MAV III.)
Investor: Masaryk University, Category A
PrintDisplayed: 19/7/2024 01:42