Higher-order recursion schemes are a natural (and old) model of programs. They define a family of finitely branching infinite term-trees - called the VALUE trees of the recursion schemes, which forms an infinite hierarchy according to their type-theoretic level.
At level 0, these trees are just the regular trees; at level 1, they are the algebraic trees i.e. trees that are generated by deterministic pushdown automata. Building on the famous work of Rabin 1969 and others, Knapik et al. (FOSSACS 2002) proved that the monadic second-order (MSO) theories of all such trees are decidable, provided the generating recursion scheme satisfies a SAFETY condition. Is the safety assumption really necessary for the decidability result? A partial answer to the question has recently been obtained by Aehlig, de Miranda and Ong (TLCA05), and independently by Knapik, Niwinski, Urzyczyn and Walukiewicz (ICALP05). They show that all trees up to level 2, whether safe or not, have decidable MSO theories. Here we give a complete answer to the question.
We prove that:
(i) The modal mu-calculus model-checking problem for trees generated by level-n recursion schemes, whether safe or not, is n-EXPTIME complete, for every n >= 1.
(ii) Hence trees generated by recursion schemes of every finite level have decidable MSO theories.
Our approach is to transfer the algorithmic analyses from the value tree generated by a level-n recursion scheme to an auxiliary COMPUTATION tree -- which is itself a tree generated by a related level-0 recursion scheme, and then to exploit a strong correspondence between branches in the value tree and TRAVERSALS in the computation tree. Both the correspondence result and some of the attendant algorithmics are applications of game semantics.