Coinduction up-to techniques

Daniela Petrisan

Bisimulations and coinduction are used in concurrency theory as proof methods for establishing behavioural equivalence of processes. Up-to techniques can be seen as a means of optimizing proofs by coinduction. For example, to establish that two processes are equivalent one can exhibit a smaller relation, which is not a bisimulation, but rather a bisimulation up to a certain technique, say ‘up-to contextual closure’. However, the up-to technique at issue has to be sound, in the sense that any bisimulation up-to should be included in a bisimulation. In this talk, I will present a general coalgebraic framework for proving the soundness of a wide range of up-to techniques for coinductive unary predicates, as well as for bisimulations. The specific up-to techniques are obtained using liftings of functors to appropriate categories of relations or predicates. I will give an overview of this framework and illustrate it with examples such as techniques for proving language equivalence of nominal automata, simulations and bisimulations with silent moves. This is joint work with Filippo Bonchi, Damien Pous and Jurriaan Rot.