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.
|Number of pages||19|
|Journal||Electronic Notes in Theoretical Computer Science|
|Publication status||Published - 7 Mar 2008|
- action systems
- data refinement
- Kleene algebra
- refinement algebra