LTL Parameter Synthesis of Parametric Timed Automata

D 2016

LTL Parameter Synthesis of Parametric Timed Automata

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

Basic information

Original name

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

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

Publisher

Lecture Notes in Computer Sciences in Computer Science, 9763

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Germany

Confidentiality degree

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

Publication form

printed version "print"

References:

URL

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/16:00088058

Organization unit

Faculty of Informatics

ISBN

978-3-319-41590-1

ISSN

DOI

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

UT WoS

000386263500012

Keywords in English

LTL model checking - parameter synthesis - timed automata

Abstract

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.

Links

GA15-11089S, research and development project

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

Investor: Czech Science Foundation

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

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

Investor: Masaryk University, Category A

Citovat

BEZDĚK, Peter, Nikola BENEŠ, Jiří BARNAT and 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, p. 172-187. ISBN 978-3-319-41590-1. Available from: 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 and 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, p.~172-187. ISBN~978-3-319-41590-1. Available from: https://dx.doi.org/10.1007/978-3-319-41591-8\_{}12.

Detailed Information on Publication Record