In [Sch96], the traces model is used as the basis for the proof rules presented. In this model, the semantics of a process P is defined to be the set of traces (sequences of events) that it may possibly perform. For example,
A useful operator on traces is projection: If D is a set of events then the trace is defined to be the maximal subsequence of tr all of whose events are drawn from D . If D is a singleton set then we overload notation and write for . Message extraction for a set of channel names C provides the maximal sequence of messages passed on channels C . Finally, provides the set of messages in tr passed along some channel in C . These may be described inductively on sequences, and the last by a set comprehension:
If tr is a sequence, then is the set of events appearing in the sequence. The operator extends to processes: is the set of events that appear in some trace of P .
In the traces model, if then we say that Q is a refinement of P , written .