下推图推广的一阶模型检验
First-Order Model Checking on Generalisations of Pushdown Graphs
摘要：
我们研究了两种推广的下推图的一阶模型检验问题。第一类是嵌套下推树类。另一类是可折叠下推图。我们的主要结果如下。可达的一阶逻辑在嵌套下推树上是一致可判定的。考虑无可达性的一阶逻辑，证明了在线性多个交替的双指数交替时间中的可判定性。具有正则可达谓词的一阶逻辑在2级可折叠下推图上是一致可判定的。此外，嵌套下推树是一阶可解释的可折叠下推图的水平2。这种解释可以扩展到可折叠下推图层次结构中的高阶嵌套下推树类的解释。我们证明了这个新的层次结构的嵌套树的第二层具有可判定的一阶模型检测。我们的可折叠下推图的可判定性结果依赖于这样一个事实，即2级可折叠下推图是均匀树自动的。我们的最后一个结果涉及一般的树自动结构。证明了Ramsey量词扩展的一阶逻辑在所有树自动结构上都是可判定的。
英文摘要：
We study the first-order model checking problem on two generalisations of pushdown graphs. The first class is the class of nested pushdown trees. The other is the class of collapsible pushdown graphs. Our main results are the following. First-order logic with reachability is uniformly decidable on nested pushdown trees. Considering first-order logic without reachability, we prove decidability in doubly exponential alternating time with linearly many alternations. First-order logic with regular reachability predicates is uniformly decidable on level 2 collapsible pushdown graphs. Moreover, nested pushdown trees are first-order interpretable in collapsible pushdown graphs of level 2. This interpretation can be extended to an interpretation of the class of higher-order nested pushdown trees in the collapsible pushdown graph hierarchy. We prove that the second level of this new hierarchy of nested trees has decidable first-order model checking. Our decidability result for collapsible pushdown graph relies on the fact that level 2 collapsible pushdown graphs are uniform tree-automatic. Our last result concerns tree-automatic structures in general. We prove that first-order logic extended by Ramsey quantifiers is decidable on all tree-automatic structures.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
