The limit of recursion in state-based systems.
Giacomo Barlucchi
Authors: Giacomo Barlucchi, Bahareh Afshari and Graham Leigh
In this talk we present a study about closure ordinals of the modal \(\mu\)-calculus, i.e., modal logic extended with least and greatest fixed point operators.
We show that \(\omega^2\) is a strict upper bound on the closure ordinals of the \(\Sigma\)-fragment of the modal \(\mu\)-calculus, i.e., formulas generated from closed \(\mu\)-calculus formulas and variables through the logical and modal operators, and the \(\mu\) operator. This reproves and extends the claims in [1] concerning closure ordinals of the alternation-free fragment. The approach presented here develops a theory of ordinal annotations based on the notion of well-annotations previously introduced by Kozen [2]. By imposing minimality on the annotating ordinals we relate well-annotations to the existence of closure ordinals. The central argument involves a pumping lemma for well-annotations. Assuming the existence of a sufficiently ‘large’ frame, repetition of annotated sets enables a transfinite series of substitutions, showing it possible to obtain a minimal well-annotation corresponding in size to an arbitrary countable ordinal, thereby refuting the existence of closure ordinals equal or greater than \(\omega^2\).
Bibliography
- Bahareh Afshari and Graham E. Leigh,On closure ordinals for the modal mu-calculus,Computer Science Logic 2013 {(CSL} 2013)(Torino, Italy),(Simona Ronchi Della Rocca, editor),vol. 23,Schloss Dagstuhl - Leibniz-Zentrum f{ü}r Informatik, 2013,pp. 30–44.
- Dexter Kozen,A Finite Model Theorem for the Propositional mu-Calculus,Studia Logica: An International Journal for Symbolic Logic,vol. 47 (1988), no. 3, pp. 233–241.