Skip to main content


eCommons@Cornell

eCommons@Cornell >
College of Engineering >
Computer Science >
Computer Science Technical Reports >

Please use this identifier to cite or link to this item: http://hdl.handle.net/1813/6993
Title: Progress Measures and Finite Arguments for Infinite Computation
Authors: Klarlund, Nils
Keywords: computer science
technical report
Issue Date: Sep-1990
Publisher: Cornell University
Citation: http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR90-1153
Abstract: We establish principles for proving properties about infinite computations by reasoning about finite ones. We apply these principles to show that for a wide variety of verification problems - involving nondeterminism, fairness, and liveness - there are assertional verification methods that directly relate program and specification. Most previous research relies on transformations of programs in order to reduce a verification problem to problems that can be solved using classical techniques such a refinement mappings and well-founded orderings. Progress measures, the key innovation of this thesis, provide direct, syntax-independent verification techniques for a wide range of specifications. We exhibit progress measures for the language containment problem for nondeterministic automata; for verification with general fairness constraints; and for verification of very general specifications, including infinitary temporal logics. We obtain and optimal solution (in a recursion-theoretic sense) to the problem of verifying infinite computations by reasoning about finite ones. This result establishes a link between descriptive set theory and the theory of verification.
URI: http://hdl.handle.net/1813/6993
Appears in Collections:Computer Science Technical Reports

Files in This Item:

File Description SizeFormat
90-1153.pdf7.55 MBAdobe PDFView/Open
90-1153.ps1.61 MBPostscriptView/Open

Refworks Export

Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.

 

© 2014 Cornell University Library Contact Us