TY - JOUR

T1 - Neighbourhood structures: bisimilarity and basic model theory

AU - Hansen, H.H.

AU - Kupke, C.A.

AU - Pacuit, E.

PY - 2009

Y1 - 2009

N2 - Neighbourhood structures are the standard semantic tool used to reason about
non-normal modal logics. The logic of all neighbourhood models is called classical modal
logic. In coalgebraic terms, a neighbourhood frame is a coalgebra for the contravariant
powerset functor composed with itself, denoted by 22. We use this coalgebraic modelling
to derive notions of equivalence between neighbourhood structures. 22-bisimilarity and
behavioural equivalence are well known coalgebraic concepts, and they are distinct, since
22 does not preserve weak pullbacks. We introduce a third, intermediate notion whose witnessing relations we call precocongruences (based on pushouts). We give back-and-forth style characterisations for 22-bisimulations and precocongruences, we show that on a single coalgebra, precocongruences capture behavioural equivalence, and that between neighbourhood structures, precocongruences are a better approximation of behavioural equivalence than 22-bisimulations. We also introduce a notion of modal saturation for neighbourhood models, and investigate its relationship with definability and image-finiteness. We prove a Hennessy-Milner theorem for modally saturated and for image-finite neighbourhood models. Our main results are an analogue of Van Benthem's characterisation theorem and a model-theoretic proof of Craig interpolation for classical modal logic.

AB - Neighbourhood structures are the standard semantic tool used to reason about
non-normal modal logics. The logic of all neighbourhood models is called classical modal
logic. In coalgebraic terms, a neighbourhood frame is a coalgebra for the contravariant
powerset functor composed with itself, denoted by 22. We use this coalgebraic modelling
to derive notions of equivalence between neighbourhood structures. 22-bisimilarity and
behavioural equivalence are well known coalgebraic concepts, and they are distinct, since
22 does not preserve weak pullbacks. We introduce a third, intermediate notion whose witnessing relations we call precocongruences (based on pushouts). We give back-and-forth style characterisations for 22-bisimulations and precocongruences, we show that on a single coalgebra, precocongruences capture behavioural equivalence, and that between neighbourhood structures, precocongruences are a better approximation of behavioural equivalence than 22-bisimulations. We also introduce a notion of modal saturation for neighbourhood models, and investigate its relationship with definability and image-finiteness. We prove a Hennessy-Milner theorem for modally saturated and for image-finite neighbourhood models. Our main results are an analogue of Van Benthem's characterisation theorem and a model-theoretic proof of Craig interpolation for classical modal logic.

U2 - 10.2168/LMCS-5(2:2)2009

DO - 10.2168/LMCS-5(2:2)2009

M3 - Article

SN - 1860-5974

VL - 5

SP - 1

EP - 38

JO - Logical Methods in Computer Science

JF - Logical Methods in Computer Science

IS - 2:2

ER -