On Clock-Aware LTL Properties of Timed Automata

D 2014

On Clock-Aware LTL Properties of Timed Automata

BEZDĚK, Peter, Nikola BENEŠ, Vojtěch HAVEL, Jiří BARNAT, Ivana ČERNÁ et. al.

Základní údaje

Originální název

On Clock-Aware LTL Properties of Timed Automata

Autoři

BEZDĚK, Peter (703 Slovensko, domácí), Nikola BENEŠ (203 Česká republika, garant, domácí), Vojtěch HAVEL (203 Česká republika, domácí), Jiří BARNAT (203 Česká republika, domácí) a Ivana ČERNÁ (203 Česká republika, domácí)

Vydání

Neuveden, Theoretical Aspects of Computing – ICTAC 2014, od s. 43-60, 18 s. 2014

Nakladatel

Springer International Publishing

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Švýcarsko

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/14:00076564

Organizační jednotka

Fakulta informatiky

ISBN

978-3-319-10881-0

ISSN

DOI

http://dx.doi.org/10.1007/978-3-319-10882-7_4

Klíčová slova anglicky

Linear Temporal Logic; Timed Automata; Automata-based Model Checking

Štítky

core_B, firank_B

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 13. 10. 2020 09:25, prof. RNDr. Ivana Černá, CSc.

Anotace

V originále

We introduce the Clock-Aware Linear Temporal Logic (CA-LTL) for expressing linear time properties of timed automata, and show how to apply the standard automata-based approach of Vardi and Wolper to check for the validity of a CA-LTL formula over the continuous-time semantics of a timed automaton. Our model checking procedure employs zone-based abstraction and a new concept of the so called ultraregions. We also show that the Timed Büchi Automaton Emptiness problem is not the problem that the intended automata-based approach to CA-LTL model checking is reduced to. Finally, we give the necessary proofs of correctness, some hints for an efficient implementation, and preliminary experimental evaluation of our technique.

Návaznosti

EE2.3.30.0009, projekt VaV

Název: Zaměstnáním čerstvých absolventů doktorského studia k vědecké excelenci

LH11065, projekt VaV

Název: Řízení a ověřování vlastností komplexních hybridních systémů (Akronym: Řízení a ověřování vlastností komplexních hybridní)

Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Řízení a ověřování vlastností komplexních hybridních systémů

MUNI/A/0855/2013, interní kód MU

Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace III. (Akronym: FI MAV III.)

Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace III., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

Citovat

BEZDĚK, Peter, Nikola BENEŠ, Vojtěch HAVEL, Jiří BARNAT a Ivana ČERNÁ. On Clock-Aware LTL Properties of Timed Automata. In Gabriel Ciobanu, Dominique Méry. Theoretical Aspects of Computing – ICTAC 2014. Neuveden: Springer International Publishing, 2014, s. 43-60. ISBN 978-3-319-10881-0. Dostupné z: https://dx.doi.org/10.1007/978-3-319-10882-7_4.

@inproceedings{1199016,
   author = {Bezděk, Peter and Beneš, Nikola and Havel, Vojtěch and Barnat, Jiří and Černá, Ivana},
   address = {Neuveden},
   booktitle = {Theoretical Aspects of Computing – ICTAC 2014},
   doi = {http://dx.doi.org/10.1007/978-3-319-10882-7_4},
   editor = {Gabriel Ciobanu, Dominique Méry},
   keywords = {Linear Temporal Logic; Timed Automata; Automata-based Model Checking},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Neuveden},
   isbn = {978-3-319-10881-0},
   pages = {43-60},
   publisher = {Springer International Publishing},
   title = {On Clock-Aware LTL Properties of Timed Automata},
   year = {2014}
}

TY  - JOUR
ID  - 1199016
AU  - Bezděk, Peter - Beneš, Nikola - Havel, Vojtěch - Barnat, Jiří - Černá, Ivana
PY  - 2014
TI  - On Clock-Aware LTL Properties of Timed Automata
PB  - Springer International Publishing
CY  - Neuveden
SN  - 9783319108810
KW  - Linear Temporal Logic
KW  - Timed Automata
KW  - Automata-based Model Checking
N2  - We introduce the Clock-Aware Linear Temporal Logic (CA-LTL) for expressing linear time properties of timed automata, and show how to apply the standard automata-based approach of Vardi and Wolper to check for the validity of a CA-LTL formula over the continuous-time semantics of a timed automaton. Our model checking procedure employs zone-based abstraction and a new concept of the so called ultraregions. We also show that the Timed Büchi Automaton Emptiness problem is not the problem that the intended automata-based approach to CA-LTL model checking is reduced to. Finally, we give the necessary proofs of correctness, some hints for an efficient implementation, and preliminary experimental evaluation of our technique.
ER  -

BEZDĚK, Peter, Nikola BENEŠ, Vojtěch HAVEL, Jiří BARNAT a Ivana ČERNÁ. On Clock-Aware LTL Properties of Timed Automata. In Gabriel Ciobanu, Dominique Méry. \textit{Theoretical Aspects of Computing – ICTAC 2014}. Neuveden: Springer International Publishing, 2014, s.~43-60. ISBN~978-3-319-10881-0. Dostupné z: https://dx.doi.org/10.1007/978-3-319-10882-7\_{}4.

Podrobný výpis o publikaci