On the Borowsky-Gafni simulation algorithm

Abstract

The Borowsky-Gafni simulation can become a powerful tool for proving solvability and unsolvability results for fault-prone asynchronous systems. However, in order for this to happen, it must be clear exactly what the simulation algorithm is, and what it guarantees. This paper aims of stating and proving precise correctness guarantees for the Borowsky-Gafni simulation algorithm, using the I/O automation model and standard proof techniques. The results are complete and careful description of a version of the Borowsky-Gafni simulation algorithm, and a careful description of what it accomplishes, and a proof of correctness.