论文标题
成本自动机，安全计划和下降
Cost Automata, Safe Schemes, and Downward Closures
论文作者
论文摘要
在这项工作中，我们证明了模型检查问题的安全递归方案对交替的b-automata定义的特性的确定性。然后，我们利用此结果来展示如何计算安全递归方案认可的有限树的语言闭合。 高阶递归方案是一种表达式形式主义，用于通过lambda术语的固定点来定义有限和无限排名树的语言。它们扩展了常规和无上下文的语法，并且在表达能力上等效于简单键入的$λy$ -calculus和Coldapsible Perfapsible Automata。在句法限制中的安全性，限制了其表达能力。 交替的b-automata类是无限树上交替自动机的延伸。它通过可用于描述界限属性的计数特征来增强它们。
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.
