@article{BarozziniClementeColcomberParys:FI:2023,
    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 {$\lambda$}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.},
    Author = {Barozzini, David and Clemente, Lorenzo and Colcombet, Thomas and Parys, Pawe{{\l}}},
    File = {Cost Automata, Safe Schemes, and Downward Closures - 2004.12187 - b.pdf},
    ISBN = {1875-8681},
    Journal = {Fundamenta Informaticae},
    Keywords = {Cost logics; cost automata; downward closures; higher-order recursion schemes; safe recursion schemes},
    Number = {3},
    Pages = {127--178},
    Publisher = {IOS Press},
    Title = {Cost Automata, Safe Schemes, and Downward Closures},
    Volume = {188},
    Year = {2022},
    bdsk-url-1 = {https://doi.org/10.3233/FI-222145},
    date-added = {2023-04-18 06:37:29 +0200},
    date-modified = {2023-05-24 12:25:30 +0200},
    doi = {10.3233/FI-222145}
}

@article{BarozziniClementeColcomberParys:FI:2023, 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 {$\lambda$}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.}, Author = {Barozzini, David and Clemente, Lorenzo and Colcombet, Thomas and Parys, Pawe{{\l}}}, File = {Cost Automata, Safe Schemes, and Downward Closures - 2004.12187 - b.pdf}, ISBN = {1875-8681}, Journal = {Fundamenta Informaticae}, Keywords = {Cost logics; cost automata; downward closures; higher-order recursion schemes; safe recursion schemes}, Number = {3}, Pages = {127--178}, Publisher = {IOS Press}, Title = {Cost Automata, Safe Schemes, and Downward Closures}, Volume = {188}, Year = {2022}, bdsk-url-1 = {https://doi.org/10.3233/FI-222145}, date-added = {2023-04-18 06:37:29 +0200}, date-modified = {2023-05-24 12:25:30 +0200}, doi = {10.3233/FI-222145} }