LTL Parameter Synthesis of Parametric Timed Automata

D 2016

LTL Parameter Synthesis of Parametric Timed Automata

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

Základní údaje

Originální název

LTL Parameter Synthesis 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í

Berlin, Software Engineering and Formal Methods - 14th International Conference, SEFM 2016. od s. 172-187, 16 s. 2016

Nakladatel

Lecture Notes in Computer Sciences in Computer Science, 9763

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

Utajení

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

Forma vydání

tištěná verze "print"

Odkazy

URL

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/16:00088058

Organizační jednotka

Fakulta informatiky

ISBN

978-3-319-41590-1

ISSN

DOI

http://dx.doi.org/10.1007/978-3-319-41591-8_12

UT WoS

000386263500012

Klíčová slova anglicky

LTL model checking - parameter synthesis - timed automata

Štítky

core_B, firank_B

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 13. 5. 2020 19:19, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

The parameter synthesis problem for parametric timed automata is undecidable in general even for very simple reachability properties. In this paper we introduce restrictions on parameter valua- tions under which the parameter synthesis problem is decidable for LTL properties. The investigated bounded integer parameter synthesis prob- lem could be solved using an explicit enumeration of all possible parame- ter valuations. We propose an alternative symbolic zone-based method for this problem which results in a faster computation. Our technique extends the ideas of the automata-based approach to LTL model check- ing of timed automata. To justify the usefulness of our approach, we provide experimental evaluation and compare our method with explicit enumeration technique.

Návaznosti

GA15-11089S, projekt VaV

Název: Získávání parametrů biologických modelů pomocí techniky ověřování modelů

Investor: Grantová agentura ČR, Získávání parametrů biologických modelů pomocí techniky ověřování modelů

MUNI/A/0945/2015, interní kód MU

Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace V.

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

Citovat

BEZDĚK, Peter, Nikola BENEŠ, Jiří BARNAT a Ivana ČERNÁ. LTL Parameter Synthesis of Parametric Timed Automata. In Rocco De Nicola, Eva K{\"{u}}hn. Software Engineering and Formal Methods - 14th International Conference, SEFM 2016. Berlin: Lecture Notes in Computer Sciences in Computer Science, 9763, 2016, s. 172-187. ISBN 978-3-319-41590-1. Dostupné z: https://dx.doi.org/10.1007/978-3-319-41591-8_12.

@inproceedings{1350763,
   author = {Bezděk, Peter and Beneš, Nikola and Barnat, Jiří and Černá, Ivana},
   address = {Berlin},
   booktitle = {Software Engineering and Formal Methods - 14th International Conference, SEFM 2016.},
   doi = {http://dx.doi.org/10.1007/978-3-319-41591-8_12},
   editor = {Rocco De Nicola, Eva K{\"{u}}hn},
   keywords = {LTL model checking - parameter synthesis - timed automata},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Berlin},
   isbn = {978-3-319-41590-1},
   pages = {172-187},
   publisher = {Lecture Notes in Computer Sciences in Computer Science, 9763},
   title = {LTL Parameter Synthesis of Parametric Timed Automata},
   url = {http://dx.doi.org/10.1007/978-3-319-41591-8_12},
   year = {2016}
}

TY  - JOUR
ID  - 1350763
AU  - Bezděk, Peter - Beneš, Nikola - Barnat, Jiří - Černá, Ivana
PY  - 2016
TI  - LTL Parameter Synthesis of Parametric Timed Automata
PB  - Lecture Notes in Computer Sciences in Computer Science, 9763
CY  - Berlin
SN  - 9783319415901
KW  - LTL model checking - parameter synthesis - timed automata
UR  - http://dx.doi.org/10.1007/978-3-319-41591-8_12
L2  - http://dx.doi.org/10.1007/978-3-319-41591-8_12
N2  - The parameter synthesis problem for parametric timed automata is undecidable in general even for very simple reachability properties. In this paper we introduce restrictions on parameter valua- tions under which the parameter synthesis problem is decidable for LTL properties. The investigated bounded integer parameter synthesis prob- lem could be solved using an explicit enumeration of all possible parame- ter valuations. We propose an alternative symbolic zone-based method for this problem which results in a faster computation. Our technique extends the ideas of the automata-based approach to LTL model check- ing of timed automata. To justify the usefulness of our approach, we provide experimental evaluation and compare our method with explicit enumeration technique.
ER  -

BEZDĚK, Peter, Nikola BENEŠ, Jiří BARNAT a Ivana ČERNÁ. LTL Parameter Synthesis of Parametric Timed Automata. In Rocco De Nicola, Eva K$\{\backslash$''$\{$u$\}\}$hn. \textit{Software Engineering and Formal Methods - 14th International Conference, SEFM 2016.}. Berlin: Lecture Notes in Computer Sciences in Computer Science, 9763, 2016, s.~172-187. ISBN~978-3-319-41590-1. Dostupné z: https://dx.doi.org/10.1007/978-3-319-41591-8\_{}12.

Podrobný výpis o publikaci