Eternity variables to prove simulation of specifications
<|reference_start|>Eternity variables to prove simulation of specifications: Simulations of specifications are introduced as a unification and generalization of refinement mappings, history variables, forward simulations, prophecy variables, and backward simulations. A specification implements another specification if and only if there is a simulation from the first one to the second one that satisfies a certain condition. By adding stutterings, the formalism allows that the concrete behaviours take more (or possibly less) steps than the abstract ones.   Eternity variables are introduced as a more powerful alternative for prophecy variables and backward simulations. This formalism is semantically complete: every simulation that preserves quiescence is a composition of a forward simulation, an extension with eternity variables, and a refinement mapping. This result does not need finite invisible nondeterminism and machine closure as in the Abadi-Lamport Theorem. Internal continuity is weakened to preservation of quiescence.<|reference_end|>
@article{hesselink2002eternity,
    title={Eternity variables to prove simulation of specifications},
    author={Wim H. Hesselink},
    journal={ACM Trans. on Computational Logic 6 (2005) 175-201.},
    year={2002},
    archivePrefix={arXiv},
    eprint={cs/0207095},
    primaryClass={cs.DC cs.LO}
}