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
Link To Document