Skip to main content


eCommons@Cornell >
College of Engineering >
Computer Science >
Computer Science Technical Reports >

Please use this identifier to cite or link to this item:
Title: Verification Methods for the Divergent Runs of Clock Systems
Authors: Henzinger, Thomas A.
Kopke, Peter W.
Keywords: computer science
technical report
Issue Date: Feb-1995
Publisher: Cornell University
Abstract: 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.
Appears in Collections:Computer Science Technical Reports

Files in This Item:

File Description SizeFormat
95-1482.pdf287.24 kBAdobe PDFView/Open
95-1482.ps348.49 kBPostscriptView/Open

Refworks Export

Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.


© 2014 Cornell University Library Contact Us