Traces

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,

$$\begin{array} {l} traces(a \rightarrow b \rightarrow\mbox{ \... ...a\rangle, \langle a,b\rangle, \langle a,b,c\rangle\}\end{array}$$

A useful operator on traces is projection: If D is a set of events then the trace $tr \mbox{$\mid$\hspace{-.037in}\small\`{}}D$ is defined to be the maximal subsequence of tr all of whose events are drawn from D . If D is a singleton set $\{d\}$ then we overload notation and write $tr \mbox{$\mid$\hspace{-.037in}\small\`{}}d$ for $tr \mbox{$\mid$\hspace{-.037in}\small\`{}}\{d\}$. Message extraction $tr \downarrow C$for a set of channel names C provides the maximal sequence of messages passed on channels C . Finally, $tr \Downarrow C$ 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:

$$\begin{eqnarray*} \langle \rangle\mbox{$\mid$\hspace{-.037in}\small\`{}}D & = & ... ...) \mbox{$\mid$\hspace{-.037in}\small\`{}}m \neq \langle \rangle\}\end{eqnarray*}$$

If tr is a sequence, then $\sigma(tr)$ is the set of events appearing in the sequence. The operator $\sigma$ extends to processes: $\sigma(P)$ is the set of events that appear in some trace of P .

In the traces model, if $traces(Q) \subseteq traces(P)$ then we say that Q is a refinement of P , written $P \sqsubseteq Q$.