| Identifikační kód | RIV/00216224:14330/14:00077081 |
|---|
| Název v anglickém jazyce | LTL Model Checking of Parametric Timed Automata |
|---|
| Druh | D - Článek ve sborníku |
|---|
| Jazyk | eng - angličtina |
|---|
| Obor - skupina | I - Informatika |
|---|
| Obor | IN - Informatika |
|---|
| Rok uplatnění | 2014 |
|---|
| Kód důvěrnosti údajů | S - Úplné a pravdivé údaje o výsledku nepodléhající ochraně podle zvláštních právních předpisů. |
|---|
| Počet výskytů výsledku | 1 |
|---|
| Počet tvůrců celkem | 4 |
|---|
| Počet domácích tvůrců | 4 |
|---|
| Výčet všech uvedených jednotlivých tvůrců | Peter Bezděk (státní příslušnost: SK - Slovenská republika, domácí tvůrce: A, vedidk: 4376447)
Nikola Beneš (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 2050587)
Jiří Barnat (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 5692792)
Ivana Černá (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 2361132) |
|---|
| Popis výsledku v anglickém jazyce | 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. |
|---|
| Klíčová slova oddělená středníkem | Linear Temporal Logic; Parameter Synthesis; Parametric Timed Automata; Automata-based Model Checking |
|---|
| Stránka www, na které se nachází výsledek | - |
|---|