Progress measures and finite arguments for infinite computations

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 as 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 an 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.