一句话：引入带天使非确定性的概率 Kleene 代数与自动机，以多重集分布语义克服单子分配律障碍，并证明 Kleene 定理。
论文研究概率 Kleene 代数中引入天使非确定性（angelic nondeterminism）的问题。由于幂集单子与 Giry 单子之间不存在分配律，直接组合非确定性与概率选择会遇到理论障碍。作者转而采用多重集上的分布作为语义载体，定义相应自动机类，并给出操作语义与指称语义。进一步建立余代数理论，得到完整的 Kleene 定理，以及等式推理原则。该工作将 Kleene 代数、自动机、余代数与概率语义统一在一个框架中，为带概率与天使选择的程序/系统推理提供了代数与语义基础。
We introduce a version of probabilistic Kleene algebra with angelic nondeterminism and a corresponding class of automata. Our approach implements semantics via distributions over multisets in order to overcome theoretical barriers arising from the lack of a distributive law between the powerset and Giry monads. We produce a full Kleene theorem and a coalgebraic theory, as well as both operational and denotational semantics and equational reasoning principles.
@article{paperbot3122,
title = {Probabilistic Kleene Algebra with Angelic Nondeterminism},
author = {Shawn Ong and Stephanie Ma and Dexter Kozen},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {PLDI},
year = {2025},
doi = {10.1145/3729286}
}