Completeness of Fair 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 to get a completeness proof. The powerset construction also adds infinite runs and is therefore not applicable either. This paper shows that a completeness proof is nevertheless possible by adding infinite prophecy information, effectively moving nondeterminism 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. Finally, the proof is extended to deal with supplementary predicates, that specify fairness and liveness assumptions, by porting a related result of Wim Hesselink for refinements that use the Abadi-Lamport setting.