Další formáty:
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 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.
|