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 {\mu}-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.

翻译：一元二阶逻辑（MSO）通过引入取值于集合的变量及对这些变量的量化，扩展了一阶逻辑（FO）。本文提出并研究一元树逻辑（MTL），它是MSO在无穷树模型上定义的一个子片段，其中变量所遍历的集合为原模型中的任意子树。我们分析了MTL与MSO及MPL变体（即带路径量化的MSO）在表达能力上的比较。此外，我们还讨论了与时间逻辑的联系，具体表现为将分级μ演算中的非平凡片段嵌入MTL，并证明MTL足以编码用于推理具有FO可定义目标策略的时间逻辑。