Higher-order Recursion Schemes and Collapsible Pushdown Automata: Logical Properties
Higher-order Recursion Schemes and Collapsible Pushdown Automata: Logical Properties
复制标题
高阶递归方案和可折叠下推自动机：逻辑属性
DOI：
10.1145/3452917
复制
发表时间：
2021
影响因子：
0.5
通讯作者：
Broadbent C
中科院分区：
文献类型：
--
作者：
Broadbent C
本文研究一类非常普遍的无限排名树的逻辑属性，即由高阶递归方案生成的树。我们认为，一元二阶逻辑和模态<？TeX $\mu$？>-微积分，三个主要问题：模型检查，逻辑反射（a.k.a.全局模型检查，要求公式成立的元素集的有限描述），以及选择（如果存在，要求具有二阶自由变量的MSO公式成立的元素集的有限描述）。对于每一个问题，我们都提供了有效的解决方案。这是获得，由于一个已知的高阶递归方案和可折叠的下推自动机之间的连接，并在以前的工作有关奇偶校验游戏上的过渡图的可折叠的下推自动机。
This article studies the logical properties of a very general class of infinite ranked trees, namely, those generated by higher-order recursion schemes. We consider, for both monadic second-order logic and modal <?TeX $\mu$?>-calculus, three main problems: model-checking, logical reflection (a.k.a. global model-checking, that asks for a finite description of the set of elements for which a formula holds), and selection (that asks, if exists, for some finite description of a set of elements for which an MSO formula with a second-order free variable holds). For each of these problems, we provide an effective solution. This is obtained, thanks to a known connection between higher-order recursion schemes and collapsible pushdown automata and on previous work regarding parity games played on transition graphs of collapsible pushdown automata.