Helle Hvid Hansen ; Clemens Kupke ; Eric Pacuit - Neighbourhood Structures: Bisimilarity and Basic Model Theory

lmcs:1167 - Logical Methods in Computer Science, April 9, 2009, Volume 5, Issue 2 - https://doi.org/10.2168/LMCS-5(2:2)2009
Neighbourhood Structures: Bisimilarity and Basic Model Theory

Authors: Helle Hvid Hansen ; Clemens Kupke ; Eric Pacuit

    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.

    Volume: Volume 5, Issue 2
    Published on: April 9, 2009
    Imported on: December 19, 2007
    Keywords: Computer Science - Logic in Computer Science,F.1.1,F.3.2,F.4.1,I.2.4

    Linked data

    Source : ScholeXplorer IsReferencedBy DOI 10.1017/s1755020316000447
    Source : ScholeXplorer IsReferencedBy HANDLE 11245.1/e86e9f61-5ac8-4595-b8f2-67e1400d35ba
    • 11245.1/e86e9f61-5ac8-4595-b8f2-67e1400d35ba
    • 10.1017/s1755020316000447
    • 10.1017/s1755020316000447
    • 10.1017/s1755020316000447
    Instantial neighbourhood logic
    van Benthem, J. ; Bezhanishvili, N. ; Enqvist, S. ; Yu, J. ;

    36 Documents citing this article

    Consultation statistics

    This page has been seen 1059 times.
    This article's PDF has been downloaded 561 times.