Operations on traces include:
A Trace of a process is a log/record of the events/actions it has
undertaken (tape recording).
A Specification is a predicate (some expression in terms of variables
in the trace) that we would like to be true about a process.
A trace can go on for ever (e.g. trace of the GAME process).
Traces are written #tex2html_wrap_inline4080#
;SPM_lt;;SPM_gt; is the empty trace.
A trace of CLEVERGAME might be:
Catenation: s #tex2html_wrap_inline4086# t
Simply appends trace t to trace s.
Note: f(s #tex2html_wrap_inline4088# t) is f(s) #tex2html_wrap_inline4090# f(t)
(for classes of
functions which map sequences of events to sequences of events).
All the symbols not in alphabet A are removed from the trace s.
Most important is Ordering:
If s is a copy of an initial subsequence of t, it is possible to find
an extension u of s, s.t. s #tex2html_wrap_inline4092# u = t. Thus we can define an ordering,
in some sense #tex2html_wrap_inline4094#.
Other useful operations include
#tex2html_wrap_inline4096# , the head of a trace,
#tex2html_wrap_inline4098# , the tail of a trace, and
#tex2html_wrap_inline4100#, the length of a trace.