MODEL-CHECKING IN DENSE REAL-TIME

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 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 ∃{white diamond suit} <5, meaning "possibly within 5 time units." The formulas of the resulting logic, Timed CTL (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 we introduce 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 Π11-hard. The question of deciding whether there exists a timed graph satisfying a TCTL-formula is also undecidable. © 1993 Academic Press, Inc.