## From Quantity to Quality

*
Thomas A. Henzinger
and Orna Kupferman*

In temporal-logic model checking, we verify the correctness of a
program with respect to a desired behavior by checking whether a
structure that models the program satisfies a temporal-logic formula
that specifies the behavior. The model-checking problem for the
branching-time temporal logic CTL can be solved in linear running
time, and model-checking tools for CTL are used successfully in
industrial applications. The development of programs that must meet
rigid real-time constraints has brought with it a need for real-time
temporal logics that enable quantitative reference to time. Early
research on real-time temporal logics uses the discrete domain of the
integers to model time. Present research on real-time temporal logics
focuses on continuous time and uses the dense domain of the reals to
model time. There, model checking becomes significantly more
complicated. For example, the model-checking problem for TCTL, a
continuous-time extension of the logic CTL, is PSPACE-complete.

In this paper we suggest a reduction from TCTL model checking to CTL
model checking. The contribution of such a reduction is twofold.
Theoretically, while it has long been known that model-checking
methods for untimed temporal logics can be extended quite easily to
handle discrete time, it was not clear whether and how untimed methods
can handle the reset quantifier of TCTL, which resets a real-valued
clock. Practically, our reduction enables anyone who has a tool for
CTL model checking to use it for TCTL model checking. The TCTL
model-checking algorithm that follows from our reduction is in PSPACE,
matching the known bound for this problem. In addition, it enjoys the
wide distribution of CTL model-checking tools and the extensive and
fruitful research efforts and heuristics that have been put into these
tools.

*Proceedings of the
International Workshop on Hybrid and Real-Time Systems*
(HART),
Lecture Notes in Computer Science 1201,
Springer, 1997, pp. 48-62.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 1997 Springer.