Artículo

Estamos trabajando para incorporar este artículo al repositorio
Consulte el artículo en la página del editor
Consulte la política de Acceso Abierto del editor

Abstract:

Three important results about the expressivity of a modal logic L are the Characterization Theorem (that identifies a modal logic L as a fragment of a better known logic), the Definability Theorem (that provides conditions under which a class of L-models can be defined by a formula or a set of formulas of L), and the Separation Theorem (that provides conditions under which two disjoint classes of L-models can be separated by a class definable in 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 ω-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 L, this property can be seen as a test that identifies the adequate notion of observational equivalence for a particular modal logic. © 2014 Elsevier B.V.

Registro:

Documento: Artículo
Título:Characterization, definability and separation via saturated models
Autor:Areces, C.; Carreiro, F.; Figueira, S.
Filiación:FaMAF, Universidad Nacional de Córdoba, Argentina
Institute for Logic, Language and Computation, University of Amsterdam, Netherlands
Departamento de Computación, FCEyN, Universidad de Buenos Aires, Argentina
CONICET, Argentina
Palabras clave:Characterization; Definability; Modal logics; Model theory; Saturation; Separation; Simulation; Characterization; Formal logic; Saturation (materials composition); Separation; Characterization theorems; Definability; First order logic; Modal logic; Model theory; Observational equivalences; Separation theorem; Simulation; Computer simulation
Año:2014
Volumen:537
Número:C
Página de inicio:72
Página de fin:86
DOI: http://dx.doi.org/10.1016/j.tcs.2014.02.047
Título revista:Theoretical Computer Science
Título revista abreviado:Theor Comput Sci
ISSN:03043975
CODEN:TCSCD
Registro:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03043975_v537_nC_p72_Areces

Referencias:

  • Areces, C., Hybrid logics: The old and the new (2007) Proceedings of LogKCA-07, San Sebastian, Spain, pp. 15-29. , X. Arrazola, J. Larrazabal (Eds.)
  • Areces, C., Figueira, D., Figueira, S., Mera, S., Expressive power and decidability for memory logics (2008) Lecture Notes in Comput. Sci., 5110, pp. 56-68. , Springer, Berlin/Heidelberg, Logic, Language, Information and Computation, Proceedings of WoLLIC
  • Areces, C., Figueira, D., Figueira, S., Mera, S., The expressive power of memory logics (2011) Rev. Symb. Log., 4 (2), pp. 290-318
  • Areces, C., Figueira, S., Mera, S., Completeness results for memory logics (2011) Ann. Pure Appl. Logic, 163 (7), pp. 961-972
  • Areces, C., ten Cate, B., Hybrid logics (2006) Handbook of Modal Logics, pp. 821-868. , Elsevier, P. Blackburn, F. Wolter, J. van Benthem (Eds.)
  • Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P., (2007) The Description Logic Handbook, , Cambridge University Press, New York, NY, USA
  • Blackburn, P., de Rijke, M., Venema, Y., (2001) Modal Logic, , Cambridge University Press, New York, NY, USA
  • Carreiro, F., On characterization, definability and ω-saturated models (2011) Lecture Notes in Comput. Sci., 6916, pp. 62-76. , Springer, Berlin/Heidelberg, International Colloquium on Theoretical Aspects of Computing
  • Chang, C., Keisler, H., Studies in Logic and the Foundations of Mathematics (1973) Model Theory, 73. , Elsevier Science B.V., Amsterdam, The Netherlands
  • Dawar, A., Otto, M., Modal characterisation theorems over special classes of frames (2009) Ann. Pure Appl. Logic, 161 (1), pp. 1-42
  • de Rijke, M., The modal logic of inequality (1992) J. Symbolic Logic, 57, pp. 566-584
  • de Rijke, M., (1995) Modal model theory, , Tech. rep. CS-R9517, CWI, Amsterdam
  • de Rijke, M., Sturm, H., Global definability in basic modal logic (2001) Essays on Non-Classical Logic, pp. 111-135. , World Scientific Publishers, H. Wansing (Ed.)
  • Goranko, V., Otto, M., Model theory of modal logic (2006) Handbook of Modal Logics, pp. 255-325. , Elsevier, P. Blackburn, F. Wolter, J. van Benthem (Eds.)
  • Goranko, V., Passy, S., Using the universal modality: Gains and questions (1992) J. Logic Comput., 2 (1), pp. 5-30
  • Hansen, H., (2003) Monotonic modal logics, , Master's thesis, ILLC, University of Amsterdam
  • Hollenberg, M., (1998) Logic and bisimulation, , Ph.D. thesis, Philosophical Institute, Utrecht University
  • Janin, D., Walukiewicz, I., On the expressive completeness of the propositional μ-calculus with respect to monadic second order logic (1996) Lecture Notes in Comput. Sci., 1119, pp. 263-277. , Springer, U. Montanari, V. Sassone (Eds.) CONCUR
  • Kamp, H., (1968) Tense logic and the theory of linear order, , Ph.D. thesis, University of California, Los Angeles
  • Keisler, H., The ultraproduct construction (2010) Contemp. Math., 530, pp. 163-179. , American Mathematical Society, V. Bergelson, A. Blass, M. Di Nasso, R. Jin (Eds.) Ultrafilters Across Mathematics
  • Kozen, D., Results on the propositional μ-calculus (1983) Theoret. Comput. Sci., 27 (3), pp. 333-354
  • Kurtonina, N., de Rijke, M., Bisimulations for temporal logic (1997) J. Log. Lang. Inf., 6, pp. 403-425
  • Kurtonina, N., de Rijke, M., Classifying description logics (1997) Description Logics, 410. , URA-CNRS
  • Kurtonina, N., de Rijke, M., Simulating without negation (1997) J. Logic Comput., 7, pp. 503-524
  • Kurtonina, N., de Rijke, M., Expressiveness of concept expressions in first-order description logics (1999) Artificial Intelligence, 107 (2), pp. 303-333
  • Marker, D., Model Theory: An Introduction (2002) Grad. Texts in Math., , Springer
  • Marx, M., Venema, Y., Multi-dimensional modal logic (1997) Appl. Log. Ser., 4
  • Mera, S., (2009) Modal memory logics, , Ph.D. thesis, Universidad de Buenos Aires & Université Henri Poincare, Buenos Aires, Argentina
  • Moller, F., Rabinovich, A., On the expressive power of CTL* (1999) LICS, IEEE Computer Society, pp. 360-368
  • Otto, M., Bisimulation invariance and finite models (2006) Lect. Notes Log., pp. 276-298. , ASL, Z. Chatzidakis, P. Koepke, W. Pohlers (Eds.) Logic Colloquium '02
  • Pattinson, D., Coalgebraic modal logic: Soundness, completeness and decidability of local consequence (2003) Theoret. Comput. Sci., 309 (1-3), pp. 177-193
  • Prior, A., (1967) Past, Present and Future, , Clarendon Press, Oxford
  • Prior, A., (1968) Papers on Time and Tense, , University of Oxford Press
  • Rosen, E., Modal logic over finite structures (1995) J. Log. Lang. Inf., 6, pp. 427-439
  • Schröder, L., Pattinson, D., Coalgebraic correspondence theory (2010) Lecture Notes in Comput. Sci., 6014, pp. 328-342. , Springer, L. Ong (Ed.) Proceedings of FoSSaCS 2010
  • Schröder, L., Pattinson, D., Rank-1 modal logics are coalgebraic (2010) J. Logic Comput., 20 (5), pp. 1113-1147
  • Sturm, H., (1997) Modale Fragmente von Lωω und Lω1ω, , Ph.D. thesis, CIS, University of Munich
  • van Benthem, J., (1976) Modal correspondence theory, , Ph.D. thesis, Universiteit van Amsterdam, Instituut voor Logica en Grondslagenonderzoek van Exacte Wetenschappen

Citas:

---------- APA ----------
Areces, C., Carreiro, F. & Figueira, S. (2014) . Characterization, definability and separation via saturated models. Theoretical Computer Science, 537(C), 72-86.
http://dx.doi.org/10.1016/j.tcs.2014.02.047
---------- CHICAGO ----------
Areces, C., Carreiro, F., Figueira, S. "Characterization, definability and separation via saturated models" . Theoretical Computer Science 537, no. C (2014) : 72-86.
http://dx.doi.org/10.1016/j.tcs.2014.02.047
---------- MLA ----------
Areces, C., Carreiro, F., Figueira, S. "Characterization, definability and separation via saturated models" . Theoretical Computer Science, vol. 537, no. C, 2014, pp. 72-86.
http://dx.doi.org/10.1016/j.tcs.2014.02.047
---------- VANCOUVER ----------
Areces, C., Carreiro, F., Figueira, S. Characterization, definability and separation via saturated models. Theor Comput Sci. 2014;537(C):72-86.
http://dx.doi.org/10.1016/j.tcs.2014.02.047