Computing systems can be seen nowadays as highly distributed and concurrent entities, that interact in various ways ranging from shared data to message exchange. Applications that need to be developed for such systems are particularly complex and reasoning about their correctness is a very challenging issue. Being able to apply formal methods for validating properties of such applications and systems is not merely of theoretical interest, but also a crucial goal in developing industrial critical systems of high quality and performance.

Coping with concurrency on a rigorous sound basis is only possible if an appropriate formal model is available, that is rich enough for modelling purposes and suﬃciently simple for providing a ﬂexible framework for mathematical reasoning. Various models have been proposed for concurrent systems, let us just mention Petri nets, event structures, process algebras, or Milner-Hoare’s theory of communicating sequential systems. In the late seventies Mazurkiewicz proposed the notion of traces as an intuitive and mathematically elegant abstraction of concurrency. The underlying notion of partial commutations proved to be a very natural concept, that had been already considered in combinatorics by Cartier and Foata (1969), as well as in computer science in the area of parallel program schemata by Keller (1973). The theory of Mazurkiewicz traces is a particularly appealing framework, since it employs techniques and tackles problems from quite diverse areas including formal language theory, combinatorics, graph theory, algebra, logic, and the theory of concurrent and parallel systems. In all these areas the theory of traces has led to interesting problems and signiﬁcant results, and “The Book of Traces” (1995) gives an excellent overview of the results obtained until the mid nineties.

In recent years, Mazurkiewicz trace theory has spread towards various other areas, continuing to be a rich source of powerful methods and of new challenging problems. Some of these oﬀsprings are described next.

Communicating ﬁnite-state machines, or equivalently, FIFO channel systems or message passing automata, are the most basic model for concurrent peers that cooperate via asynchronous message pass- ing using unbounded buﬀers. Compared with other models of true concurrency, like Petri nets for instance, these machines are computationally much harder, actually Turing equivalent. Channel systems are the basis of the standard ITU notation SDL (norm Z.100). Their syntactic counterpart are message sequence charts (ITU norm Z.120), a standard that is widely used in the design of protocols. Various results about the expressivity of these formalisms and the decidability of model-checking problems have been obtained by exploiting their connection with Mazurkiewicz traces. Trace theory is for instance the building brick in showing the equivalence of different speciﬁcation formalisms under some natural assumptions on the channel scheduling policy.

Control problems arise in open environments, where a system is required to behave in a desired way, no matter how the environment acts. Control problems can be also viewed as games between a system and its environment, where being able to compute a winning strategy amounts to synthesize a controller that enforces the system to behave as speciﬁed. Whereas the control of sequential (ﬁnite-state) systems is meanwhile both well-understood and tractable, the case of distributed systems is more challenging (undecidable in the general case). Several restricted models for distributed games have been considered, and various decidability results and open problems are known. Trace theory plays again a fundamental role, since several game models are based on asynchronous automata, which are the standard model of distributed automaton associated with trace languages.

Temporal logics for traces have been developed in the linear-time framework (i.e., formulas express properties of single distributed executions). As it turned out, the local logics are algorithmically more appealing than global ones. The investigations concentrate on two aspects: the search for a simple set of modularities that allow to capture the whole of ﬁrst-order logic and methods for handling large sets of modularities eﬃciently. While the former problem has been solved by the results of Diekert and Gastin, the latter is still ﬂourishing. In the light of the results on distributed games, it is a hard problem to come up with a branching time and local temporal logic that has the nice features of logics like CTL or CTL∗ . Furthermore, the transfer of insights from the trace setting into more applied scenarios like MSCs is not completed.

It is not just interesting to ask whether a particular word is accepted by a ﬁnite automaton, but also to know the number of diﬀerent ways it can be accepted. This question developed into the theory of weighted automata and formal power series. Some of the cornerstones of trace theory have been analyzed in this light and some of the results on rational formal power series have been transferred into the trace setting, but much is left to be done, e.g., almost nothing is known about algebraic series in partially commuting variables. So far, the relation to probabilistic and timed systems remains to be explored in depth.