Cost Automata, Safe Schemes, and Downward Closures

In this work we prove decidability of the model-checking problem for saferecursion schemes against properties defined by alternating B-automata. We thenexploit this result to show how to compute downward closures of languages offinite trees recognized by safe recursion schemes. Higher-order recursion schemes are an expressive formalism used to definelanguages of finite and infinite ranked trees by means of fixed points oflambda terms. They extend regular and context-free grammars, and are equivalentin expressive power to the simply typed $\lambda Y$-calculus and collapsiblepushdown automata. Safety in a syntactic restriction which limits theirexpressive power. The class of alternating B-automata is an extension of alternating parityautomata over infinite trees; it enhances them with counting features that canbe used to describe boundedness properties