Refinement-oriented probability for CSP

Carroll Morgan*, Annabelle McIver, Karen Seidel, J. W. Sanders

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

52 Citations (Scopus)


Jones and Plotkin give a general construction for forming a probabilistic powerdomain over any directed-complete partial order [Jon90, JoP89]. We apply their technique to the failures/divergences semantic model for Communicating Sequential Processes [Hoa85]. The resulting probabilistic model supports a new binary operator, probabilistic choice, and retains all operators of CSP including its two existing forms of choice. An advantage of using the general construction is that it is easy to see which CSP identities remain true in the probabilistic model. A surprising consequence however is that probabilistic choice distributes through all other operators; such algebraic mobility means that the syntactic position of the choice operator gives little information about when the choice actually must occur. That in turn leads to some interesting interaction between probability and nondeterminism. A simple communications protocol is used to illustrate the probabilistic algebra, and several suggestions are made for accommodating and controlling nondeterminism when probability is present.

Original languageEnglish
Pages (from-to)617-647
Number of pages31
JournalFormal Aspects of Computing
Issue number6
Publication statusPublished - 1996
Externally publishedYes


  • Concurrency
  • CSP
  • Nondeterminism
  • Probability
  • Refinement


Dive into the research topics of 'Refinement-oriented probability for CSP'. Together they form a unique fingerprint.

Cite this