Other formats:
BibTeX
LaTeX
RIS
@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 and 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, p.~43-60. ISBN~978-3-319-10881-0. Available from: https://dx.doi.org/10.1007/978-3-319-10882-7\_{}4.
|
