The Limit of Recursion in State-based Systems
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866912687620882432 |
|---|---|
| author | Afshari, Bahareh Barlucchi, Giacomo Leigh, Graham E. |
| author_facet | Afshari, Bahareh Barlucchi, Giacomo Leigh, Graham E. |
| contents | 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.
|
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2511_02594 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | The Limit of Recursion in State-based Systems Afshari, Bahareh Barlucchi, Giacomo Leigh, Graham E. Logic in Computer Science F.4.1 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. |
| title | The Limit of Recursion in State-based Systems |
| topic | Logic in Computer Science F.4.1 |
| url | https://arxiv.org/abs/2511.02594 |