Bisimulation for neighbourhood structures

H.H. Hansen, C.A. Kupke, E. Pacuit

    Research output: Book/ReportReportAcademic

    Abstract

    Neighbourhood structures are the standard semantic tool used to reason about non-normal modal logics. In coalgebraic terms, a neighbourhood frame is a coalgebra for the contravariant powerset functor composed with itself, denoted by 2^2. In our paper, we investigate the coalgebraic equivalence notions of 2^2-bisimulation, behavioural equivalence and neighbourhood bisimulation (a notion based on pushouts), with the aim of finding the logically correct notion of equivalence on neighbourhood structures. Our results include relational characterisations for 2^2-bisimulation and neighbourhood bisimulation, and an analogue of Van Benthem's characterisation theorem for all three equivalence notions. We also show that behavioural equivalence gives rise to a Hennessy-Milner theorem, and that this is not the case for the other two equivalence notions.
    Original languageEnglish
    Place of PublicationAmsterdam
    PublisherInstitute for Logic, Language and Computation (ILLC), University of Amsterdam
    Number of pages23
    Publication statusPublished - 2007

    Publication series

    NamePrepublication Series
    VolumePP-2007-30

    Fingerprint

    Dive into the research topics of 'Bisimulation for neighbourhood structures'. Together they form a unique fingerprint.

    Cite this