Probabilistic Concurrent Kleene Algebra

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.

In Proceedings QAPL 2013, arXiv:1306.2413

References in corpus (1)

• Assume-Guarantee Abstraction Refinement for Probabilistic Systems

Cited by in corpus (4)

• Towards Verifying Safety Properties of Real-Time Probabilistic Systems
• On the construction of multi-valued concurrent dynamic logic
• An Event Structure Model for Probabilistic Concurrent Kleene Algebra
• Quantitative Aspects of Programming Languages and Systems over the past $2^4$ years and beyond