一句话：求解无穷树上一元二阶逻辑的概率满足问题：计算随机树满足公式的概率，并证明该概率为代数数。
本文研究 Rabin 树定理的概率变体。Rabin 树定理给出了无穷树上一元二阶逻辑（MSO）可满足性问题的判定算法；本文则考虑随机选取的无穷树满足给定 MSO 公式的概率，并给出计算该概率的方法。作者证明该概率总是一个代数数，从而将此前针对弱于完整 MSO 的形式系统所获得的结果推广到完整 MSO。该工作结束了关于更弱形式系统概率满足性的一系列研究，为无穷树上的概率逻辑提供了精确的算法与代数性质刻画。
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.
DOI 原文 ·
@inproceedings{paperbot7484,
title = {The Probabilistic Rabin Tree Theorem
<sup>*</sup>},
author = {Damian Niwiński and Paweł Parys and Michał Skrzypczak},
booktitle = {LICS},
year = {2023},
doi = {10.1109/lics56636.2023.10175800}
}