FORWARD AND BACKWARD SIMULATIONS PART I: UNTIMED SYSTEMS (replaces TM-486)
N. Lynch, Frits Vaandrager · DSpace@MIT (Massachusetts Institute of Technology) · 1994
A unified, comprehensive presentation of simulation techniques for verification of concurrent systems is given, in terms of a simple untimed automaton model. In particular, (1) refinements, (2) forward and backward simulations, (3) hybrid forward-backward and backward-forward simulations, and (4) history and prophecy relations are defined.