Model-checking is a method of verifying concurrent systems in which a state-transition graph model of the system behavior is compared with a temporal logic formula. This paper extends model-checking for the branching-time logic CTL to the analysis of {\it real-time\/} systems, whose correctness depends on the magnitudes of the timing delays. For specifications, we extend the syntax of CTL to allow quantitative temporal operators such as $\exists\Diamond_{<5}$, meaning ``possibly within 5 time units.'' The formulas of the resulting logic, {\it Timed CTL\/} (TCTL), are interpreted over {\em continuous computation trees\/}, trees in which paths are maps from the set of nonnegative reals to system states. To model finite-state systems we introduce {\em timed graphs\/} --- state-transition graphs annotated with timing constraints.
As our main result, we develop an algorithm for model-checking, for determining the truth of a TCTL-formula with respect to a timed graph. We argue that choosing a dense domain instead of a discrete domain to model time does not significantly blow up the complexity of the model-checking problem. On the negative side, we show that the denseness of the underlying time domain makes the validity problem for TCTL $\Pi_1^1$-hard. The question of deciding whether there exists a timed graph satisfying a TCTL-formula is also undecidable.
Information and Computation 104(1):2-34, 1993. A preliminary version appeared in the Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science (LICS 1990).