Speaker
Giacomo Barlucchi
Gothenburg University
Talks at this conference:
Friday, 15:15, J336 
The limit of recursion in statebased systems. 
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 alternationfree fragment. The approach presented here develops a theory of ordinal annotations based on the notion of wellannotations previously introduced by Kozen [2]. By imposing minimality on the annotating ordinals we relate wellannotations to the existence of closure ordinals. The central argument involves a pumping lemma for wellannotations. 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 wellannotation corresponding in size to an arbitrary countable ordinal, thereby refuting the existence of closure ordinals equal or greater than \(\omega^2\). Bibliography
