Neighbourhood Structures: Bisimilarity and Basic Model Theory

H.H. Hansen, C. Kupke, E. Pacuit

Research output: Contribution to JournalArticleAcademicpeer-review

101 Downloads (Pure)


Neighbourhood structures are the standard semantic tool used to reason aboutnon-normal modal logics. The logic of all neighbourhood models is called classical modallogic. In coalgebraic terms, a neighbourhood frame is a coalgebra for the contravariantpowerset functor composed with itself, denoted by22. We use this coalgebraic modellingto derive notions of equivalence between neighbourhood structures.22-bisimilarity andbehavioural equivalence are well known coalgebraic concepts, and they are distinct, since22does not preserve weak pullbacks. We introduce a third, intermediate notion whose wit-nessing relations we call precocongruences (based on pushouts). We give back-and-forthstyle characterisations for22-bisimulations and precocongruences, we show that on a singlecoalgebra, precocongruences capture behavioural equivalence, and that between neighbour-hood structures, precocongruences are a better approximation of behavioural equivalencethan22-bisimulations. We also introduce a notion of modal saturation for neighbourhoodmodels, and investigate its relationship with definability and image-finiteness. We prove aHennessy-Milner theorem for modally saturated and for image-finite neighbourhood mod-els. Our main results are an analogue of Van Benthem’s characterisation theorem and amodel-theoretic proof of Craig interpolation for classical modal logic
Original languageEnglish
Article number1167
Pages (from-to)1-38
Number of pages38
JournalLogical Methods in Computer Science
Issue number2
Publication statusPublished - 9 Apr 2009


Dive into the research topics of 'Neighbourhood Structures: Bisimilarity and Basic Model Theory'. Together they form a unique fingerprint.

Cite this