Enhancements of the bisimulation proof method

This tutorial discusses enhancements of the bisimulation proof method, with the goal of facilitating the proof of bisimilarity results. The bisimulation proof method is one of the main reasons for the success of bisimilarity. According to the method, to establish the bisimilarity between two given objects one has to find a bisimulation relation containing these objects as a pair. This means proving a certain closure property for each pair in the relation. The amount of work needed in proofs therefore depends on the size of the relation. The enhancements of the method in the chapter allow one to reduce such work by using relations that need only be contained in bisimulation relations. The chapter shows that it is possible to define a whole theory of enhancements, which can be very effective in applications.