Let the statements of the program be numbered from zero to the
total number of statements in the program. We define the state of a process
to be the value of each variable in the program's data space.
The message queue of a process is not considered
part of the program's data space.
The timed process trace of a process is a
sequence that captures the state changes
of the process, and the timestamps of the state changes,
from process initialization to process termination.
Formally, let a timed process trace be denoted by TP or 
, where:
describes the sequence of statements
that is executed. It contains a single statement number when a send
or receive statement is executed, and a sequence of statement numbers
when a local code block is executed.
is the state of the process before the statement sequence
is executed.
is the time at which the statement sequence started
execution, relative to time at which the process started execution.
is the data of the accepted message if
the statement executed is a receive statement. Otherwise, this field
is null.
, contains the final state of
the process, and the time it terminated. To emphasize that
the final term does not denote the execution
of any statement, 
is set to -1.
The trace or execution trace of a program is a tuple of the
timed process
traces of its processes. Formally,
, where E is the
trace, 
is the timed process trace for process
n, and N is the total number
of processes in the execution of the program. We assume all
processes start at the same time. The execution time of a
trace is the maximum of the termination times of its
constituent timed process traces.
The trace set or execution trace set, 
,
of program P with
input I, is the set of all possible traces of the given
program for the given input.