Probabilistic concurrent Kleene algebra

Annabelle McIver; Tahiry Rabehaja; Georg Struth

doi:10.4204/EPTCS.117.7

Probabilistic concurrent Kleene algebra

Annabelle McIver, Tahiry Rabehaja, Georg Struth

School of Computing

Research output: Contribution to journal › Conference paper › peer-review

9 Citations (Scopus)

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.

Original language	English
Pages (from-to)	97-115
Number of pages	19
Journal	Proceedings 11th International Workshop on Quantitative Aspects of Programming Languages and Systems : Rome, 23rd-24th March 2013
DOIs	https://doi.org/10.4204/EPTCS.117.7
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

Access to Document

10.4204/EPTCS.117.7

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",

note = "International Workshop on Quantitative Aspects of Programming Languages and Systems (11th : 2013) ; Conference date: 23-03-2013 Through 24-03-2013",

}

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

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

SN - 2075-2180

T2 - International Workshop on Quantitative Aspects of Programming Languages and Systems (11th : 2013)

Y2 - 23 March 2013 through 24 March 2013

ER -

Probabilistic concurrent Kleene algebra

Abstract

Access to Document

Fingerprint

Cite this