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