BENEŠ, Nikola, Peter BEZDĚK, Kim G. LARSEN a Jiří SRBA. Language Emptiness of Continuous-Time Parametric Timed Automata. In Magnús M. Halldórsson, Kazuo Iwama, Naoki Kobayashi, Bettina Speckmann. Automata, Languages, and Programming. Neuveden: Springer Berlin Heidelberg, 2015, s. 69-81. ISBN 978-3-662-47665-9. Dostupné z: https://dx.doi.org/10.1007/978-3-662-47666-6_6.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Language Emptiness of Continuous-Time Parametric Timed Automata
Autoři BENEŠ, Nikola (203 Česká republika, garant, domácí), Peter BEZDĚK (703 Slovensko, domácí), Kim G. LARSEN (208 Dánsko) a Jiří SRBA (203 Česká republika).
Vydání Neuveden, Automata, Languages, and Programming, od s. 69-81, 13 s. 2015.
Nakladatel Springer Berlin Heidelberg
Další údaje
Originální 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"
Impakt faktor Impact factor: 0.402 v roce 2005
Kód RIV RIV/00216224:14330/15:00081178
Organizační jednotka Fakulta informatiky
ISBN 978-3-662-47665-9
ISSN 0302-9743
Doi http://dx.doi.org/10.1007/978-3-662-47666-6_6
UT WoS 000364317900006
Klíčová slova anglicky Parametric Timed Automata; Decidability; Language Emptiness
Štítky core_A, firank_A
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: Prof. Jiří Srba, Ph.D., učo 2841. Změněno: 30. 3. 2017 22:44.
Anotace
Parametric timed automata extend the standard timed automata with the possibility to use parameters in the clock guards. In general, if the parameters are real-valued, the problem of language emptiness of such automata is undecidable even for various restricted subclasses. We thus focus on the case where parameters are assumed to be integer-valued, while the time still remains continuous. On the one hand, we show that the problem remains undecidable for parametric timed automata with three clocks and one parameter. On the other hand, for the case with arbitrary many clocks where only one of these clocks is compared with (an arbitrary number of) parameters, we show that the parametric language emptiness is decidable. The undecidability result tightens the bounds of a previous result which assumed six parameters, while the decidability result extends the existing approaches that deal with discrete-time semantics only. To the best of our knowledge, this is the first positive result in the case of continuous-time and unbounded integer parameters, except for the rather simple case of single-clock automata.
Návaznosti
GA15-08772S, projekt VaVNázev: Analýza korektnosti vícevláknových programů v C a C++
Investor: Grantová agentura ČR, Correctness Analysis of C and C++ Programs with Threads
GA15-11089S, projekt VaVNá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/1159/2014, interní kód MUNázev: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace IV.
Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace IV., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
MUNI/A/1206/2014, interní kód MUNázev: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Akronym: SKOMU)
Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
VytisknoutZobrazeno: 13. 5. 2024 08:31