Language Emptiness of Continuous-Time Parametric Timed Automata

D 2015

Language Emptiness of Continuous-Time Parametric Timed Automata

BENEŠ, Nikola, Peter BEZDĚK, Kim G. LARSEN and Jiří SRBA

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

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"

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

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

Abstract

V originále

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 project

Name: Analýza korektnosti vícevláknových programů v C a C++

Investor: Czech Science Foundation

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/1159/2014, interní kód MU

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

Investor: Masaryk University, Category A

MUNI/A/1206/2014, interní kód MU

Name: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Acronym: SKOMU)

Investor: Masaryk University, Category A

Citovat

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.

@inproceedings{1316355,
   author = {Beneš, Nikola and Bezděk, Peter and Larsen, Kim G. and Srba, Jiří},
   address = {Neuveden},
   booktitle = {Automata, Languages, and Programming},
   doi = {http://dx.doi.org/10.1007/978-3-662-47666-6_6},
   editor = {Magnús M. Halldórsson, Kazuo Iwama, Naoki Kobayashi, Bettina Speckmann},
   keywords = {Parametric Timed Automata; Decidability; Language Emptiness},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Neuveden},
   isbn = {978-3-662-47665-9},
   pages = {69-81},
   publisher = {Springer Berlin Heidelberg},
   title = {Language Emptiness of Continuous-Time Parametric Timed Automata},
   year = {2015}
}

TY  - JOUR
ID  - 1316355
AU  - Beneš, Nikola - Bezděk, Peter - Larsen, Kim G. - Srba, Jiří
PY  - 2015
TI  - Language Emptiness of Continuous-Time Parametric Timed Automata
PB  - Springer Berlin Heidelberg
CY  - Neuveden
SN  - 9783662476659
KW  - Parametric Timed Automata
KW  - Decidability
KW  - Language Emptiness
N2  - 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.
ER  -

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. \textit{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.

Detailed Information on Publication Record