Justifying induction on modal μ-formulae

We define a rank function for formulae of the propositional modal μ-calculus such that the rank of a fixed point is strictly bigger than the rank of any of its finite approximations. A rank function of this kind is needed, for instance, to establish the collapse of the modal μ-hierarchy over transitive transition systems. We show that the range of the rank function is ωω. Further we establish that the rank is computable by primitive recursion, which gives us a uniform method to generate formulae of arbitrary rank below ωω.