Trace theory

For trace theory in natural language syntax, see Trace (linguistics).

In mathematics and computer science, trace theory aims to provide a concrete mathematical underpinning for the study of concurrent computation and process calculi. The underpinning is provided by an algebraic definition of the free partially commutative monoid or trace monoid, or equivalently, the history monoid, which provides a concrete algebraic foundation, analogous to the way that the free monoid provides the underpinning for formal languages.

The power of trace theory stems from the fact that the algebra of dependency graphs (such as Petri nets) is isomorphic to that of trace monoids, and thus, one can apply both algebraic formal language tools, as well as tools from graph theory.

While the trace monoid had been studied by Pierre Cartier and Dominique Foata for its combinatorics in the 1960s, trace theory was first formulated by Antoni Mazurkiewicz in the 1970s, in an attempt to evade some of the problems in the theory of concurrent computation, including the problems of interleaving and non-deterministic choice with regards to refinement in process calculi.

References

• Volker Diekert, Grzegorz Rozenberg, eds. The Book of Traces, (1995) World Scientific, Singapore ISBN 981-02-2058-8
• Volker Diekert, Yves Metivier, "Partial Commutation and Traces", In G. Rozenberg and A. Salomaa, editors, Handbook of Formal Languages, Vol. 3, Beyond Words. Springer-Verlag, Berlin, 1997.
• Volker Diekert, Combinatorics on traces, LNCS 454, Springer, 1990, ISBN 3-540-53031-2