## Verification Methods for the Divergent Runs of Clock Systems

*
Thomas A. Henzinger
and Peter W. Kopke*

We present a methodology for proving temporal properties of the
divergent runs of reactive systems with real-valued clocks. A run
*diverges* if time advances beyond any bound. Since the
divergent runs of a system may satisfy liveness properties that are
not satisfied by some convergent runs, the standard proof rules are
incomplete if only divergent runs are considered.

First, we develop a sound and complete proof calculus for divergence,
which is based on translating clock systems into discrete systems.
Then, we show that simpler proofs can be obtained for stronger
divergence assumptions, such as *unknown epsilon-divergence*,
which requires that all delays have a minimum duration of some unknown
constant epsilon. We classify all real-time systems into an infinite
hierarchy, according to how well they admit the translation of
eventuality properties into equivalent safety properties.

*Proceedings of the
Third International Symposium on Formal Techniques in Real-Time and
Fault-Tolerant Systems*
(FTRTFT),
Lecture Notes in Computer Science 863,
Springer, 1994, pp. 351-372.

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