Completeness of ASM Refinement

ASM refinements are verified using generalized forward simulations which allow to refine m abstract operations to n concrete operations with arbitrary m and n. One main difference to data refinement is that ASM refinement considers infinite runs and termination. Since backward simulation does not preserve termination in general, the standard technique of adding history information to the concrete level is not applicable. The powerset construction also adds infinite runs and is therefore not applicable too. This paper shows that a completeness proof is nevertheless possible by adding infinite prophecy information, effectively moving nondetermism to the initial state. Adding such prophecy information can be done on the semantic level, but also by a simple syntactic transformation that removes the choose construct of ASMs. The completeness proof is also ported to give a completeness proof for IO automata.