On Clock-Aware LTL Properties of Timed Automata

Autoři BEZDĚK Peter BENEŠ Nikola — HAVEL Vojtěch — BARNAT Jiří ČERNÁ Ivana
Druh Článek ve sborníku
Citace 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, 18 s. ISBN 978-3-319-10881-0. doi:10.1007/978-3-319-10882-7_4.
Originální jazyk angličtina
Obor Informatika
Doi http://dx.doi.org/10.1007/978-3-319-10882-7_4
Klíčová slova Linear Temporal Logic; Timed Automata; Automata-based Model Checking

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:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.

Další info