Probabilities and Priorities in Timed CSP

Abstract

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. The semantics for our language represents a process as the set of its possible behaviours, where a behaviour models the priorities for different actions. A number of algebraic laws for our language are given and the model is illustrated with two examples.