Neighbourhood structures: bisimilarity and basic model theory

Helle Hvid Hansen, Clemens Kupke, Eric Pacuit

Research output: Contribution to journalArticle

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.
LanguageEnglish
Article number2
Number of pages38
JournalLogical Methods in Computer Science
Volume5
Issue number2
DOIs
Publication statusPublished - 9 Apr 2009

Fingerprint

Model Theory
Modal Logic
Equivalence
Bisimulation
Classical Logic
Coalgebra
Interpolation
Semantics
Definability
Characterization Theorem
Pullback
Finiteness
Model
Functor
Saturation
Interpolate
Logic
Analogue
Distinct
Term

Keywords

  • Neighbourhood semantics
  • non-normal modal logic
  • bisimulation
  • behavioural equivalence

Cite this

@article{c1f239e50982425babe41d0983ae18f4,
title = "Neighbourhood structures: bisimilarity and basic model theory",
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.",
keywords = "Neighbourhood semantics, non-normal modal logic, bisimulation, behavioural equivalence",
author = "Hansen, {Helle Hvid} and Clemens Kupke and Eric Pacuit",
year = "2009",
month = "4",
day = "9",
doi = "10.2168/LMCS-5(2:2)2009",
language = "English",
volume = "5",
journal = "Logical Methods in Computer Science",
issn = "1860-5974",
number = "2",

}

Neighbourhood structures : bisimilarity and basic model theory. / Hansen, Helle Hvid; Kupke, Clemens; Pacuit, Eric.

In: Logical Methods in Computer Science, Vol. 5, No. 2, 2, 09.04.2009.

Research output: Contribution to journalArticle

TY - JOUR

T1 - Neighbourhood structures

T2 - Logical Methods in Computer Science

AU - Hansen, Helle Hvid

AU - Kupke, Clemens

AU - Pacuit, Eric

PY - 2009/4/9

Y1 - 2009/4/9

N2 - 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.

AB - 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.

KW - Neighbourhood semantics

KW - non-normal modal logic

KW - bisimulation

KW - behavioural equivalence

U2 - 10.2168/LMCS-5(2:2)2009

DO - 10.2168/LMCS-5(2:2)2009

M3 - Article

VL - 5

JO - Logical Methods in Computer Science

JF - Logical Methods in Computer Science

SN - 1860-5974

IS - 2

M1 - 2

ER -