Bisimulations for neighbourhood structures

Neighbourhood semantics forms a generalisation of Kripke semantics, and it has become the standard tool for reasoning about non-normal modal logics in which (Kripke valid) principles such as []p /\ []q (Meet) and []p -> (Mon) are considered not to hold. In computer science and social choice theory, non-normal modal logics are used to formalise system (or agent) properties in terms of ability in strategic games. These logics have in common that they are monotonic, meaning they contain the above formula (Mon). Non-monotonic modal logics occur in deontic logic where monotonicity can lead to paradoxical obligations, and in the modelling of knowledge and related epistemic notions.

Bisimulation for monotonic neighbourhood structures has already been studied in detail (by M. Pauly, and in our previous work). But based on simple intuitions, it is not immediately clear how this notion can be generalised to non-monotonic structures. This is where coalgebra proves useful. A neighbourhood frame is a coalgebra for the contravariant powerset functor composed with itself, and this coalgebraic modelling provides us with a number of generic notions of observational equivalence.

In our talk we first discuss and compare three (coalgebraic) equivalence notions on neighbourhood structures: bisimilarity (for the functor), neighbourhood bisimilarity and behavioural equivalence. We provide relational characterisations for bisimilarity and neighbourhood bisimilarity, and we show that with respect to these two notions the class of finite models is not a Hennessy-Milner class. Behavioural equivalence, on the other hand, does give rise to a Hennessy-Milner theorem, but it seems harder to characterise relationally. Finally we show an analogue of Van Benthem's characterisation theorem: Over the class of neighbourhood models, all three notions characterise the modal fragment of first-order logic.  

hosted by