Probabilistic Concurrent Kleene Algebra

TL;DR

This paper extends concurrent Kleene algebra to include probabilistic aspects, creating a unified algebraic framework that models nondeterminism, concurrency, and probability, and is validated against probabilistic automata.

Contribution

It introduces a probabilistic extension of concurrent Kleene algebra and generalizes Jones' rely/guarantee calculus within this framework.

Findings

The algebra is sound with respect to probabilistic automata.

It unifies nondeterminism, concurrency, and probability in a single algebraic structure.

The framework supports algebraic reasoning about probabilistic concurrent systems.

Abstract

We provide an extension of concurrent Kleene algebras to account for probabilistic properties. The algebra yields a unified framework containing nondeterminism, concurrency and probability and is sound with respect to the set of probabilistic automata modulo probabilistic simulation. We use the resulting algebra to generalise the algebraic formulation of a variant of Jones' rely/guarantee calculus.