Abstract
| Language | English |
|---|---|
| Article number | 2 |
| Number of pages | 38 |
| Journal | Logical Methods in Computer Science |
| Volume | 5 |
| Issue number | 2 |
| DOIs | |
| Publication status | Published - 9 Apr 2009 |
Fingerprint
Keywords
- Neighbourhood semantics
- non-normal modal logic
- bisimulation
- behavioural equivalence
Cite this
}
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 journal › Article
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 -