• DocumentCode
    2022329
  • Title

    Modal characterisation theorems over special classes of frames

  • Author

    Dawar, Anuj ; Otto, Martin

  • Author_Institution
    Comput. Lab., Cambridge Univ., UK
  • fYear
    2005
  • fDate
    26-29 June 2005
  • Firstpage
    21
  • Lastpage
    30
  • Abstract
    We investigate model theoretic characterisations of the expressive power of modal logics in terms of bisimulation invariance. The paradigmatic result of this kind is van Benthem´s theorem, which says that a first-order formula is invariant under bisimulation if and only if it is equivalent to a formula of basic modal logic. The present investigation primarily concerns ramifications for specific classes of structures. We study in particular model classes defined through conditions on the underlying frames, with a focus on frame classes that play a major role in modal correspondence theory and often correspond to typical application domains of modal logics. Classical model theoretic arguments do not apply to many of the most interesting classes -for instance, rooted connected frames, well-founded frames, finite rooted connected frames, finite transitive frames, finite equivalence frames - as these are not elementary. Instead we develop and extend the game-based analysis (first-order Ehrenfeucht-Fraisse versus bisimulation games) over such classes and provide bisimulation preserving model constructions within these classes.
  • Keywords
    bisimulation equivalence; game theory; Benthem theorem; bisimulation invariance; first-order formula; frame classes; game-based analysis; modal characterisation theorem; modal logic; Computer science; Laboratories; Logic;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Logic in Computer Science, 2005. LICS 2005. Proceedings. 20th Annual IEEE Symposium on
  • ISSN
    1043-6871
  • Print_ISBN
    0-7695-2266-1
  • Type

    conf

  • DOI
    10.1109/LICS.2005.27
  • Filename
    1509206