Justifying induction on modal $μ$-formulae

TitleJustifying induction on modal $μ$-formulae
Publication TypeJournal Article
Year of Publication2014
AuthorsAlberucci, L, Krähenbühl, J, Studer, T
JournalLogic Journal of IGPL
AbstractWe define a rank function for formulae of the propositional modal $\mu$-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 $\mu$-hierarchy over transitive transition systems. We show that the range of the rank function is $\omega^\omega$. Further we establish that the rank is computable by primitive recursion, which gives us a uniform method to generate formulae of arbitrary rank below $\omega^\omega$.