Abstract
We propose an abstract refinement algebra for reasoning about probabilistic programs in a total-correctness setting. The algebra is equipped with operators that determine whether a program is enabled, has certain failure or does not have certain failure, respectively. As an application, refinement rules for probabilistic action systems are derived in the algebra.
Original language | English |
---|---|
Pages (from-to) | 177-195 |
Number of pages | 19 |
Journal | Electronic Notes in Theoretical Computer Science |
Volume | 201 |
Issue number | C |
DOIs | |
Publication status | Published - 7 Mar 2008 |
Keywords
- action systems
- data refinement
- Kleene algebra
- probability
- refinement algebra