Equations, contractions, and unique solutions

This talk is about proof techniques for behavioural equivalences. One of the most studied behavioural equivalences is bisimulation, and the main reason for its success is the associated bisimulation proof method. This method can be further enhanced by means of `up-to bisimulation' techniques. In the talk, I will discuss a different proof method, based on unique solutions of equations. I will introduce contractions, special forms of inequations. I will show that the `unique solution of contraction' method is at least as powerful as the bisimulation proof method and its enhancements. I will then show that the method can be transferred onto other behavioural equivalences,possibly non-coinductive, enabling the coinductive reasoning style with these equivalences too.