Higher-order recursion schemes are an expressive formalism used to define languages of possibly infinite ranked trees. They extend regular and context-free grammars, and are equivalent to simply typed λY-calculus and collapsible pushdown automata. In this work we prove, under a syntactical constraint called safety, decidability of the model-checking problem for recursion schemes against properties defined by alternating B-automata, an extension of alternating parity automata for infinite trees with a boundedness acceptance condition. We then exploit this result to show how to compute downward closures of languages of finite trees recognized by safe recursion schemes.
@InProceedings{barozzini_et_al:LIPIcs.ICALP.2020.109, author = {Barozzini, David and Clemente, Lorenzo and Colcombet, Thomas and Parys, Pawe{\l}}, title = {{Cost Automata, Safe Schemes, and Downward Closures}}, booktitle = {47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)}, pages = {109:1--109:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-138-2}, ISSN = {1868-8969}, year = {2020}, volume = {168}, editor = {Czumaj, Artur and Dawar, Anuj and Merelli, Emanuela}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2020.109}, URN = {urn:nbn:de:0030-drops-125169}, doi = {10.4230/LIPIcs.ICALP.2020.109}, annote = {Keywords: Cost logics, cost automata, downward closures, higher-order recursion schemes, safe recursion schemes} }
Feedback for Dagstuhl Publishing