Nancy Lynch and Frits Vaandrager. Forward and Backward Simulations, Part I: Untimed Systems. Technical Memo, MIT/LCS/TM-486, Laboratory for Computer Science, Massachusetts Institute of Technology, Cambridge, MA 02139, May 1993. (Compressed Postscript)

Abstract

A comprehensive presentation of simulation techniques is given in terms of a simple (untimed) automaton model. In particular, we discuss (1) refinements, (2) forward and backward simulations, (3) forward-backward and backward-forward simulations, and (4) history and prophecy relations. History and prophecy relations are new and are abstractions of the history and prophecy variables of Abadi and Lamport, as well as the auxiliary variables of Owicki and Gries. We give elegant and short proofs of soundness and completeness results for complicated simulations in terms of soundness and (partial) completeness results for simple simulations. In Part II of this paper, it is shown how most of the results for untimed automata can be carried over smoothly to the setting of timed automata.