Bisimulation for Neighbourhood Structuress
Helle Hvid Hansen, Clemens Kupke, Eric Pacuit

Abstract:
Neighbourhood structures are the standard semantic tool used to reason
about non-normal modal logics. In coalgebraic terms, a neighbourhood
frame is a coalgebra for the contravariant powerset functor composed
with itself, denoted by 2^2. In our paper, we investigate the
coalgebraic equivalence notions of 2^2-bisimulation, behavioural
equivalence and neighbourhood bisimulation (a notion based on
pushouts), with the aim of finding the logically correct notion of
equivalence on neighbourhood structures.  Our results include
relational characterisations for 2^2-bisimulation and neighbourhood
bisimulation, and an analogue of Van Benthem's characterisation
theorem for all three equivalence notions. We also show that
behavioural equivalence gives rise to a Hennessy-Milner theorem, and
that this is not the case for the other two equivalence notions.