  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.
