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
Volume22
Pagination805-817
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$.
URLhttp://www.iam.unibe.ch/ltgpub/2014/aks14.pdf
DOI10.1093/jigpal/jzu001