Probabilistic rely-guarantee calculus

详细信息    查看全文

• 作者：Annabelle McIver^a ; ^{annabelle.mciver@mq.edu.au} ; Tahiry Rabehaja^a ; ^{tahiry.rabehaja@mq.edu.au} ; Georg Struth^b ; ^{g.struth@sheffield.ac.uk}
• 关键词：Probabilistic programs ; Concurrency ; Rely-guarantee ; Program verification ; Program semantics ; Kleene algebra ; Event structures
• 刊名：Theoretical Computer Science
• 出版年：2016
• 出版时间：6 December 2016
• 年：2016
• 卷：655
• 期：part_PB
• 页码：120-134
• 全文大小：498 K
• 卷排序：655

文摘

Jones' rely-guarantee calculus for shared variable concurrency is extended to include probabilistic behaviours. We use an algebraic approach that is based on a combination of probabilistic Kleene algebra with concurrent Kleene algebra. Soundness of the algebra is shown relative to a general probabilistic event structure semantics. The main contribution of this paper is a collection of rely-guarantee rules built on top of that semantics. In particular, we show how to obtain bounds on probabilities of correctness by deriving quantitative extensions of rely-guarantee rules. The use of these rules is illustrated by a detailed verification of a simple probabilistic concurrent program: a faulty Eratosthenes sieve.