The message sequence of a process is the sequence
of messages the process accepts from initialization to termination.
Formally, a message sequence is denoted by M or
, where
is the data of the nth accepted message.
is the number of the statement at which the message
is accepted.
A message trace,
, of a trace E,
is a tuple of the message sequences of each of the
processes in that trace. Formally,
, where N is the
total number of processes in trace E, and
is the message sequence of process n (where
).
The message trace set,
, of program P for input I,
is the set of all possible message traces of the program for the given
input i.e.
.
If two traces have the same message trace, they
must have the same program trace, i.e. given two
traces
and
,
.
In other words, just as in sequential programs
the program input is sufficient to
determine the program trace, in the case of message passing programs the
program input and the message trace together are sufficient to determine
the program trace.