The Rabin tree theorem yields an algorithm to solve the satisfiability problem for monadic second-order logic over infinite trees. Here we solve the probabilistic variant of this problem. Namely, we show how to compute the probability that a randomly chosen tree satisfies a given formula. We additionally show that this probability is an algebraic number. This closes a line of research where similar results were shown for formalisms weaker than the full monadic second-order logic.

翻译：拉宾树定理给出了在无限树上的一元二阶逻辑可满足性问题的算法。本文解决了该问题的概率变体。具体而言，我们展示了如何计算随机选择的树满足给定公式的概率。此外，我们证明该概率是一个代数数。这终结了一条研究路线，此前已有类似结果针对比完整一元二阶逻辑更弱的形式体系得到证明。