一句话：提出 Demonic Outcome Logic，统一推理同时含随机选择与恶魔非确定性的程序，并支持循环终止与结果分布量化。
密码学与机器学习等应用常使用随机化，但程序还可能同时包含非确定性（用于并发、效率或算法设计），现有随机程序分析难以覆盖二者交织的情形。本文提出 Demonic Outcome Logic，用于推理同时利用随机化和恶魔非确定性的程序。该逻辑支持并行分析多次执行，并可用等式定律操作前后条件，包括概率选择对非确定性选择的分配律；其循环规则能由单一前提同时证明终止并量化最终结果的分布。作者通过 Monty Hall、对抗性公平硬币模拟协议以及基于启发式的概率 SAT 求解器等案例展示推理能力。
Programs increasingly rely on randomization in applications such as cryptography and machine learning. Analyzing randomized programs has been a fruitful research direction, but there is a gap when programs also exploit nondeterminism(for concurrency, efficiency, or algorithmic design). In this paper, we introduce Demonic Outcome Logic for reasoning about programs that exploit both randomization and nondeterminism. The logic includes several novel features, such as reasoning about multiple executions in tandem and manipulating pre- and postconditions using familiar equational laws—including the distributive law of probabilistic choices over nondeterministic ones. We also give rules for loops that both establish termination and quantify the distribution of final outcomes from a single premise. We illustrate the reasoning capabilities of Demonic Outcome Logic through several case studies, including the Monty Hall problem, an adversarial protocol for simulating fair coins, and a heuristic based probabilistic SAT solver.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2410-22540,
title = {A Demonic Outcome Logic for Randomized Nondeterminism},
author = {Noam Zilberstein and Dexter Kozen and Alexandra Silva and Joseph Tassarotti},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {POPL},
year = {2025},
doi = {10.1145/3704855}
}