Neighbourhood Structures: Bisimilarity and Basic Model Theory - Computer Science > Logic in Computer ScienceReportar como inadecuado




Neighbourhood Structures: Bisimilarity and Basic Model Theory - Computer Science > Logic in Computer Science - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

Abstract: Neighbourhood structures are the standard semantic tool used to reason aboutnon-normal modal logics. The logic of all neighbourhood models is calledclassical modal logic. In coalgebraic terms, a neighbourhood frame is acoalgebra for the contravariant powerset functor composed with itself, denotedby 2^2. We use this coalgebraic modelling to derive notions of equivalencebetween neighbourhood structures. 2^2-bisimilarity and behavioural equivalenceare well known coalgebraic concepts, and they are distinct, since 2^2 does notpreserve weak pullbacks. We introduce a third, intermediate notion whosewitnessing relations we call precocongruences based on pushouts. We giveback-and-forth style characterisations for 2^2-bisimulations andprecocongruences, we show that on a single coalgebra, precocongruences capturebehavioural equivalence, and that between neighbourhood structures,precocongruences are a better approximation of behavioural equivalence than2^2-bisimulations. We also introduce a notion of modal saturation forneighbourhood models, and investigate its relationship with definability andimage-finiteness. We prove a Hennessy-Milner theorem for modally saturated andfor image-finite neighbourhood models. Our main results are an analogue of VanBenthem-s characterisation theorem and a model-theoretic proof of Craiginterpolation for classical modal logic.



Autor: Helle Hvid Hansen, Clemens Kupke, Eric Pacuit

Fuente: https://arxiv.org/







Documentos relacionados