Picture water droplets

Developing mathematical theories of the physical world: Open Access research on fluid dynamics from Strathclyde

Strathprints makes available Open Access scholarly outputs by Strathclyde's Department of Mathematics & Statistics, where continuum mechanics and industrial mathematics is a specialism. Such research seeks to understand fluid dynamics, among many other related areas such as liquid crystals and droplet evaporation.

The Department of Mathematics & Statistics also demonstrates expertise in population modelling & epidemiology, stochastic analysis, applied analysis and scientific computing. Access world leading mathematical and statistical Open Access research!

Explore all Strathclyde Open Access research...

Neighbourhood structures : bisimilarity and basic model theory

Hansen, Helle Hvid and Kupke, Clemens and Pacuit, Eric (2009) Neighbourhood structures : bisimilarity and basic model theory. Logical Methods in Computer Science, 5 (2). ISSN 1860-5974

Full text not available in this repository. Request a copy from the Strathclyde author

Abstract

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 2². We use this coalgebraic modelling to derive notions of equivalence between neighbourhood structures. 2²-bisimilarity and behavioural equivalence are well known coalgebraic concepts, and they are distinct, since 2² 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 2²-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 2²-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.