Gavin Lowe
1992, 38pp.
In a previous paper [TR-24-91] we presented two languages based upon timed CSP, with associated semantic models. The first language included biased operators in the syntax, which could be used to model different priorities on actions. The second language extended this by adding a probabilistic choice operator to the syntax; this allowed us to give a semantics which modelled the probabilities of different behaviours occurring.
In this paper we aim to extend these two languages, to bring them up to the full expressive strength of timed CSP. We add environments (variable bindings) to our semantics; this allows us to give a more satisfactory model of recursion and allows us to model mutual recursion.
Our previous language did not allow us to model communication of values over a channel. We extend our language and semantic model to overcome this.
We prove a new property that holds of all behaviours of a process; this basically says that if a process can refuse two actions seperately then it can refuse their union.
We also add infinite probabilistic choice, timeout, timed transfer, event interrupt and communicating parallel operators to our syntax, and give corresponding semantic definitions.