Observational equivalence between coalgebras over Set

Coalgebras provide a framework for studying various types of transition systems in a uniform way. In particular the theory of coalgebras yields for a given type of transition system a notion of "observational equivalence". In case the systems under consideration can be represented as coalgebras for a weak pullback preserving set functor F, observational equivalence can be nicely captured using the so-called "F-bisimulations". In my talk I want to focus on observational equivalence between coalgebras for functors that lack this property. For these functors I will propose so-called "relational equivalences" (a notion based on pushouts) as a useful generalization of F-bisimulations.

In the first part of my talk I want to motivate why coalgebras for functors that do not preserve weak pullbacks are interesting by taking a closer look at neighbourhood frames. In coalgebraic terms, a neighbourhood frame is a coalgebra for the contravariant powerset functor composed with itself, i.e., a coalgebra for a functor that does not preserve weak pullbacks. I will discuss observational equivalence between neighbourhood frames in detail and finally sketch how to obtain a Van Benthem characterisation theorem for classical modal logic: over the class of neighbourhood frames classical modal logic can be seen as the fragment of first-order logic that is invariant under observational equivalence.

In the second part of the talk I want to argue why, in my opinion, relational equivalences are a useful generalization of coalgebraic bisimulations. We characterize those set functors F for which every observational equivalence between F-coalgebras is a relational equivalence.