Maria João Gouveia ; Luigi Santocanale - 1 and the modal μ-calculus

lmcs:4356 - Logical Methods in Computer Science, October 15, 2019, Volume 15, Issue 4 - https://doi.org/10.23638/LMCS-15(4:1)2019
1 and the modal μ-calculusArticle

Authors: Maria João Gouveia ; Luigi Santocanale

    For a regular cardinal κ, a formula of the modal μ-calculus is κ-continuous in a variable x if, on every model, its interpretation as a unary function of x is monotone and preserves unions of κ-directed sets. We define the fragment C1(x) of the modal μ-calculus and prove that all the formulas in this fragment are 1-continuous. For each formula ϕ(x) of the modal μ-calculus, we construct a formula ψ(x)C1(x) such that ϕ(x) is κ-continuous, for some κ, if and only if ϕ(x) is equivalent to ψ(x). Consequently, we prove that (i) the problem whether a formula is κ-continuous for some κ 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 μ-calculus. An ordinal α is the closure ordinal of a formula ϕ(x) if its interpretation on every model converges to its least fixed-point in at most α steps and if there is a model where the convergence occurs exactly in α steps. We prove that ω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, ω, ω1 by using the binary operator symbol + gives rise to a closure ordinal.


    Volume: Volume 15, Issue 4
    Published on: October 15, 2019
    Accepted on: August 5, 2019
    Submitted on: March 9, 2018
    Keywords: Computer Science - Logic in Computer Science,Mathematics - Logic,03D70, 03B45, 03B70,F.4.1
    Funding:
      Source : OpenAIRE Graph
    • Research Project; Code: SFRH/BSAB/128039/2016

    1 Document citing this article

    Consultation statistics

    This page has been seen 2193 times.
    This article's PDF has been downloaded 407 times.