Nancy Lynch and Frits Vaandrager. Forward and Backward Simulations, Part II: Timing-Based Systems. Revised since Laboratory for Computer Science, Massachusetts Institute of Technology, Cambridge MA, Technical Memo MIT/LCS/TM-487.b., April 1993. Updated version --September 1993. (Compressed Postscript)

Abstract

A general automaton model for timing-based systems is presented and is used as the context for developing a variety of simulation proof techniques for such systems. These techniques include (1) refinements, (2) forward and backward simulations, (3) forward-backward and backward-forward simulations, and (4) history and prophecy relations. Soundness and completeness results are given for these simulations. These results are largely analogous to the results in Part I of this paper for untimed systems. In fact, many of the results for the timed case are obtained as consequences of the analogous results for the untimed case.