Limit Operators and Convergence Measures for $\omega$-Languages with Applications to Extreme Fairness
Loading...
No Access Until
Permanent Link(s)
Collections
Other Titles
Authors
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.
Journal / Series
Volume & Issue
Description
Sponsorship
Date Issued
1990-02
Publisher
Cornell University
Keywords
computer science; technical report
Location
Effective Date
Expiration Date
Sector
Employer
Union
Union Local
NAICS
Number of Workers
Committee Chair
Committee Co-Chair
Committee Member
Degree Discipline
Degree Name
Degree Level
Related Version
Related DOI
Related To
Related Part
Based on Related Item
Has Other Format(s)
Part of Related Item
Related To
Related Publication(s)
Link(s) to Related Publication(s)
References
Link(s) to Reference(s)
Previously Published As
http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR90-1100
Government Document
ISBN
ISMN
ISSN
Other Identifiers
Rights
Rights URI
Types
technical report