Gavin Lowe
1991, 50pp.
In this paper we present two refinements to timed CSP [see PRG-75]: a probabilistic model, and a fully deterministic model with a notion of priority.
In the first part of the paper we describe the deterministic model, which is based upon prioritizing bags of actions. We describe a language based upon timed CSP in which we have refined the syntax so as to remove all nondeterminism by producing biased 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 algebraic laws for our language are given and the model is illustrated with an example.
In the second part of the paper, we extend the language by adding a probabilistic choice operator. We produce a semantic model for our language which gives the probabilities of different behaviours occurring, as well as modeling the relative priorities for events within a behaviour. The model is illustrated with an example of a communications protocol transmitting messages over an unreliable medium.