Probabilistic Concurrent Kleene Algebra

Annabelle McIver
(Macquarie University)
Tahiry Rabehaja
(Macquarie University and University of Sheffield)
Georg Struth
(University of Sheffield)

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.

In Luca Bortolussi and Herbert Wiklicky: Proceedings 11th International Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2013), Rome, 23rd-24th March 2013, Electronic Proceedings in Theoretical Computer Science 117, pp. 97–115.
Published: 11th June 2013.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: