Title :
Modal characterisation theorems over special classes of frames
Author :
Dawar, Anuj ; Otto, Martin
Author_Institution :
Comput. Lab., Cambridge Univ., UK
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;
Conference_Titel :
Logic in Computer Science, 2005. LICS 2005. Proceedings. 20th Annual IEEE Symposium on
Print_ISBN :
0-7695-2266-1
DOI :
10.1109/LICS.2005.27