Nancy Lynch and Frits Vaandrager. Forward and Backward Simulations, Part II: Timing-Based Systems. Information and Computation, 128(1):1-25, July 1996. .pdf Also, Technical Memo MIT/LCS/TM-487.c., Laboratory for Computer Science, Massachusetts Institute of Technology. .pdf.

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) hybrid forward-backward and backward-forward simulations, and (4) history and prophecy relations. Relationships between the different types of simulations, as well as soundness and completeness results, are stated and proved. 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.