Characterization, Definability and Separation via Saturated Models

Areces, C., Carreiro, F., and Figueira, S.. 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: (download)

@ARTICLE{arec:char13,
  author = {Areces, C. and Carreiro, F. and Figueira, S.},
  title = {Characterization, Definability and Separation via Saturated Models},
  journal = {Theoretical Computer Science},
  year = {2014},
  volume = {537},
  pages = {72-86},
  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}
}

Generated by bib2html.pl (written by Patrick Riley) on Sun Oct 02, 2016 17:05:49