Oxford University Computing Laboratory
4pm Tuesday 15th November 2005
Room 2511, JCMB, King's Buildings
Higher-order recursion schemes are a natural (and old) model of 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 SAFETY condition. A natural question is whether the assumption of safety is necessary. Recently two teams independently showed that the answer is no at level 2.
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 the attendant algorithmics rely crucially on game semantics.