一句话：提出概率高阶不动点逻辑 PHFL，证明其表达力与模型检测的不可判定性，并用类型系统刻画可判定片段。
本文提出概率高阶不动点逻辑 PHFL，它既是高阶不动点逻辑的概率扩展，也可视为 PCTL 与 μ^p-演算的高阶扩展。作者研究 PHFL 的表达力与模型检测问题：证明 PHFL 严格强于 μ^p-演算；即使限制为仅含 μ 算子且阶为 1 的片段，其在有限马尔可夫链上的模型检测仍不可判定。对于完整 PHFL，作者给出从 Lubarsky μ-算术到 PHFL 的翻译，由此得到模型检测的 Π^1_1-困难与 Σ^1_1-困难。正面结果方面，论文用一种新颖的类型系统刻画了 PHFL 模型检测的一个可判定片段。
We introduce PHFL, a probabilistic extension of higher-order fixpoint logic, which can also be regarded as a higher-order extension of probabilistic temporal logics such as PCTL and the $\mu^p$-calculus. We show that PHFL is strictly more expressive than the $\mu^p$-calculus, and that the PHFL model-checking problem for finite Markov chains is undecidable even for the $\mu$-only, order-1 fragment of PHFL. Furthermore the full PHFL is far more expressive: we give a translation from Lubarsky's $\mu$-arithmetic to PHFL, which implies that PHFL model checking is $\Pi^1_1$-hard and $\Sigma^1_1$-hard. As a positive result, we characterize a decidable fragment of the PHFL model-checking problems using a novel type system.
@article{paperbot1259,
title = {A Probabilistic Higher-order Fixpoint Logic},
author = {Yo Mitani and Naoki Kobayashi and Takeshi Tsukada},
journal = {Logical Methods in Computer Science},
volume = {Volume 17, Issue 4},
year = {2021},
doi = {10.46298/lmcs-17(4:15)2021}
}