文章基本信息

标题：Cost Automata, Safe Schemes, and Downward Closures
本地全文：下载
作者：David Barozzini ; Lorenzo Clemente ; Thomas Colcombet 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2020
卷号：168
页码：109:1-109:18
DOI：10.4230/LIPIcs.ICALP.2020.109
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：Cost logics; cost automata; downward closures; higher-order recursion schemes; safe recursion schemes