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. Limit Operators and Convergence Measures for $\omega$-Languages with Applications to Extreme Fairness

Limit Operators and Convergence Measures for $\omega$-Languages with Applications to Extreme Fairness

File(s)
90-1100.pdf (1.28 MB)
90-1100.ps (340.23 KB)
Permanent Link(s)
https://hdl.handle.net/1813/6940
Collections
Computer Science Technical Reports
Author
Klarlund, Nils
Abstract

Methods of program verification for liveness and fairness rely on measuring "progress" of finite computations towards satisfying the specification. Previous methods are based on explaining progress in terms of well-founded sets. These approaches, however, often led to complicated transformations or inductive applications of proof rules. Our main contribution is a simpler measure of progress based on an ordering that is not well-founded. This ordering is a variation on the Kleene-Brouwer ordering on nodes of a finite-path tree. It has the unusual property that for any infinite ordered sequence of nodes, the liminf of the node depths (levels) is finite. This novel view of progress gives a precise mathematical characterization of what it means to satisfy very general program properties. In particular, we solve the problem of finding a progress measure for termination under extreme fairness.

Date Issued
1990-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/TR90-1100
Type
technical report

Site Statistics | Help

About eCommons | Policies | Terms of use | Contact Us

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