Probabilistic rely-guarantee calculus

DOI10.1016/J.TCS.2016.01.016zbMATH Open1356.68156OpenAlexW2962831884MaRDI QIDQ507375FDOQ507375

Authors Annabelle McIver, Tahiry Rabehaja, Georg Struth 

Publication date 6 February 2017

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1409.0582

zbMATH Keywords

concurrencyevent structuresprogram semanticsprogram verificationKleene algebrarely-guaranteeprobabilistic programs

Mathematics Subject Classification ID

Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Semantics in the theory of computing (68Q55) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: Jones' rely-guarantee calculus for shared variable concurrency is extended to include probabilistic behaviours. We use an algebraic approach which combines and adapts probabilistic Kleene algebras 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 by deriving rely-guarantee rules within the true-concurrent denotational semantics. The use of these rules is illustrated by a detailed verification of a simple probabilistic concurrent program: a faulty Eratosthenes sieve.

Recommendations

• Probabilistic concurrent Kleene algebra
• Generalised rely-guarantee concurrency: an algebraic foundation
• The Rely-Guarantee method for verifying shared variable concurrent programs
• scientific article; zbMATH DE number 1956564
• On rely-guarantee reasoning

Cites work

• scientific article; zbMATH DE number 4018370 (Why is no real title available?)
• scientific article; zbMATH DE number 2087342 (Why is no real title available?)
• scientific article; zbMATH DE number 794262 (Why is no real title available?)
• A Structural Proof of the Soundness of Rely/guarantee Rules
• A language of specified programs
• A refinement calculus for shared-variable parallel and distributed programming
• An event structure model for probabilistic concurrent Kleene algebra
• Concurrent Kleene Algebra
• Concurrent Kleene algebra and its foundations
• Free shuffle algebras in language varieties
• Probabilistic concurrent Kleene algebra
• Probabilistic may/must testing: retaining probabilities by restricted schedulers
• Probabilistic models for the guarded command language
• Probabilistic rely-guarantee calculus
• Retaining the probabilities in probabilistic testing theory
• Semantics of probabilistic programs
• Towards Automated Proof Support for Probabilistic Distributed Systems

Cited in

(6)

• Probabilistic concurrent Kleene algebra
• Schedulers and finishers: on generating the behaviours of an event structure
• Weighted synchronous automata
• A better composition operator for quantitative information flow analyses
• Schedulers and finishers: on generating and filtering the behaviours of an event structure
• Probabilistic rely-guarantee calculus

This page was built for publication: Probabilistic rely-guarantee calculus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q507375)