The Limit of Recursion in State-based Systems
Bahareh Afshari, Giacomo Barlucchi, Graham E. Leigh
TL;DR
The paper addresses the problem of bounding fixed-point iterations (closure ordinals) for the Sigma-fragment of the modal $\mu$-calculus on countable structures. It introduces a refined theory of conservative well-annotations, building on Kozen's work, and a pumping argument implemented via conjunctive modal equation systems to control ordinal growth. The main result shows that the countable closure ordinals are strictly less than $\omega^2$, resolving gaps in prior proofs and providing a streamlined framework for ordinal analysis. The approach yields a robust method with potential to extend to the full calculus and to illuminate the connection between syntactic representations and semantic fixed-point behavior.
Abstract
We prove that omega^2 strictly bounds the iterations required for modal definable functions to reach a fixed point across all countable structures. The result corrects and extends the previously claimed result by the first and third authors on closure ordinals of the alternation-free mu-calculus in [3]. The new approach sees a reincarnation of Kozen's well-annotations, devised for showing the finite model property for the modal mu-calculus. We develop a theory of 'conservative' well-annotations where minimality of annotations is guaranteed, and isolate parts of the structure that locally determine the closure ordinal of relevant formulas. This adoption of well-annotations enables a direct and clear pumping process that rules out closure ordinals between omega^2 and the limit of countability.