Abstract
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 language | English |
---|---|
Article number | 1167 |
Pages (from-to) | 1-38 |
Number of pages | 38 |
Journal | Logical Methods in Computer Science |
Volume | 5 |
Issue number | 2 |
DOIs | |
Publication status | Published - 9 Apr 2009 |