Refinement algebra for probabilistic programs

Larissa Meinicke*, Kim Solin

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

6 Citations (Scopus)


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
Issue number1
Publication statusPublished - Jan 2010


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


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

Cite this