Coinduction Up-To in a Fibrational Setting

ABSTRACT. Bisimulation up-to enhances the coinductive proof method for bisimilarity, providing efficient proof techniques for equivalences of different kinds of systems. Even before Milner introduced and applied such methods in his work on CCS, Hopcroft and Karp used up-to techniques to check equivalence of deterministic automata.

In this work, we prove the soundness of such techniques in an abstract fibrational setting building on the seminal work of Hermida and Jacobs. To do this in a modular way we generalise Pous and Sangiorgi's notion of \emph{compatibility}. This allows us to systematically prove the soundness of up-to techniques, not only for bisimilarity but for a large class of coinductive predicates modeled as coalgebras. By tuning the parameters of our framework, we obtain novel proof techniques for unary predicates and nominal automata, a variant of the GSOS rule format for similarity, and a new categorical treatment of weak bisimilarity.