Limit Operators and Convergence Measures for $\omega$-Languages with Applications to Extreme Fairness
| dc.contributor.author | Klarlund, Nils | en_US |
| dc.date.accessioned | 2007-04-23T17:45:38Z | |
| dc.date.available | 2007-04-23T17:45:38Z | |
| dc.date.issued | 1990-02 | en_US |
| dc.description.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. | en_US |
| dc.format.extent | 1340242 bytes | |
| dc.format.extent | 348397 bytes | |
| dc.format.mimetype | application/pdf | |
| dc.format.mimetype | application/postscript | |
| dc.identifier.citation | http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR90-1100 | en_US |
| dc.identifier.uri | https://hdl.handle.net/1813/6940 | |
| dc.language.iso | en_US | en_US |
| dc.publisher | Cornell University | en_US |
| dc.subject | computer science | en_US |
| dc.subject | technical report | en_US |
| dc.title | Limit Operators and Convergence Measures for $\omega$-Languages with Applications to Extreme Fairness | en_US |
| dc.type | technical report | en_US |