Skip to main content


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

Please use this identifier to cite or link to this item:
Title: Progress Measures and Finite Arguments for Infinite Computation
Authors: Klarlund, Nils
Keywords: computer science
technical report
Issue Date: Sep-1990
Publisher: Cornell University
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.
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