  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.
