On Clock-Aware LTL Properties of Timed Automata

Varování

Publikace nespadá pod Filozofickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.

Autoři	BEZDĚK Peter BENEŠ Nikola HAVEL Vojtěch BARNAT Jiří ČERNÁ Ivana
Rok publikování	2014
Druh	Článek ve sborníku
Konference	Theoretical Aspects of Computing – ICTAC 2014
Fakulta / Pracoviště MU	Fakulta informatiky
Citace
Doi	http://dx.doi.org/10.1007/978-3-319-10882-7_4
Obor	Informatika
Klíčová slova	Linear Temporal Logic; Timed Automata; Automata-based Model Checking
Popis	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.
Související projekty:	Řízení a ověřování vlastností komplexních hybridních systémů Zaměstnáním čerstvých absolventů doktorského studia k vědecké excelenci Rozsáhlé výpočetní systémy: modely, aplikace a verifikace III.