Language Emptiness of Continuous-Time Parametric Timed Automata

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.

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

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

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

---

Anotace

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.

---

Návaznosti

GA15-08772S, projekt VaV	Ná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 VaV	Ná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 MU	Ná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 MU	Ná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