The Limit of Recursion in State-based Systems
Giacomo Barlucchi, FLoV
We prove that ω2 strictly bounds the iterations required for modal definable functions to reach a fixed point across all countable structures. In doing so, we both extend and correct the previously claimed result on closure ordinals of the alternation-free μ-calculus. The new approach sees a reincarnation of Kozen’s well-annotations, originally devised for showing the finite model property for the modal μ-calculus. We develop a theory of conservative well-annotations where minimality of the annotation is guaranteed, and isolate relevant parts of the structure that necessitate an unfolding of fixed points. This adoption of well-annotations enables a direct and clear pumping process that rules out closure ordinals between ω2 and the limit of countability.