License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2017.38
URN: urn:nbn:de:0030-drops-76926
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2017/7692/
Go to the corresponding LIPIcs Volume Portal

Gouveia, Maria João ; Santocanale, Luigi

Aleph1 and the Modal mu-Calculus

pdf-format:
LIPIcs-CSL-2017-38.pdf (0.7 MB)

Abstract

For a regular cardinal kappa, a formula of the modal mu-calculus is kappa-continuous in a variable x if, on every model, its interpretation as a unary function of x is monotone and preserves unions of kappa-directed sets. We define the fragment C1 (x) of the modal mu-calculus and prove that all the formulas in this fragment are aleph_1-continuous. For each formula phi(x) of the modal mu-calculus, we construct a formula psi(x) in C1 (x) such that phi(x) is kappa-continuous, for some kappa, if and only if psi(x) is equivalent to phi(x). Consequently, we prove that (i) the problem whether a formula is kappa-continuous for some kappa is decidable, (ii) up to equivalence, there are only two fragments determined by continuity at some regular cardinal: the fragment C0(x) studied by Fontaine and the fragment C1 (x). We apply our considerations to the problem of characterizing closure ordinals of formulas of the modal mu-calculus. An ordinal alpha is the closure ordinal of a formula phi(x) if its interpretation on every model converges to its least fixed-point in at most alpha steps and if there is a model where the convergence occurs exactly in alpha steps. We prove that omega_1, the least uncountable ordinal, is such a closure ordinal. Moreover we prove that closure ordinals are closed under ordinal sum. Thus, any formal expression built from 0, 1, omega, omega_1 by using the binary operator symbol + gives rise to a closure ordinal.

BibTeX - Entry

@InProceedings{gouveia_et_al:LIPIcs:2017:7692,
  author =	{Maria Jo{\~a}o Gouveia and Luigi Santocanale},
  title =	{{Aleph1 and the Modal mu-Calculus}},
  booktitle =	{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
  pages =	{38:1--38:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-045-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{82},
  editor =	{Valentin Goranko and Mads Dam},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2017/7692},
  URN =		{urn:nbn:de:0030-drops-76926},
  doi =		{10.4230/LIPIcs.CSL.2017.38},
  annote =	{Keywords: Modal mu-calculus, regular cardinal, continuous function, aleph1, omega1, closure ordinal, ordinal sum}
}

Keywords: Modal mu-calculus, regular cardinal, continuous function, aleph1, omega1, closure ordinal, ordinal sum
Collection: 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)
Issue Date: 2017
Date of publication: 16.08.2017

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI