부산대학교 도서관

Summary: ``This article studies the logical properties of a verygeneral class of infinite ranked trees, namely, those generated byhigher-order recursion schemes. We consider, for both monadicsecond-order logic and modal $\mu$-calculus, three main problems:model-checking, logical reflection (a.k.a. global model-checking, thatasks for a finite description of the set of elements for which aformula holds), and selection (that asks, if exists, for some finitedescription of a set of elements for which an MSO formula with asecond-order free variable holds). For each of these problems, weprovide an effective solution. This is obtained, thanks to a knownconnection between higher-order recursion schemes and collapsiblepushdown automata and on previous work regarding parity games played ontransition graphs of collapsible pushdown automata.''