### 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 | |

Publication status | Published - 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

Meinicke, L., & Solin, K. (2010). Refinement algebra for probabilistic programs.

*Formal Aspects of Computing*,*22*(1), 3-31. https://doi.org/10.1007/s00165-009-0111-1