概率程序的代数程序分析

以下摘要由 AI 根据胶片自动生成。

概率程序的定量推理需要统一处理概率非确定性、恶魔非确定性和抽象非确定性，但 Kleene 代数在 分支下会导致概率求和超过 1 而失效。我们提出 Markov 代数 ，程序指称构成完全偏序集，可方便地扩展更多汇聚操作，统一支持多种非确定性语义。基于最弱前期望演算，该框架可自动推断断言概率、期望值和期望时间复杂度等定量性质。