PROBABILISTIC AND PRIORITIZED MODELS OF TIMED CSP

In this paper we present two languages that are refinements of timed C SP (Davies and Schneider, this volume): a probabilistic language, and a fully deterministic language with a notion of priority. In the first part of the paper we describe the deterministic language and its sema ntic model. The syntax is based upon that of timed CSP except some of the operators are refined so as to remove all nondeterminism; this pro duces prioritized operators. The semantics for our language represents a process as the set of possible behaviours for the process, where a behaviour models the priorities for different actions. A number of alg ebraic laws for our language are given and the model is illustrated wi th two examples. In the second part of the paper, we extend the langua ge by adding a probabilistic choice operator. We produce a semantic mo del for our language which gives the probabilities of different behavi ours occurring, as well as modelling the relative priorities for event s within a behaviour. The model is illustrated with an example of a co mmunications protocol transmitting messages over an unreliable medium.