## Model-Checking in Dense Real-Time

*Rajeev Alur, Costas Courcoubetis, and
David L. Dill*
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).