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.