IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Fifth Annual IEEE Symposium on

Logic in Computer Science (LICS 1990)

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

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


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 II11-hard. The question of deciding whether a given TCTL formula is implementable by a timed graph is also undecidable


    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}

Last modified: 2016-01-1416:21
Andrzej Murawski