On Clock-Aware LTL Properties of Timed Automata

Investor logo

Warning

This publication doesn't include Faculty of Medicine. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

BEZDĚK Peter BENEŠ Nikola HAVEL Vojtěch BARNAT Jiří ČERNÁ Ivana

Year of publication 2014
Type Article in Proceedings
Conference Theoretical Aspects of Computing – ICTAC 2014
MU Faculty or unit

Faculty of Informatics

Citation
Doi http://dx.doi.org/10.1007/978-3-319-10882-7_4
Field Informatics
Keywords Linear Temporal Logic; Timed Automata; Automata-based Model Checking
Description 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.

More info