Skip to main navigation Skip to search Skip to main content

Bisimulation for neighbourhood structures

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

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    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 22. In our paper, we investigate the coalgebraic equivalence notions of 22-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 22-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
    Title of host publicationAlgebra and coalgebra in computer science : 2nd iternational conference, CALCO 2007, Bergen, Norway, August 20-24, 2007. : proceedings
    EditorsT. Mossakowski, U. Montanari, M. Haveraaen
    Place of PublicationBerlin
    PublisherSpringer
    Pages279-293
    ISBN (Print)978-3-540-73857-2
    DOIs
    Publication statusPublished - 2007

    Publication series

    NameLecture Notes in Computer Science
    Volume4624
    ISSN (Print)0302-9743

    Fingerprint

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

    Cite this