Partial Commutation and Traces

79 pagesParallelism and concurrency are fundamental concepts in computer science. Specification and verification of concurrent programs are of first importance. It concerns our daily life whether software written for distributed systems behaves correctly. It is clear that a satisfactory notion of correctness has to be based on a rigorous mathematical model. Several formalisms have been proposed. Among others there are Petri nets, Hoare's and Milner's CSP and CCS, event structures, and branching temporal logics. The mathematical analysis of these models may become complicated, however. Based on the behavior of elementary net systems Mazurkiewicz introduced the concept of partial commutation to the computer science community. The abstract description of a concurrent process is then called a trace, being defined as a congruence class of a word (sequence) modulo identities of the form ab = ba for some pairs of letters. The success of Mazurkiewicz' approach results from the fact that on one hand partial commutation copes with some important phenomena in concurrency and on the other hand it is close to the classical theory of free monoids describing sequential programs. In particular it is possible to transfer the notion of finite sequential state control to the notion of finite asynchronous state control. There is a satisfactory theory of recognizable languages relating finite semigroups, rational operations, asynchronous automata, and logic. This leads to decidability results and various effective operations. The theory of partial commutation and of trace monoids has been developed both by its interpretation as a model for parallel computation and by its mathematical interest in algebra, formal languages, and combinatorics. Since the beginning in combinatorics by Cartier and Foata (1969) and the formulation of trace theory by Mazurkiewicz (1977) the theory has grown in breadth and depth. It led to significant results with interesting applications. The present contribution reflects some important topics including basic properties and infinite traces. Most of the results are from the monograph [34], but we covered also some new material. Each section gives a short bibliographical remark and leads to further references