Logic in Computer Science (LICS 1990)

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

Authors: Alur, R. Courcoubetis, C. Dill, D.

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

BibTeX

  @InProceedings{AlurCourcoubetisDil-Modelcheckingforrea,
    author = 	 {Alur, R. and Courcoubetis, C. and Dill, D.},
    title = 	 {Model-checking for real-time systems},
    booktitle =  {Proceedings of the Fifth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1990},
    year =	 1990,
    editor =	 {John Mitchell},
    month =	 {June}, 
    pages =      {414--425},
    location =   {Philadelphia, PA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }