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 :
بازگشت