一句话：证明带几乎必然分支量词的 MSO+∇ 在完整二叉树上真值判定不可判定。
本文研究完整二叉树上单子二阶逻辑（MSO）的一种扩展：新增量词“几乎必然存在/每条分支 π ∈ {0,1}ω 满足公式 φ(π)”，并按 Shelah 与 Lehmann 的记号称为 MSO+∇。该逻辑由 Michalewski 和 Mio 提出，能够包含多种定性概率形式化，如定性概率检查、概率 LTL 以及带概率接受条件的奇偶树自动机。论文证明：判定给定的 MSO+∇ 句子在完整二叉树上是否为真，是不可判定的。该结果揭示了概率化 MSO 扩展在树上的表达力与判定性边界，并为相关定性概率逻辑的算法问题提供了不可判定性下界。
This paper is about an extension of monadic second-order logic over the full binary tree, which has a quantifier saying “almost surely a branch π ∈ {0,1}ωsatisfies a formula φ(π)”, This logic was introduced by Michalewski and Mio; we call it MSO+∇ following notation of Shelah and Lehmann. The logic Mso+∇ subsumes many qualitative probabilistic formalisms, including qualitative probabilistic check, probabilistic LTL, or parity tree automata with probabilistic acceptance conditions. We show that it is undecidable to check if a given sentence of MSO+∇ is true in the full binary tree11Independently and in parallel another proof of this result was given employing different techniques in [3]..
DOI 原文 ·
@inproceedings{paperbot4967,
title = {MSO+∇ is undecidable},
author = {Mikolaj Bojanczyk and Edon Kelmendi and Michal Skrzypczak},
booktitle = {LICS},
year = {2019},
doi = {10.1109/lics.2019.8785892}
}