Sergio Yovine

IMAG, France

Symbolic Model-Checking for Timed Automata and TCTL: The tool Kronos.

DIMACS Center - Room 431
Busch Campus
Piscataway, New Jersey
November 1, 1995 at 4:30 PM


Timed automata are automata extended with clocks that accurately measure the real time elapsed and have been proposed by Alur and Dill for modelling timed systems. For specifying real-time requirements such as bounded response time, the branching-time temporal logic CTL has also been extended to TCTL (Timed CTL) in a similar way. In this talk I'll present the symbolic model-checking algorithm I developed in collaboration with Henzinger, Sifakis and Nicollin. This algorithm is the basis of the verification tool Kronos. I'll also present the tool and its application to the analysis of several case studies.