Nancy Lynch and Sergio Rajsbaum. On the Borowsky-Gafni Simulation Algorithm. Extended Abstract in Proceedings of ISTCS 1996: The Fourth Israel Symposium on Theory of Computing and Systems, Jerusalem, Israel, pages 4-15, June 1996. Also, short version in Proceedings of the Fifteenth Annual ACM Symposium on Principles of Distributed Computing, Philadelphia, PA, page 57, May 1996. .pdf.

Abstract

The first precise description of a version of the Borowsky-Gafni fault-tolerant simulation algorithm is given, along with a careful description of what it accomplishes and a proof of correctness. The algorithm implements a notion of fault-tolerant reducibility between decision problems. This notion of reducibility is defined, and examples of its use are provided.

The algorithm is presented and verified in terms of I/O automata. The presentation has a great deal of interesting modularity, expressed by I/O automaton composition and both forward and backward simulation relations. Composition is used to include a safe agreement module as a subroutine. Forward and backward simulation relations are used to view the algorithm as implementing a multi-try snapshot strategy.