Nancy Lynch and Frits Vaandrager. Forward and backward simulations for timing-based systems. In J. W. de Bakker, W. P. de Roever, C. Huizing, and G. Rozenberg, editors, Proceedings of Real-Time: Theory in Practice (REX Workshop, Mook, The Netherlands, June 1991), volume 600 of Lecture Notes in Computer Science, pages 397-446. Springer-Verlag 1992. .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. As a first step, a comprehensive overview of simulation techniques for simple untimed automata is given. In particular, soundness and completeness results for (1) refinements, (2) forward and backward simulations, (3) forward-backward and backward-forward simulations, and (4) history and prophecy relations are given. History and prophecy relations are new and are abstractions of the history variables of Owicki and Gries and the prophecy variables of Abadi and Lamport, respectively. As a subsequent step, it is shown how most of the results for untimed automata can be carried over to the setting of timed automata. In fact, many of the results for the timed case are obtained as consequences of the analogous results for the untimed case.