Logic in Computer Science (LICS 2005)

Paper: Modal Characterisation Theorems over Special Classes of Frames (at LICS 2005)

Authors: Anuj Dawar Martin Otto

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-Fraýssé versus bisimulation games) over such classes and provide bisimulation preserving model constructions within these classes.

BibTeX

  @InProceedings{DawarOtto-ModalCharacterisati,
    author = 	 {Anuj Dawar and Martin Otto},
    title = 	 {Modal Characterisation Theorems over Special Classes of Frames},
    booktitle =  {Proceedings of the Twentieth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2005},
    year =	 2005,
    editor =	 {Prakash Panangaden},
    month =	 {June}, 
    pages =      {21--30},
    location =   {Chicago, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }