Refinement algebra for probabilistic programs

Larissa Meinicke; Kim Solin

doi:10.1007/s00165-009-0111-1

Refinement algebra for probabilistic programs

Larissa Meinicke^*, Kim Solin

^*Corresponding author for this work

Department of Computing

Research output: Contribution to journal › Article › peer-review

6 Citations (Scopus)

Abstract

We identify a refinement algebra for reasoning about probabilistic program transformations in a total-correctness setting. The algebra is equipped with operators that determine whether a program is enabled or terminates respectively. As well as developing the basic theory of the algebra we demonstrate how it may be used to explain key differences and similarities between standard (i.e. non-probabilistic) and probabilistic programs and verify important transformation theorems for probabilistic action systems.

Original language	English
Pages (from-to)	3-31
Number of pages	29
Journal	Formal Aspects of Computing
Volume	22
Issue number	1
DOIs	https://doi.org/10.1007/s00165-009-0111-1
Publication status	Published - Jan 2010

Keywords

Action systems
Atomicity refinement
Data refinement
Kleene algebra
Probability
Refinement algebra

Access to Document

10.1007/s00165-009-0111-1

Link to publication in Scopus

Fingerprint Dive into the research topics of 'Refinement algebra for probabilistic programs'. Together they form a unique fingerprint.

Cite this

@article{137d355ad3d049ed923e8f3e7f77c1bc,

title = "Refinement algebra for probabilistic programs",

abstract = "We identify a refinement algebra for reasoning about probabilistic program transformations in a total-correctness setting. The algebra is equipped with operators that determine whether a program is enabled or terminates respectively. As well as developing the basic theory of the algebra we demonstrate how it may be used to explain key differences and similarities between standard (i.e. non-probabilistic) and probabilistic programs and verify important transformation theorems for probabilistic action systems.",

keywords = "Action systems, Atomicity refinement, Data refinement, Kleene algebra, Probability, Refinement algebra",

author = "Larissa Meinicke and Kim Solin",

year = "2010",

month = jan,

doi = "10.1007/s00165-009-0111-1",

language = "English",

volume = "22",

pages = "3--31",

journal = "Formal Aspects of Computing",

issn = "0934-5043",

publisher = "Springer, Springer Nature",

number = "1",

}

TY - JOUR

T1 - Refinement algebra for probabilistic programs

AU - Meinicke, Larissa

AU - Solin, Kim

PY - 2010/1

Y1 - 2010/1

N2 - We identify a refinement algebra for reasoning about probabilistic program transformations in a total-correctness setting. The algebra is equipped with operators that determine whether a program is enabled or terminates respectively. As well as developing the basic theory of the algebra we demonstrate how it may be used to explain key differences and similarities between standard (i.e. non-probabilistic) and probabilistic programs and verify important transformation theorems for probabilistic action systems.

AB - We identify a refinement algebra for reasoning about probabilistic program transformations in a total-correctness setting. The algebra is equipped with operators that determine whether a program is enabled or terminates respectively. As well as developing the basic theory of the algebra we demonstrate how it may be used to explain key differences and similarities between standard (i.e. non-probabilistic) and probabilistic programs and verify important transformation theorems for probabilistic action systems.

KW - Action systems

KW - Atomicity refinement

KW - Data refinement

KW - Kleene algebra

KW - Probability

KW - Refinement algebra

UR - http://www.scopus.com/inward/record.url?scp=77149134993&partnerID=8YFLogxK

U2 - 10.1007/s00165-009-0111-1

DO - 10.1007/s00165-009-0111-1

M3 - Article

AN - SCOPUS:77149134993

VL - 22

SP - 3

EP - 31

JO - Formal Aspects of Computing

JF - Formal Aspects of Computing

SN - 0934-5043

IS - 1

ER -