Enhancements of the bisimulation proof method
Damien Pous, Davide Sangiorgi · Cambridge University Press eBooks · 2011
One of the main reasons for the success of bisimilarity is the strength of the associated proof method. We discuss here the method on processes, more precisely, on Labelled Transition Systems (LTSs). However the reader should bear in mind that the bisimulation concept has applications in many areas beyond concurrency [San12]. According to the proof method, to establish that two processes are bisimilar it suffices to find a relation on processes that contains the given pair and that is a bisimulation. Being a bisimulation means that related processes can match each other's transitions so that the derivatives are again related. In general, when two processes are bisimilar there may be many relations containing the pair, including the bisimilarity relation, defined as the union of all bisimulations. However, the amount of work needed to prove that a relation is a bisimulation depends on its size, since there are transition diagrams to check for each pair. It is therefore important to use relations as small as possible. In this chapter we show that the bisimulation proof method can be enhanced, by employing relations called ‘bisimulations up to’. These relations need not be bisimulations; they are just contained in a bisimulation. The proof that a relation is a ‘bisimulation up to’ follows diagram-chasing arguments similar to those in bisimulation proofs. The reason why ‘bisimulations up to’ are interesting is that they can be substantially smaller than any enclosing bisimulation; hence they may entail much less work in proofs.