  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.

Logic in Computer Science;Formal Languages and Automata Theory;Logic