Refinement algebra for probabilistic programs

Larissa Meinicke*, Kim Solin

*Corresponding author for this work

Research output: Contribution to journalArticle

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 languageEnglish
Pages (from-to)3-31
Number of pages29
JournalFormal Aspects of Computing
Volume22
Issue number1
DOIs
Publication statusPublished - Jan 2010

Keywords

  • Action systems
  • Atomicity refinement
  • Data refinement
  • Kleene algebra
  • Probability
  • Refinement algebra

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

  • Cite this