LTL Parameter Synthesis of Parametric Timed Automata

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F16%3A00088058" target="_blank" >RIV/00216224:14330/16:00088058 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1007/978-3-319-41591-8_12" target="_blank" >http://dx.doi.org/10.1007/978-3-319-41591-8_12</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-319-41591-8_12" target="_blank" >10.1007/978-3-319-41591-8_12</a>

Jazyk výsledku

angličtina

Název v původním jazyce

LTL Parameter Synthesis of Parametric Timed Automata

Popis výsledku v původním jazyce

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ázev v anglickém jazyce

LTL Parameter Synthesis of Parametric Timed Automata

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

<a href="/cs/project/GA15-11089S" target="_blank" >GA15-11089S: Získávání parametrů biologických modelů pomocí techniky ověřování modelů</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2016

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Software Engineering and Formal Methods - 14th International Conference, SEFM 2016.

ISBN

9783319415901

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

16

Strana od-do

172-187

Název nakladatele

Lecture Notes in Computer Sciences in Computer Science, 9763

Místo vydání

Berlin

Místo konání akce

Vienna

Datum konání akce

4. 7. 2016

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—