概率性 Rely-Guarantee 演算

Jones 提出的用于共享变量并发性的 rely-guarantee 演算被扩展以包含概率行为。我们采用了一种代数方法，将概率 Kleene 代数与并发 Kleene 代数相结合并加以适配。相对于通用的概率事件结构语义，证明了该代数的可靠性。本文的主要贡献是基于该语义构建的一系列 rely-guarantee 规则。特别是，我们展示了如何在真并发指称语义中推导 rely-guarantee 规则以获得概率界限。通过对一个简单的概率并发程序（即有故障的埃拉托斯特尼筛法）的详细验证，说明了这些规则的用法。