Higher-order recursive schemes are a natural (and old) model of functional programs. They define a family of finitely branching infinite (term-)trees, which forms an infinite hierarchy according to their type-theoretic level.

Building on the famous work of Rabin 1969 and others, Knapik et al. (FOSSACS 2002) proved that the MSO theories of all such trees are decidable, provided the generating recursion scheme satisfies a syntactic constraint called SAFETY, which is an awkward condition.

We prove that

(i) The modal mu-calculus model checking problem for trees generated by level-n recursion schemes is n-EXPTIME complete, for all n >= 1.

(ii) Hence trees generated by recursion schemes of every level, whether safe or not, have decidable MSO theories.

In this talk, we survey the area, explain the result, and sketch a game-semantic proof.