Technical Reports

A List by Author: Peter Bezdìk

e-mail:

xbezdek1(a)fi.muni.cz

On Clock-Aware LTL Properties of Timed Automata

by Peter Bezdìk, Nikola Bene¹, Vojtìch Havel, Jiøí Barnat, Ivana Èerná, A full version of the paper presented at conference ICTAC 2014. June 2014, 27 pages.

FIMU-RS-2014-04. Available as Postscript, PDF.

Abstract:

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.