Programming Research Group Technical Report TR-1-91

An operational semantics for Timed CSP

S A Schneider.

February 1991, 42pp.

An operational semantics is defined for the language of timed CSP, in terms of two relations: an evolution relation, which describes when a process becomes another simply by allowing time to pass; and a timed transition relation, which describes when a process may become another by performing an action at a particular time. It is shown how the timed behaviours used as the basis for the denotational models of the language may be extracted from the operational semantics. Finally, the failures model for timed CSP is shown to be equivalent to may-testing, and thus to trace congruence.


A version of this paper is available as a 206,479 byte compressed PostScript file.