Probabilistic rely-guarantee calculus

Annabelle McIver, Tahiry Rabehaja*, Georg Struth

*Corresponding author for this work

Research output: Contribution to journalArticle

1 Citation (Scopus)

Abstract

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.

Original languageEnglish
Pages (from-to)120-134
Number of pages15
JournalTheoretical Computer Science
Volume655
DOIs
Publication statusPublished - 6 Dec 2016

Keywords

  • Concurrency
  • Event structures
  • Kleene algebra
  • Probabilistic programs
  • Program semantics
  • Program verification
  • Rely-guarantee

Fingerprint Dive into the research topics of 'Probabilistic rely-guarantee calculus'. Together they form a unique fingerprint.

  • Cite this