一句话：提出单子树逻辑 MTL，在无限树上对任意子树进行二阶量化，刻画其表达能力并联系分级 µ-演算与策略时序逻辑。
单子二阶逻辑（MSO）在集合变量上允许二阶量化。本文定义并研究单子树逻辑（MTL），它是 MSO 在无限树模型上的一个片段，其中集合变量被解释为原模型的任意子树。论文比较 MTL 与 MSO 的若干变体以及路径量化逻辑 MPL 的表达能力，并刻画面向无限树的集合量化能表达哪些性质。结果方面，作者给出可嵌入 MTL 的非平凡分级 µ-演算片段，并证明 MTL 足以编码用于推理策略的时序逻辑，且这些策略的目标可由一阶逻辑定义。该工作将树上的 MSO 量化、时序逻辑与策略推理联系起来，为分析无限树模型上的逻辑表达力提供了新视角。
Monadic Second-Order Logic (MSO) extends First-Order Logic (FO) with variables ranging over sets and quantifications over those variables. We introduce and study Monadic Tree Logic (MTL), a fragment of MSO interpreted on infinite-tree models, where the sets over which the variables range are arbitrary subtrees of the original model. We analyse the expressiveness of MTL compared with variants of MSO and MPL, namely MSO with quantifications over paths. We also discuss the connections with temporal logics, by providing non-trivial fragments of the Graded µ-CALCULUS that can be embedded into MTL and by showing that MTL is enough to encode temporal logics for reasoning about strategies with FO-definable goals.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@inproceedings{abs-2304-11613,
title = {Quantifying Over Trees in Monadic Second-Order Logic},
author = {Massimo Benerecetti and Laura Bozzelli and Fabio Mogavero and Adriano Peron},
booktitle = {LICS},
year = {2023},
doi = {10.1109/lics56636.2023.10175832}
}