Refinement Algebra for Probabilistic Programs

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.