Modal characterisation theorems over special classes of frames
type: Item
instance of: scholarly article
title: Modal characterisation theorems over special classes of frames
zbMATH Open document ID: 1185.03027
author: Anuj Dawar
author: Martin Otto
published in: Annals of Pure and Applied Logic
publication date: 2009-10-09T00:00:00Z
review text: The paper investigates model-theoretic characterisations of the expressive power of modal logics in terms of bisimulation invariance on specific classes of structures, analogous to van Benthem's theorem saying that a first-order formula is invariant under bisimulation if, and only if, it is equivalent to a formula of basic modal logic. In particular, the authors study 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 frames, finite rooted frames, finite transitive frames, well-founded transitive frames, finite equivalence frames -- as these are not elementary. Instead, the authors 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. Over most of the classes considered, they obtain finite model theory analogues of the classically expected characterisations, with new proofs also for the classical setting. The class of transitive frames is a notable exception, with a marked difference between the classical and the finite model theory of bisimulation-invariant first-order properties. Over the class of all finite transitive frames in particular, it turns out that monadic second-order logic is no more expressive than first-order logic as far as bisimulation-invariant properties are concerned. The authors obtain ramifications of the de Jongh-Sambin theorem and a new and specific analogue of the Janin-Walukiewicz characterisation of bisimulation-invariant monadic second-order logic for finite transitive frames.
reviewed by: Valentin Goranko
Mathematics Subject Classification ID: 03B45
Mathematics Subject Classification ID: 03C13
Mathematics Subject Classification ID: 03C40
zbMATH DE Number: 5612542
zbMATH Keywords: modal logic
zbMATH Keywords: finite model theory
zbMATH Keywords: bisimulation
zbMATH Keywords: preservation
zbMATH Keywords: expressive completeness
MaRDI profile type: Publication
full work available at URL: j.apal.2009.04.002
OpenAlex ID: W2029611280
Wikidata QID: Q58215565
cites work: The modalμ-calculus hierarchy over restricted classes of transition systems
cites work: Modal languages and bounded fragments of predicate logic
cites work: Modal logic
cites work: Q4255575
cites work: Q4298571
cites work: Q3666827
cites work: On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic
cites work: Modal and guarded characterisation theorems over finite transition systems
cites work: Modal logic over finite structures
cites work: Q3900021
cites work: Some modal aspects of XPath
DOI: 10.1016/J.APAL.2009.04.002
description: scientific article; zbMATH DE number 5612542