  This paper studies the logical properties of a very general class of infinite
ranked trees, namely those generated by higher-order recursion schemes. We
consider, for both monadic second-order logic and modal mu-calculus, three main
problems: model-checking, logical reflection (aka global model-checking, that
asks for a finite description of the set of elements for which a formula holds)
and selection (that asks, if exists, for some finite description of a set of
elements for which an MSO formula with a second-order free variable holds). For
each of these problems we provide an effective solution. This is obtained
thanks to a known connection between higher-order recursion schemes and
collapsible pushdown automata and on previous work regarding parity games
played on transition graphs of collapsible pushdown automata.
