The limit view of infinite computations

We show how to view computations involving very general liveness properties as limits of finite approximations. This computational model does not require introduction of infinite nondeterminism as with most traditional approaches. Our results allow us directly to relate finite computations in order to infer properties about infinite computations. Thus we are able to provide a mathematical understanding of what simulations and bisimulations are when liveness is involved. In addition, we establish links between verification theory and classical results in descriptive set theory. Our result on simulations is the essential contents of the Kleene-Suslin Theorem, and our result on bisimulation expresses Martin's Theorem about the determinacy of Borel games.