## What Good Are Digital Clocks?

*
Thomas A. Henzinger,
Zohar Manna, and Amir Pnueli*

Real-time systems operate in "real," continuous time and state changes
may occur at any real-numbered time point. Yet many verification
methods are based on the assumption that states are observed at
integer time points only. What can we conclude if a real-time system
has been shown "correct" for integral observations?

Integer-time verification techniques suffice if the problem of whether
all real-numbered behaviors of a system satisfy a property can be
reduced to the question of whether the integral observations satisfy a
(possibly modified) property. We show that this reduction is possible
for a large and important class of systems and properties: the class
of systems includes all systems that can be modeled as timed
transition systems; the class of properties includes time-bounded
invariance and time-bounded response.

*Proceedings of the
19th International Colloquium on Automata, Languages, and Programming*
(ICALP),
Lecture Notes in Computer Science 623,
Springer, 1992, pp. 545-558.

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