Affiliations: [a] Institute of Informatics, University of Warsaw, Warsaw, Poland, dbarozzini@mimuw.edu.pl
| [b] Institute of Informatics, University of Warsaw, Warsaw, Poland, clementelorenzo@gmail.com
| [c] IRIF-CNRS-Université de Paris, Paris, France, thomas.colcombet@irif.fr
| [d] Institute of Informatics, University of Warsaw, Warsaw, Poland, parys@mimuw.edu.pl
Correspondence:
[‡]
Address for correspondence: Institute of Informatics, University of Warsaw, Warsaw, Poland.
Note: [*] Author supported by the National Science Centre, Poland (grant no. 2016/22/E/ST6/00041).
Note: [†] Author supported by the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No.670624), and the DeLTA ANR project (ANR-16-CE40-0007).
Abstract: In this work we prove decidability of the model-checking problem for safe recursion schemes against properties defined by alternating B-automata. We then exploit this result to show how to compute downward closures of languages of finite trees recognized by safe recursion schemes. Higher-order recursion schemes are an expressive formalism used to define languages of finite and infinite ranked trees by means of fixed points of lambda terms. They extend regular and context-free grammars, and are equivalent in expressive power to the simply typed λY-calculus and collapsible pushdown automata. Safety in a syntactic restriction which limits their expressive power. The class of alternating B-automata is an extension of alternating parity automata over infinite trees; it enhances them with counting features that can be used to describe boundedness properties.
