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.
|Number of pages||19|
|Journal||Proceedings 11th International Workshop on Quantitative Aspects of Programming Languages and Systems : Rome, 23rd-24th March 2013|
|Publication status||Published - 2013|
|Event||International Workshop on Quantitative Aspects of Programming Languages and Systems (11th : 2013) - Rome|
Duration: 23 Mar 2013 → 24 Mar 2013