Characterization, Definability and Separation via Saturated Models

C. Areces, F. Carreiro, and S. Figueira. Characterization, Definability and Separation via Saturated Models. Theoretical Computer Science, 537:72–86, 2014.

Download

[pdf] 

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). In this article 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 constrains 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. As 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.

BibTeX

@Article{Areces2014b,
  author =       "C. Areces and F. Carreiro and S. Figueira",
  journal =      "Theoretical Computer Science",
  title =        "Characterization, Definability and Separation via
                 Saturated Models",
  year =         "2014",
  pages =        "72--86",
  volume =       "537",
  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). In this article 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 constrains 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. As 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.",
  owner =        "areces",
  timestamp =    "2013.04.11",
}