Causal Traces

Causal traces are strings over caused actions, which do not only tell what has happened (the action) but also on which actions in the past this was dependent (the causes). The latter information is provided by a set of backpointers along the trace, in the form of positive natural numbers. Thus, causal traces are the linear time counterpart of the well-known model of causal trees. We develop a complete algebra of causal traces, in which it is allowed to swap subtraces that are causally independent. Care has to be taken that such swapping is congruent with respect to trace composition; in particular, caused actions that occur later in the trace may have to be adjusted to take swapping into account. The objects of the algebra are therefore not simply traces, but traces combined with a causal adjustment which retains the necessary information to make concatenation well-defined. We show how adjusted causal traces can be used to implement Mazurkiewicz traces, and how they may be used as morphisms in a symmetric strict monoidal category very similar to that of concatenable (Petri net) processes