Programming Research Group Technical Monograph PRG-111

Gavin Lowe

DPhil thesis Hilary 1993, 219 pages, ISBN 0-902928-88-0

In this thesis we present two languages that are refinements of Reed and Roscoe's language of Timed CSP: a probabilistic language, and a prioritized language.

We begin by describing the prioritized language and its semantic model. The syntax is based upon that of Timed CSP except some of the operators are refined into biased operators. A number of algebraic laws for our language are given and the model is illustrated with two examples.

We then describe the probabilistic languge, which is built on top of the prioritized language. The only cause of nondeterminism in the prioritized language is the nondeterministic choice operator; by replacing this with a probabilistic choice operator we obtain a language where it is possible to calculate the probability of any particular behaviour. The model is illustrated with an example of a communications protocol transmitting messages over an unreliable medium.