In: Information and Computation, Vol. 116, No. 2, pages 193-213. 1995.
Abstract: 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 behaviors 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.
Keywords: Petri nets, operational semantics, timed CSP, timed transition relation.