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.