Probabilistic models for the guarded command language

The two models presented in this paper provide two different semantics for an extension of Dijkstra's language of guarded commands. The extended language has an additional operator, namely probabilistic choice, which makes it possible to express randomized algorithms. An earlier model by Claire Jones included probabilistic choice but not non-determinism, which meant that it could not be used for the development of algorithms from specifications. Our second model is built on top of Claire Jones' model, using a general method of extending a probabilistic cpo to one which also contains non-determinism. The first model was constructed from scratch, as it were, guided only by the desire for certain algebraic properties of the language constructs, which we found lacking in the second model. We compare and contrast the properties of the two models both by giving examples and by constructing mappings between them and the non-probabilistic model. On the basis of this comparison we argue that, in general, the first model is preferable to the second.