Modal characterisation theorems over special classes of frames (Q732052)

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.