Model-checking for real-time systems

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 interpreted 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 transitions. 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.