Algorithmic Model Theory

Model Theory of Modal Logics over Special Frames

Modal logics occur as restricted fragments of first-order logic that combine very good model theoretic and algorithmic properties with an expressiveness that ideally suits typical applications in, for instance, knowledge representation, temporal specification, analysis of multi-agent systems and games [GO06]. It would often be natural to consider classes of structures with special requirements on the underlying frames, which cannot be dealt with easily unless the relevant constraints are first-order definable. Examples of interesting non-elementary frame classes include the class of finite frames or classes of rooted transitive frames. Expressive completeness of suitable modal logics for the class of all bisimulation invariant first-order properties relative to such restricted classes can be shown with specially adapted techniques that combine the analysis of the bisimulation game with bisimulation respecting model transformations. In [DO09], we develop a variety of new results along these lines. Among these is the emergence of a novel modality that is necessary for expressive completeness over transitive frames without strict infinite paths but not bisimulation safe over the class of all frames. Further generalisations of the proof techniques used here show that over various classes of transitive frames without infinite strict paths, monadic second-order logic is no more expressive than first-order logic as far as bisimulation invariant properties are concerned. These results lead to ramifications of a classical theorem of de Jongh and Sambin in modal logic. [O04, DO05].

Bibliography

[GO06] V. Goranko and M. Otto, Model Theory of Modal Logics,
in: Handbook of Modal Logic, edited by P. Blackburn, F. Wolter, and J. van Benthem, Elsevier 2006, pp. 255-325.
BibTeX entry

[DO09] A. Dawar and M. Otto, Modal Characterisation Theorems over Special Classes of Frames,
Annals of Pure and Applied Logic, volume 161, 2009, pp.~1-42. Abstract
BibTeX entry

[O04] M. Otto, Modal and Guarded Characterisation Theorems over Finite Transition Systems,
Annals of Pure and Applied Logic, volume 130, 2004, pp.~173-205. Abstract
BibTeX entry

[DO05] A. Dawar and M. Otto, Modal Characterisation Theorems over Special Classes of Frames, Proceedings of 20th IEEE Symposium on Logic in Computer Science LICS 2005, pp 21-30.
Abstract BibTeX entry

 

A A A | Print Print | Impressum Legal note | Contact Contact
    zum Seitenanfangzum Seitenanfang