The Diagonal Problem for Higher-Order Recursion Schemes is Decidable

A non-deterministic recursion scheme recognizes a language of finite trees. This very expressive model can simulate, among others, higher-order pushdown automata with collapse. We show the decidability of the diagonal problem for schemes: given a scheme G, decide whether for every n there exists a tree in the language of G that has at least n appearances of every alphabet letter. This result has several interesting consequences. In particular, it gives an algorithm to compute the downward closure of languages of words recognized by schemes. In turn, this has immediate application to separability problems and reachability analysis of concurrent systems.