BENEŠ, Nikola, Peter BEZDĚK, Kim G. LARSEN and 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, p. 69-81. ISBN 978-3-662-47665-9. Available from: https://dx.doi.org/10.1007/978-3-662-47666-6_6.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name Language Emptiness of Continuous-Time Parametric Timed Automata
Authors BENEŠ, Nikola (203 Czech Republic, guarantor, belonging to the institution), Peter BEZDĚK (703 Slovakia, belonging to the institution), Kim G. LARSEN (208 Denmark) and Jiří SRBA (203 Czech Republic).
Edition Neuveden, Automata, Languages, and Programming, p. 69-81, 13 pp. 2015.
Publisher Springer Berlin Heidelberg
Other information
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher Germany
Confidentiality degree is not subject to a state or trade secret
Publication form printed version "print"
Impact factor Impact factor: 0.402 in 2005
RIV identification code RIV/00216224:14330/15:00081178
Organization unit Faculty of Informatics
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
Keywords in English Parametric Timed Automata; Decidability; Language Emptiness
Tags core_A, firank_A
Tags International impact, Reviewed
Changed by Changed by: Prof. Jiří Srba, Ph.D., učo 2841. Changed: 30/3/2017 22:44.
Abstract
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.
Links
GA15-08772S, research and development projectName: Analýza korektnosti vícevláknových programů v C a C++
Investor: Czech Science Foundation
GA15-11089S, research and development projectName: Získávání parametrů biologických modelů pomocí techniky ověřování modelů
Investor: Czech Science Foundation
MUNI/A/1159/2014, interní kód MUName: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace IV.
Investor: Masaryk University, Category A
MUNI/A/1206/2014, interní kód MUName: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Acronym: SKOMU)
Investor: Masaryk University, Category A
PrintDisplayed: 19/7/2024 01:33