Cornell University
Library
Cornell UniversityLibrary

eCommons

Help
Log In(current)
  1. Home
  2. Cornell Computing and Information Science
  3. Computer Science
  4. Computer Science Technical Reports
  5. Verification Methods for the Divergent Runs of Clock Systems

Verification Methods for the Divergent Runs of Clock Systems

File(s)
95-1482.pdf (287.24 KB)
95-1482.ps (348.49 KB)
Permanent Link(s)
https://hdl.handle.net/1813/7141
Collections
Computer Science Technical Reports
Author
Henzinger, Thomas A.
Kopke, Peter W.
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.

Date Issued
1995-02
Publisher
Cornell University
Keywords
computer science
•
technical report
Previously Published as
http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR95-1482
Type
technical report

Site Statistics | Help

About eCommons | Policies | Terms of use | Contact Us

copyright © 2002-2026 Cornell University Library | Privacy | Web Accessibility Assistance