一句话：提出 pcOL，首个能表达概率并发程序完整结果分布的程序逻辑，并支持几乎必然终止等推理。
概率并发程序的随机化特性使其形式推理长期落后于实践，已有程序逻辑无法刻画概率并发程序的全结果分布。本文提出概率并发结果逻辑（pcOL），将并发分离逻辑与概率分离逻辑的思想融入 Outcome Logic：分离关系被重新解释为概率独立性，从而在并发线程间组合式地描述变量的联合分布；同时基于结果推理进行情况分析，并引入条件化与不变式等组合推理原则，以精确处理依赖随机共享状态的线程。作者在多个例子中展示 pcOL 的适用性，包括证明无界循环的几乎必然终止。
Although randomization has long been used in distributed computing, formal methods for reasoning aboutprobabilistic concurrent programs have lagged behind. No existing program logics can express specificationsabout the full distributions of outcomes resulting from programs that are both probabilistic and concurrent. To address this, we introduce Probabilistic Concurrent Outcome Logic ( pcOL ), which incorporates ideas fromconcurrent and probabilistic separation logics into Outcome Logic to introduce new compositional reasoningprinciples. At its core, pcOL reinterprets the rules of Concurrent Separation Logic in a setting where separationmodels probabilistic independence, so as to compositionally describe joint distributions over variables inconcurrent threads. Reasoning about outcomes also proves crucial, as case analysis is often necessary to deriveprecise information about threads that rely on randomized shared state. We demonstrate pcOL on a variety ofexamples, including to prove almost sure termination of unbounded loops.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2411-11662,
title = {Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants},
author = {Noam Zilberstein and Alexandra Silva and Joseph Tassarotti},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776651}
}