## Paper: Model-checking for real-time systems (at LICS 1990)

*Winner of the Test-of-Time Award in 2010***Rajeev Alur Costas Courcoubetis David L. Dill**

### Abstract

This research extends CTL model-checking to the analysis of real-time systems, whose correctness depends on the magnitudes
of the timing delays. For specifications, the syntax of CTL is extended to allow quantitative temporal operators. The formulas
of the resulting logic, TCTL, are interpretation over continuous computation trees, trees in which paths are maps from the
set of nonnegative reals to system states. To model finite-state systems the notion of timed graphs is introduced-state-transition
graphs extended with a mechanism that allows the expression of constant bounds on the delays between the state transition.
As the main result, an algorithm is developed for model checking, that is, for determining the truth of a TCTL formula with
respect to a timed graph. It is argued that choosing a dense domain, instead of a discrete domain, to model time does not
blow up the complexity of the model-checking problem. On the negative side, it is shown that the denseness of the underlying
time domain makes TCTL II_{1}^{1}-hard. The question of deciding whether a given TCTL formula is implementable by a timed graph is also undecidable

### BibTeX

@InProceedings{AlurCourcoubetisDil-Modelcheckingforrea, author = {Rajeev Alur and Costas Courcoubetis and David L. Dill}, title = {Model-checking for real-time systems}, booktitle = {Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science (LICS 1990)}, year = {1990}, month = {June}, pages = {414--425}, location = {Philadelphia, PA, USA}, publisher = {IEEE Computer Society Press} }