10.2168/LMCS-5(2:2)2009
https://lmcs.episciences.org/1167
Hansen, Helle Hvid
Helle Hvid
Hansen
Kupke, Clemens
Clemens
Kupke
Pacuit, Eric
Eric
Pacuit
Neighbourhood Structures: Bisimilarity and Basic Model Theory
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.
Comment: uses LMCS.cls (included), 2 figures (both ps and pdf)
episciences.org
Computer Science - Logic in Computer Science
F.1.1
F.3.2
F.4.1
I.2.4
arXiv.org - Non-exclusive license to distribute
2015-06-25
2009-04-09
2009-04-09
eng
journal article
arXiv:0901.4430
10.48550/arXiv.0901.4430
1860-5974
10.1017/s1755020316000447
11245.1/e86e9f61-5ac8-4595-b8f2-67e1400d35ba
https://lmcs.episciences.org/1167/pdf
VoR
application/pdf
Logical Methods in Computer Science
Volume 5, Issue 2
Researchers
Students