LTL Model Checking of Parametric Timed Automata

D 2014

LTL Model Checking of Parametric Timed Automata

BEZDĚK, Peter, Nikola BENEŠ, Jiří BARNAT a Ivana ČERNÁ

Základní údaje

Originální název

LTL Model Checking of Parametric Timed Automata

Autoři

BEZDĚK, Peter (703 Slovensko, garant, domácí), Nikola BENEŠ (203 Česká republika, domácí), Jiří BARNAT (203 Česká republika, domácí) a Ivana ČERNÁ (203 Česká republika, domácí)

Vydání

Brno, Czech Republic, MEMICS 2014, od s. 28-39, 12 s. 2014

Nakladatel

NOVPRESS

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Česká republika

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

tištěná verze "print"

Kód RIV

RIV/00216224:14330/14:00077081

Organizační jednotka

Fakulta informatiky

ISBN

978-80-214-5022-6

Klíčová slova anglicky

Linear Temporal Logic; Parameter Synthesis; Parametric Timed Automata; Automata-based Model Checking

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 13. 10. 2020 09:25, prof. RNDr. Ivana Černá, CSc.

Anotace

V originále

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.

Návaznosti

EE2.3.30.0009, projekt VaV

Název: Zaměstnáním čerstvých absolventů doktorského studia k vědecké excelenci

MUNI/A/0855/2013, interní kód MU

Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace III. (Akronym: FI MAV III.)

Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace III., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

Citovat

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.

@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.

Podrobný výpis o publikaci