Please use this identifier to cite or link to this item: http://hdl.handle.net/1813/6940
 Title: Limit Operators and Convergence Measures for $\omega$-Languages with Applications to Extreme Fairness Authors: Klarlund, Nils Keywords: computer sciencetechnical report Issue Date: Feb-1990 Publisher: Cornell University Citation: http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR90-1100 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. URI: http://hdl.handle.net/1813/6940 Appears in Collections: Computer Science Technical Reports

Files in This Item:

File Description SizeFormat