Modal characterisation theorems over special classes of frames.

*(English)*Zbl 1185.03027The 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.

Reviewer: Valentin F. Goranko (Johannesburg)

##### MSC:

03B45 | Modal logic (including the logic of norms) |

03C13 | Model theory of finite structures |

03C40 | Interpolation, preservation, definability |

PDF
BibTeX
XML
Cite

\textit{A. Dawar} and \textit{M. Otto}, Ann. Pure Appl. Logic 161, No. 1, 1--42 (2009; Zbl 1185.03027)

Full Text:
DOI

##### References:

[1] | L. Alberucci, A. Facchini, The modal \(\mu\)-calculus hierarchy over restricted classes of transition systems. The Journal of Symbolic Logic (in press) · Zbl 1191.03012 |

[2] | Andréka, H.; van Benthem, J.; Németi, I., Modal languages and bounded fragments of predicate logic, Journal of philosophical logic, 27, 217-274, (1998) · Zbl 0919.03013 |

[3] | Blackburn, P.; de Rijke, M.; Venema, Y., () |

[4] | G. D’Agostino, G. Lenzi, On the \(\mu\)-calculus over transitive and finite transitive frames, Preprint, 2008 |

[5] | A. Dawar, M. Otto, Modal characterisation theorems over special classes of frames, in: Proceedings of 20th IEEE Symposium on Logic in Computer Science, LICS’05, 2005, pp. 21-30 · Zbl 1185.03027 |

[6] | Ebbinghaus, H.-D.; Flum, J., Finite model theory, (1999), Springer |

[7] | Ebbinghaus, H.-D.; Flum, J.; Thomas, W., Mathematical logic, (1994), Springer · Zbl 0795.03001 |

[8] | Gaifman, H., On local and nonlocal properties, (), 105-135 |

[9] | Goranko, V.; Otto, M., Model theory of modal logic, (), 249-330 |

[10] | Janin, D.; Walukiewicz, I., On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic, (), 263-277 |

[11] | F. Moller, A. Rabinovich, On the expressive power of CTL*, in: Proceedings of 14th IEEE Symposium on Logic in Computer Science, LICS’99, 1999, pp. 360-369 |

[12] | M. Otto, Elementary proof of the van Benthem-Rosen characterisation theorem. Technical Report 2342, Department of Mathematics, Technische Universität Darmstadt, 2004 |

[13] | Otto, M., Modal and guarded characterisation theorems over finite transition systems, Annals of pure and applied logic, 130, 173-205, (2004) · Zbl 1056.03018 |

[14] | Rosen, E., Modal logic over finite structures, Journal of logic, language and information, 6, 427-439, (1997) · Zbl 0882.03014 |

[15] | Smorynski, C., Beth’s theorem and self-referential sentences, (), 253-260 · Zbl 0453.03018 |

[16] | B. ten Cate, G. Fontaine, T. Litak, Some modal aspects of XPath, Preprint, in: Pre-proceedings of Methods for Modalities, 2007 · Zbl 1242.68010 |

[17] | J. van Benthem, Modal Logic and Classical Logic, Bibliopolis, Napoli, 1983 |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.