|
Probabilistic communicating processes
Karen Seidel
DPhil thesis, Michaelmas 1992, 125 pages,
ISBN 0-902928-79-1
A mathematical formalism for the specification and proof of
correctness of probabilistic communicating processes is developed. This
formalism combines a notion of probabilistic correctness with the
theory of concurrency provided by the language of CSP. A semantics of a
model in which processes are defined as probability measures on the
space of infinite traces is presented. Later the sematics of a model in
which processes are defined as conditional probability measures is
presented. A significant case study is used to demonstrate the
applicability of the model and the proof rules.
|
![[Oxford Spires]](/im/spires.gif){kind=small}
oucl