Probabilistic Demonic Refinement Algebra

Abstract. We propose an abstract algebra for reasoning about probabilistic programs. In contrast to probablisitic Kleene algebra it allows reasoning about total correctness and in addition to weak iteration (Kleene star) also has a strong iteration operator. We extend the algebra with operators that determine whether a program is enabled, has certain failure or does not have certain failure, respectively. The algebra is applied to the derivation of refinement rules for probabilistic action systems.