What Good Are Digital Clocks?

Real-time systems operate in \real," continuous time and state changes may occur at any real-numbered time point. Yet many veri cation 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 veri cation techniques su ce 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 modi ed)property. Weshow that this reduction is possible for a large and importantclass 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.

• Type: Conference
• Year: 1992
• Where: ICALP
• Authors: Thomas A. Henzinger, Zohar Manna, Amir Pnueli
• Keywords: ICALP 1992, Integer Time, Programming Languages, Real-time System, Veri Cation