2026-07-25T12:08:01Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:12516 2024-03-06T10:50:20Z ddc:004 open_access

Cost Automata, Safe Schemes, and Downward Closures Barozzini, David Clemente, Lorenzo Colcombet, Thomas Parys, Paweł Cost logics cost automata downward closures higher-order recursion schemes safe recursion schemes 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik David Barozzini and Lorenzo Clemente and Thomas Colcombet and Paweł Parys 2020 Is Part Of LIPIcs, Volume 168, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ICALP.2020.109 urn:nbn:de:0030-drops-125169 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2020.109 eng https://creativecommons.org/licenses/by/3.0/legalcode