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 sufficiently simple for providing a flexible 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 significant 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 offsprings are described next.

Message sequence charts and synthesis of communicating automata

Communicating finite-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 buffers. 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 specification formalisms under some natural assumptions on the channel scheduling policy.

Synthesis and control

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 specified. Whereas the control of sequential (finite-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.

Concurrent temporal logics

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 first-order logic and methods for handling large sets of modularities efficiently. While the former problem has been solved by the results of Diekert and Gastin, the latter is still flourishing. 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.

Equations and word membership problems

Partial commutation, the feature that separates free monoids from trace monoids, has been investigated in algebra independently from the development in computer science. The work on the solvability of equations in monoids (e.g., partially commutative inverse monoids, graph products) re-joins these two directions with surprising connections to Petri nets. The algorithms for deciding word membership have been investigated from the beginning, by Bertoni, Goldwurm and Sabbadini. Recently some research on more efficient solutions has focused on specific classes of languages, like star-free, local or languages corresponding to well-nested cycles.

Quantitative aspects

It is not just interesting to ask whether a particular word is accepted by a finite automaton, but also to know the number of different 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.