The Limit of Recursion in State-based Systems

TL;DR

This paper establishes that omega^2 is the strict upper bound on the number of iterations needed for certain fixed points in countable structures, refining previous results on the mu-calculus closure ordinals.

Contribution

It introduces a new approach using conservative well-annotations to precisely determine the closure ordinal bounds for modal definable functions.

Findings

Omega^2 bounds the iteration count for fixed points in countable structures.

The method refines previous bounds on mu-calculus closure ordinals.

A new theory of conservative well-annotations is developed.

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.