Probabilistic models for the guarded command language

He Jifeng*, K. Seidel, A. McIver

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

120 Citations (Scopus)


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.

Original languageEnglish
Pages (from-to)171-192
Number of pages22
JournalScience of Computer Programming
Issue number2-3
Publication statusPublished - Apr 1997
Externally publishedYes


  • Algebraic laws
  • Probabilistic programming language
  • Semantics


Dive into the research topics of 'Probabilistic models for the guarded command language'. Together they form a unique fingerprint.

Cite this