×

zbMATH — the first resource for mathematics

Characterization, definability and separation via saturated models. (English) Zbl 1323.03016
Summary: Three important results about the expressivity of a modal logic \(\mathfrak L\) are the Characterization Theorem (that identifies a modal logic \(\mathfrak L\) as a fragment of a better known logic), the Definability Theorem (that provides conditions under which a class of \(\mathfrak L\)-models can be defined by a formula or a set of formulas of \(\mathfrak L\)), and the Separation Theorem (that provides conditions under which two disjoint classes of \(\mathfrak L\)-models can be separated by a class definable in \(\mathfrak L\)).
We provide general conditions under which these results can be established for a given choice of model class and modal language whose expressivity is below first order logic. Besides some basic constraints that most modal logics easily satisfy, the fundamental condition that we require is that the class of \(\omega\)-saturated models in question has the Hennessy-Milner property with respect to the notion of observational equivalence under consideration. Given that the Characterization, Definability and Separation theorems are among the cornerstones in the model theory of \(\mathfrak L\), this property can be seen as a test that identifies the adequate notion of observational equivalence for a particular modal logic.

MSC:
03B45 Modal logic (including the logic of norms)
03C50 Models with special properties (saturated, rigid, etc.)
03C45 Classification theory, stability and related concepts in model theory
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Areces, C., Hybrid logics: the old and the new, (Arrazola, X.; Larrazabal, J., Proceedings of LogKCA-07, San Sebastian, Spain, (2007)), 15-29
[2] Areces, C.; Figueira, D.; Figueira, S.; Mera, S., Expressive power and decidability for memory logics, (Logic, Language, Information and Computation, Proceedings of WoLLIC, Edinburgh, Scotland, 2008, Lecture Notes in Comput. Sci., vol. 5110, (2008), Springer Berlin/Heidelberg), 56-68 · Zbl 1156.03029
[3] Areces, C.; Figueira, D.; Figueira, S.; Mera, S., The expressive power of memory logics, Rev. Symb. Log., 4, 2, 290-318, (2011) · Zbl 1247.03027
[4] Areces, C.; Figueira, S.; Mera, S., Completeness results for memory logics, Ann. Pure Appl. Logic, 163, 7, 961-972, (2011) · Zbl 1245.03023
[5] Areces, C.; ten Cate, B., Hybrid logics, (Blackburn, P.; Wolter, F.; van Benthem, J., Handbook of Modal Logics, (2006), Elsevier), 821-868
[6] Baader, F.; Calvanese, D.; McGuinness, D.; Nardi, D.; Patel-Schneider, P., The description logic handbook, (2007), Cambridge University Press New York, NY, USA · Zbl 1132.68055
[7] Blackburn, P.; de Rijke, M.; Venema, Y., Modal logic, (2001), Cambridge University Press New York, NY, USA · Zbl 0988.03006
[8] Carreiro, F., On characterization, definability and ω-saturated models, (International Colloquium on Theoretical Aspects of Computing, Lecture Notes in Comput. Sci., vol. 6916, (2011), Springer Berlin/Heidelberg), 62-76 · Zbl 1351.03011
[9] Chang, C.; Keisler, H., Studies in logic and the foundations of mathematics, Model Theory, vol. 73, (1973), Elsevier Science B.V. Amsterdam, The Netherlands
[10] Dawar, A.; Otto, M., Modal characterisation theorems over special classes of frames, Ann. Pure Appl. Logic, 161, 1, 1-42, (2009) · Zbl 1185.03027
[11] de Rijke, M., The modal logic of inequality, J. Symbolic Logic, 57, 566-584, (1992) · Zbl 0788.03019
[12] de Rijke, M., Modal model theory, (1995), CWI Amsterdam, Tech. rep. CS-R9517
[13] de Rijke, M.; Sturm, H., Global definability in basic modal logic, (Wansing, H., Essays on Non-Classical Logic, (2001), World Scientific Publishers), 111-135 · Zbl 0998.03014
[14] Goranko, V.; Otto, M., Model theory of modal logic, (Blackburn, P.; Wolter, F.; van Benthem, J., Handbook of Modal Logics, (2006), Elsevier), 255-325
[15] Goranko, V.; Passy, S., Using the universal modality: gains and questions, J. Logic Comput., 2, 1, 5-30, (1992) · Zbl 0774.03003
[16] Hansen, H., Monotonic modal logics, (2003), ILLC, University of Amsterdam, Master’s thesis
[17] Hollenberg, M., Logic and bisimulation, (1998), Philosophical Institute, Utrecht University, Ph.D. thesis
[18] Janin, D.; Walukiewicz, I., On the expressive completeness of the propositional μ-calculus with respect to monadic second order logic, (Montanari, U.; Sassone, V., CONCUR, Lecture Notes in Comput. Sci., vol. 1119, (1996), Springer), 263-277
[19] Kamp, H., Tense logic and the theory of linear order, (1968), University of California Los Angeles, Ph.D. thesis
[20] Keisler, H., The ultraproduct construction, (Bergelson, V.; Blass, A.; Di Nasso, M.; Jin, R., Ultrafilters Across Mathematics, Contemp. Math., vol. 530, (2010), American Mathematical Society), 163-179 · Zbl 1242.03059
[21] Kozen, D., Results on the propositional μ-calculus, Theoret. Comput. Sci., 27, 3, 333-354, (1983) · Zbl 0553.03007
[22] Kurtonina, N.; de Rijke, M., Bisimulations for temporal logic, J. Log. Lang. Inf., 6, 403-425, (1997) · Zbl 0882.03017
[23] Kurtonina, N.; de Rijke, M., Classifying description logics, (Brachman, R. J.; Donini, F. M.; Franconi, E.; Horrocks, I.; Levy, A. Y.; Rousset, M.-C., Description Logics, vol. 410, (1997), URA-CNRS)
[24] Kurtonina, N.; de Rijke, M., Simulating without negation, J. Logic Comput., 7, 503-524, (1997) · Zbl 0904.03008
[25] Kurtonina, N.; de Rijke, M., Expressiveness of concept expressions in first-order description logics, Artificial Intelligence, 107, 2, 303-333, (1999) · Zbl 0993.03042
[26] Marker, D., Model theory: an introduction, Grad. Texts in Math., (2002), Springer · Zbl 1003.03034
[27] Marx, M.; Venema, Y., Multi-dimensional modal logic, Appl. Log. Ser., 4, (1997) · Zbl 0942.03029
[28] Mera, S., Modal memory logics, (2009), Universidad de Buenos Aires & Université Henri Poincare Buenos Aires, Argentina, Ph.D. thesis
[29] Moller, F.; Rabinovich, A., On the expressive power of CTL*, (LICS, IEEE Computer Society, (1999)), 360-368
[30] Otto, M., Bisimulation invariance and finite models, (Chatzidakis, Z.; Koepke, P.; Pohlers, W., Logic Colloquium ’02, Lect. Notes Log., (2006), ASL), 276-298 · Zbl 1102.03036
[31] Pattinson, D., Coalgebraic modal logic: soundness, completeness and decidability of local consequence, Theoret. Comput. Sci., 309, 1-3, 177-193, (2003) · Zbl 1052.03009
[32] Prior, A., Past, present and future, (1967), Clarendon Press Oxford · Zbl 0169.29802
[33] Prior, A., Papers on time and tense, (1968), University of Oxford Press
[34] Rosen, E., Modal logic over finite structures, J. Log. Lang. Inf., 6, 427-439, (1995) · Zbl 0882.03014
[35] Schröder, L.; Pattinson, D., Coalgebraic correspondence theory, (Ong, L., Proceedings of FoSSaCS 2010, Lecture Notes in Comput. Sci., vol. 6014, (2010), Springer), 328-342 · Zbl 1284.03211
[36] Schröder, L.; Pattinson, D., Rank-1 modal logics are coalgebraic, J. Logic Comput., 20, 5, 1113-1147, (2010) · Zbl 1266.03032
[37] Sturm, H., Modale fragmente von \(\mathcal{L}_{\omega \omega}\) und \(\mathcal{L}_{\omega_1 \omega}\), (1997), CIS, University of Munich, Ph.D. thesis
[38] van Benthem, J., Modal correspondence theory, (1976), Universiteit van Amsterdam, Instituut voor Logica en Grondslagenonderzoek van Exacte Wetenschappen, Ph.D. thesis
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.