Neighbourhood Structures: Bisimilarity and Basic Model Theory

Details Neighbourhood Structures: Bisimilarity and Basic Model Theory Neighbourhood Structures: Bisimilarity and Basic Model Theory

2009-01-28

arxiv.org/abs/0901.4430v4

LMCS 5 (2:2) 2009

Computer Science

Logic in Computer Science

uses LMCS.cls (included), 2 figures (both ps and pdf)

Scientific paper

10.2168/LMCS-5(2:2)2009

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

Affiliated with

Also associated with

No associations

Rating

Neighbourhood Structures: Bisimilarity and Basic Model Theory does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Neighbourhood Structures: Bisimilarity and Basic Model Theory, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Neighbourhood Structures: Bisimilarity and Basic Model Theory will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-344636