Probabilistic rely-guarantee calculus

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

Authors: Annabelle McIver, Tahiry Rabehaja, Georg Struth 

Publication date: 6 February 2017

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

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.

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

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

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)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• A language of specified programs
• Concurrent Kleene Algebra
• A Structural Proof of the Soundness of Rely/guarantee Rules
• Concurrent Kleene algebra and its foundations
• Free shuffle algebras in language varieties
• Semantics of probabilistic programs
• A refinement calculus for shared-variable parallel and distributed programming
• Probabilistic models for the guarded command language
• Retaining the probabilities in probabilistic testing theory
• Probabilistic may/must testing: retaining probabilities by restricted schedulers
• An Event Structure Model for Probabilistic Concurrent Kleene Algebra
• Title not available (Why is that?)
• Title not available (Why is that?)
• Probabilistic rely-guarantee calculus
• Towards Automated Proof Support for Probabilistic Distributed Systems

Cited In (5)

• A better composition operator for quantitative information flow analyses
• Weighted synchronous automata
• Schedulers and finishers: on generating and filtering the behaviours of an event structure
• Probabilistic rely-guarantee calculus
• Schedulers and Finishers: On Generating the Behaviours of an Event Structure

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)