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 .