Probabilistic concurrent Kleene algebra

Research output: Contribution to journalConference paperResearchpeer-review

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.

Fingerprint

Kleene Algebra
Concurrent
Probabilistic Automata
Algebra
Nondeterminism
Concurrency
Modulo
Calculus
Generalise
Formulation
Simulation
Framework
Sound

Cite this

@article{820836ea9997446fbb27c96df268882e,
title = "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.",
author = "Annabelle McIver and Tahiry Rabehaja and Georg Struth",
year = "2013",
doi = "10.4204/EPTCS.117.7",
language = "English",
pages = "97--115",
journal = "Proceedings 11th International Workshop on Quantitative Aspects of Programming Languages and Systems : Rome, 23rd-24th March 2013",
issn = "2075-2180",
publisher = "EPTCS",

}

TY - JOUR

T1 - Probabilistic concurrent Kleene algebra

AU - McIver,Annabelle

AU - Rabehaja,Tahiry

AU - Struth,Georg

PY - 2013

Y1 - 2013

N2 - 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.

AB - 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.

U2 - 10.4204/EPTCS.117.7

DO - 10.4204/EPTCS.117.7

M3 - Conference paper

SP - 97

EP - 115

JO - Proceedings 11th International Workshop on Quantitative Aspects of Programming Languages and Systems : Rome, 23rd-24th March 2013

T2 - Proceedings 11th International Workshop on Quantitative Aspects of Programming Languages and Systems : Rome, 23rd-24th March 2013

JF - Proceedings 11th International Workshop on Quantitative Aspects of Programming Languages and Systems : Rome, 23rd-24th March 2013

SN - 2075-2180

ER -