TY - CONF AB - 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. AU - Henzinger, Thomas A AU - Manna, Zohar AU - Pnueli, Amir ID - 4504 T2 - 19th International Colloquium on Automata, Languages and Programming TI - What good are digital clocks? VL - 623 ER -