Reactive probabilistic programs and refinement algebra

A trace semantics is given for a probabilistic reactive language which is capable of modelling probabilistic action systems. It is shown that reactive probabilistic programs with the trace semantics form a general refinement algebra. The abstract-algebraic characterisation means that the proofs of earlier-established transformation rules can be reused for probabilistic action systems with trace semantics.16 page(s