Contributions to a Trace Theory beyond Mazurkiewicz Traces

Dietrich Kuske

Introduction

For sequential systems, a mathematical foundation has proved fruitful. Already the consideration of formal systems in the first half of this century laid the ground for an distinction between (theoretically) computable and definitely not mechanizable tasks. Complexity theory sharpens this distinction further by the investigation of the frontier between tractable and nontractable computational tasks. Finite automata, although they are a very restricted model of a sequential computing device, have a rich theory as well as a wide-spread application. Their theory is closely related to algebraic theories. Furthermore, surprising connections between different logics and automata were found. These connections make it possible to automatize certain verification tasks in the development of software and hardware systems.

Aiming at similar benefits, attempts to develop a mathematical formalization of parallelism have a longstanding tradition in computer science. In the 60s, Petri introduced nets, now called Petri nets, as a model of concurrent systems. These Petri nets inspired many theoretical investigations and now have an extensive theory. But the semantics of these nets is technically quite complicated and a mathematical treatment in its full generality turns out to be cumbersome. Another line of research in this area is based on the idea of a process algebra introduced by Milner and Hoare in the 70s. This approach focuses more on at programming languages. Cellular automata can be traced back to ideas of v.~Neumann but became widely known only in the 70s (in particular by Conway's ``Game of Life''). Now they enjoy a well understood theory as well as several extensions.

Mazurkiewicz introduced traces, another model of concurrent behaviors, into computer science. They can be defined in two equivalent ways, either as dependence graphs or as equivalence classes of words. In both cases, one starts out from a finite set of elementary or atomic actions, called alphabet, and a binary dependence relation on the set of actions. Two such actions are dependent if they e.g. use a common resource. Hence, in a parallel computation of the system, independent actions can be performed in parallel, while dependent actions can be performed sequentially, only. A computation of such a system is modeled as a directed graph. The vertices of this graph correspond to events. Two such vertices are connected by an edge iff their labels are dependent. Since the computation is meant to run in time, the graph is assumed to be acyclic. Furthermore, we consider only finite computations and therefore finite graphs. A dependence graph is nothing but such a finite directed acyclic graph with edges between dependent vertices. Thus, a dependence graph describes the causal dependence in a computation.

In the alternative definition, one considers sequential observations of some parallel computation. The order in which independent actions are performed is regarded as irrelevant. In particular, if two observations differ only in the order of independent actions, they are identified. This defines an equivalence relation on words (over the alphabet of actions) and a trace is an equivalence class with respect to this equivalence.

It turns out that the linear extensions of a dependence graph form an equivalence class, i.e. a trace, and that any trace can be obtained from some dependence graph. In this sense, the two approaches are equivalent and ``it is only a matter of taste which objects are chosen for representing concurrent processes: equivalence classes of strings or labelled graphs.'' (Mazurkiewicz 1995, page 14). It seems that this dual nature of traces has contributed to a much to their success. This is not the right place to recall the amount of results on traces that have been obtained in the last two decades. For a in-depth surveys on the results on traces, the reader is referred to Diekert and Rozenberg (1995) that concentrates on the theoretical aspects in computer science as well as in mathematics, in particular in combinatorics.

Nonetheless, it turned out that certain limitations of traces made it necessary to extend the model into different directions. The probably most modest extension was that to infinite or real traces. These were introduced to model not only finite but also infinite computations. They can be defined in several equivalent ways: as directed and downward closed sets of finite traces (Mazurkiewicz 1987), via an equivalence relation on infinite words (Stark 1989, Kwiatkowska 1990) or as infinite dependence graphs where any event dominates only a finite number of vertices. Diekert introduced alpha- and delta-complex traces as metric completion of the set of finite traces with respect to two different metrics (Diekert 1991 and 1993) and showed in particular that they can alternatively be defined as infinite dependence graphs with some alphabetic information. Most of the considerations on complex traces are based on this second characterization. Another similar extension of traces (approximating traces) is presented in the same spirit (Diekert and Gastin 1998).

The generalizations mentioned so far have been introduced to model infinite behaviors of a parallel system. Differently, the aim of semi-commutations is to model some behaviors like the producer-consumer-example that do not fit into the setting of a symmetric independence relation. The idea is that the consumption of an item can be delayed after further productions, but conversely, the production cannot be postponed after the consumption. Here, we refer the reader to the survey Clerbout, Latteux and Roos (1995) and the literature cited therein.

Another limitation of Mazurkiewicz traces is the global and fixed independence relation. There are certainly systems where the answer to the question whether two particular actions can be performed concurrently depends on the situation, e.g. on the available resources that are produced by preceding events (cf. Katz and Peled 1992). An automaton with concurrency relations (Droste 1990 and 1992) is a (finite) automaton whose states are equipped with independence relations, i.e. in this model the dependence of actions can change while the system evolves. Similarly to traces, one obtains an equivalence relation on the set of finite computation sequences by identifying those sequences that differ only in the order of independent actions. But now this independence refers to the state were the first of the two actions is performed. Thus, originally the behavior of an automaton with concurrency relations was defined via equivalence classes of sequential behaviors. In (Bracho, Droste, Kuske 1995 and 1997), representing these computations by dependence graphs, we presented a partial order semantics for these computations under some mild assumptions on the automaton with concurrency relations.

Another approach to incorporate changing independence relations into the model of traces is represented by context and generalized traces (Biermann and Rozoy 1994). Here, two actions might be independent in one context and dependent in another where the context is (in the simplest form) given by the preceding action. Again, first an equivalence of words was constructed and context traces were defined as equivalence classes of words. An attempt to represent context traces by dependence graphs succeeded only partially (Biermann and Rozoy 1995).

Common to all generalizations listed so far is that the independence of actions is a binary relation. This limits their applicability since it is not possible to model a situation were two items of some resource are claimed by three actions. In such a situation, any two of the claiming actions might be performed concurrently and the third one afterwards. In addition, traces and their successors do not allow autoconcurrency. Local traces (Hoogers, Kleijn and Thiagarajan 1992, Hoogers 1994) are an attempt to solve these problems. Here, sets or even multisets of actions are declared independent and this depends on the history of the system. A representation of such systems by local event structures was obtained in the same papers. The forthcoming work Kuske and Morin (1999) aims at a representation of computations in this model by dependence graphs.

Note that in all the extensions mentioned so far, computations were first modeled as equivalence classes of sequential executions. Later (for some models much later) it was shown that these equivalence classes can be nicely represented by structures like dependence graphs. Differently, P-traces are by definition labeled partially ordered sets. Afterwards it is shown that they can also be obtained as equivalence classes of certain equivalence relations (Arnold 1991).

Besides this duality, the different extensions of Mazurkiewicz traces have been considered under several aspects. Mazurkiewicz used traces to model the behavior of one-safe Petri nets. Categorical adjunctions were constructed between larger classes of Petri nets and trace structures (Nielsen, Rosenberg and Thiagarajan 1990), step transition systems (i.e. local traces) (Mukund 1992) and concurrent automata (Droste and Shortt 1993). The order theoretic properties of the set of all trace-like objects was investigated for real traces (Gastin and Rozoy 1993, Boldi, Cardone and Sabadini 1993, Kuske 1999), for several versions of complex traces (Gastin and Petit 1992, Teodosiu 1993 and Diekert and Gastin 1998) and for the computations of an automaton with concurrency relations (Stark 1989, Droste 1990 and 1992, Kuske 1994, Schmitt 1998). Metric and topological questions were dealt with for real traces (Kwiatkowska 1990, Kummetz and Kuske 1999), for complex and approximating traces (Diekert 1991 and 1993, Diekert and Gastin 1998) and for computations of automata with concurrency relations (Kuske and Shortt 1998). The recognizable sets of trace-like structures were studied thoroughly. The relation to rational sets was investigated for semi-commutations, for real and for complex traces (cf. the corresponding surveys in Diekert and Rozenberg (1995)) and for computations of concurrent automata (Droste 1994, 1995, 1996). The relation to logically axiomatizable sets can be found for finite and for real traces in (Thomas 1990, Ebinger and Muscholl 1993, Ebinger 1994), for computations of concurrent automata in (Droste and Kuske 1996 and 1998) and for local traces in Kuske and Morin (1999).

In the first part of the current work, we will define an extension of dependence graphs to so called S-dags where S is a finite set of actions. They generalize not only dependence graphs as defined above, but also CCI-sets (Arnold 1991), dependence graphs of computations of concurrent automata (Bracho, Droste and Kuske 1995 and 1997), and (width-bounded) sp-pomsets (Lodaya and Weil 1998 and 1999). Essentially, a S-dag is a S-labeled directed acyclic graph. The edges of this graph represent the causal dependency between the events that are modeled by the vertices. There are only two restrictions that we impose: First, we allow no autoconcurrency. Second, for any label $a$, an event can depend on and influence at most one $a$-labeled event directly.

As a computational model for these S-dags, we investigate asynchronous cellular automata. They were defined originally for dependence graphs as a truly parallel accepting device (Zielonka 1987).¹ Since then, they have been intensively studied, cf. Zielonka (1995) and Diekert and Metivier (1995) for overviews. In Droste and Gastin (1996), they were generalized in such a way that an asynchronous cellular automaton can accept labeled posets (pomsets) without autoconcurrency (cf. also Kuske 1998, Droste, Gastin and Kuske 1999). Here, we extend them to the setting of S-dags. In the literature, infinite state systems are intensively studied (Moller 1996, Burkart and Esparza 1997). We extend asynchronous cellular automata furthermore by allowing them to have infinitely many states. To preserve some finiteness, the set of states is endowed with a well-quasi ordering. Thus, loosely speaking, asynchronous cellular machines or S-ACMs are asynchronous cellular automata that run on S-dags, have possibly infinitely many states, and are equipped with a well-quasi ordering on these states.

The behavior of a S-ACM is the accepted language, i.e. a set of S-dags. Hence a S-ACM describes a property of S-dags. Since the intersection as well as the union of two acceptable sets can be accepted by a S-ACM, properties describable by S-ACMs can become quite complex. Then it is of interest whether the combined property is contradictory, or, equivalently, whether at least one S-dag satisfies it. Thus, one would like to know whether a S-ACM accepts at least one S-dag. Using a result from Finkel and Schnoebelen 1998, we show that it is possible to gain this knowledge even automatically, i.e. we show that there exists an algorithm that on input of a S-ACM decides whether the S-ACM accepts at least one S-dag. For this to hold, we restrict the asynchronous cellular machines in two ways: The notion of "monotonicity"' involves a connection between the well-quasi ordering and the transitions of the machine. The notion "effectiveness" requires that the machine is given in a certain finite way.

Another natural question is whether two properties are equivalent, i.e. whether two S-ACMs accept the same language. Since there is a S-ACM that accepts all S-dags, a special case of this equivalence problem is to ask whether a given S-ACM accepts all S-dags. The latter question, called universality, essentially asks whether the described property is always true. The corresponding question for sequential automata has a positive answer which is a consequence of the decidability of the emptiness: If one wants to know whether a sequential automaton accepts all words, one constructs the complementary automaton and checks whether its languages is empty. Thus, the crucial point for sequential automata is that they can effectively be complemented. But the set of acceptable S-dag-languages is not closed under complementation. Therefore, we cannot proceed as for sequential automata. On the contrary, we show that the universality is undecidable even for S-ACMs with only finitely many states. These finite S-ACMs are called asynchronous cellular automata or S-ACA. The undecidability of the universality implies that the equivalence of two S-ACAs, the complementability of a S-ACA as well as the existence of an equivalent deterministic S-ACA are undecidable, too. These results (restricted to pomsets) together with a sketch of proof were announced in Kuske (1998). The proof we give here is based on ideas developed together with Paul Gastin.

The following chapter deals with the question which properties can be expressed by a S-ACA. For finite sequential automata, several answers are known to the question which properties can be checked by a finite sequential automaton: Kleene showed that these are precisely the rational properties. By the Myhill-Nerode Theorem, a property can be checked by a finite sequential automaton if its syntactic monoid is finite. Furthermore, Büchi (1960) and Elgot (1961) showed that a property of words can be checked by a finite sequential automaton if it can be expressed in the monadic second order logic. This relation between a model of a computational device (finite sequential automata) and monadic second order logic is a paradigmatic result. It has been extended in several directions, e.g. to infinite words (Büchi 1960), to trees (Rabin 1969) (cf. also Thomas 1990), to finite (Thomas 1990) and to real (Ebinger and Muscholl 1993, Ebinger 1994) traces, and to computations of concurrent automata (Droste and Kuske 1996 and 1998). The celebrated theorem of Zielonka (Zielonka 1987, 1995) together with the results from Thomas (1990) states that for dependence graphs of traces, the expressive power of asynchronous cellular automata and monadic second order logic coincide. Aiming at a similar result for S-dags, in Chapter 5 we show that this is not possible in general. More precisely, we show that any recognizable set of S-dags can be axiomatized by a sentence of the monadic second order logic, but that the converse is false even for first-order logic. To overcome this, we restrict to a subclass of all S-dags, called (S,k)-dags. This restriction makes it possible to relabel a (S,k)-dag by an asynchronous cellular automaton in such a way that one obtains a dependence graph over a certain dependence alphabet. This is the crucial step in our proof that any monadically axiomatizable set of (S,k)-dags can be accepted by a (nondeterministic) asynchronous cellular automaton. But we show that it is necessary to allow nondeterminism in the automata since the expressive power of deterministic S-ACAs will be proved to be strictly weaker. Again, the restriction to pomsets of the results presented in this chapter can be found in Kuske (1998). Here, we generalize the presentation in Droste, Gastin and Kuske (1999).

The final chapter of the first part is devoted to the relation between our asynchronous cellular automata and other models of concurrent behavior. The covering relation of a pomset without autoconcurrency is a S-dag. This allows us to speak of the set of pomsets that is accepted by a S-ACA: A pomset is accepted iff its Hasse-diagram admits a successful run. For pomsets, other automata models have been proposed in the literature. In particular, Arnold considered P-asynchronous automata (Arnold 1991) and Lodaya and Weil dealt with branching automata (Lodaya and Weil 1998, 1999). We finish our consideration of S-dags and S-ACAs by a comparison of the expressive power of these automata with the expressive power of our S-ACAs. We show that branching automata when restricted to width-bounded languages have the same expressive power as S-ACAs when restricted to series-rational pomsets. Somewhat as a byproduct, this implies that the expressive power of branching automata on width bounded sp-pomsets coincides with the expressive power of the monadic second order logic. Finally, we show that any P-asynchronous automaton can be simulated by a S-ACA.

The S-dags considered in the first part of the current work are clearly labeled graphs. Above, I already cited A. Mazurkiewicz stating "it is only a matter of taste which objects are chosen for representing concurrent processes: equivalence classes of strings or labelled graphs". To satisfy those that prefer the algebraic approach (or at least appreciate it as the author), this is followed in the second part where left divisibility monoids are considered. These left divisibility monoids were introduced in (Droste and Kuske 1998, 1999). As pointed out earlier, trace monoids are defined via a finite presentation (using a set of letters S together with a dependence relation on S). Later, algebraic properties where discovered that characterize trace monoids (up to isomorphism, Duboc 1986). Differently, left divisibility monoids are defined in the language of monoids, i.e. via their algebraic properties. In particular, it is required that the prefix relation be a partial order and that for any monoid element, the set of prefixes forms a distributive lattice. Thus, divisibility monoids involve monoid theoretic as well as order theoretic concepts.

In Chapter 8, we show that divisibility monoids can be finitely presented. Not only will we show that this is possible in general, but we will give a concrete representation for any divisibility monoid. Finally, we give a decidable class of finite presentations that give rise to all divisibility monoids.

Kleene's theorem on recognizable languages of finite words has been generalized in several directions, e.g. to formal power series (Schützenberger 1961), to infinite words (Büchi 1960), and to infinite trees (Rabin 1969). More recently, rational monoids were investigated (Sakarovitch 1987), in which the recognizable languages coincide with the rational ones. Building on results from Cori and Perrin (1985), Cori and Metivier (1988), Metivier (1986), a complete characterization of the recognizable languages in a trace monoid by c-rational sets was obtained in Ochmanski (1985). A further generalization of Kleene's and Ochmanski's results to concurrency monoids was given in Droste (1995). In Chapter 9, we derive such a result for divisibility monoids. The proofs by Ochmanski (1985) and by Droste (1995) rely on the internal structure of the elements of the monoids. Here, we do not use the internal representation of the monoid elements, but algebraic properties of the monoid itself. Thus, the considerations in Chapter 9 that appeared in Droste and Kuske (1999) can be seen as an algebraic proof of Ochmanski's Theorem.

The following chapter is devoted to the question when a divisibility monoid satisfies Kleene's Theorem, i.e. when the rational and the recognizable sets coincide. For trace monoids, this is only the case if the trace monoid is free. Our result for divisibility monoids states that they satisfy Kleene's Theorem iff they are rational. A defining property of divisibility monoids is that the sets of prefixes form a distributive lattice for any element of the monoid. We prove that this set of distributive lattices is width-bounded iff the monoid satisfies Kleene's Theorem. We obtain these characterizations applying the theory of rational functions (cf. Berstel 1979) and a Foata normal form of monoid elements similar to that for traces.

Büchi showed that the monadic second order theory of the linearly ordered set (N,<) is decidable. To achieve this goal, he used finite automata. In the course of these considerations he showed that a language in a free finitely generated monoid is recognizable iff it is monadically axiomatizable. In computer science, this latter result and its extension to infinite words are often referred to as "Büchi's Theorem" while in logic this term denotes the decidability of the monadic theory of (N,<). In the final chapter, I understand it in this second meaning. There, we show that certain monadic theories associated to a divisibility monoid are decidable. Let L denote the set of distributive lattices associated to a given divisibility monoid. We show that the monadic theory of this class is decidable iff the monoid satisfies Kleene's Theorem. In general, this theory is undecidable, but the monadic theory of the join-irreducible elements of these lattices is still decidable. For trace monoids, this latter result just states that the monadic theory of all dependence graphs is decidable, a corollary from Ebinger and Muscholl (1993) and Ebinger (1994).

At the very end, we prove an order theoretic result that is inspired by the two decidabilities just mentioned: Together with a result from Chapter 10, we know that the monadic theory of L is decidable if and only if L is width-bounded. In a certain sense, we show that this does not depend on the special character of L as the set of lattices associated with a divisibility monoid. Indeed, we show that any set of finite distributive lattices L has a decidable monadic theory if and only if the monadic theory of the join-irreducible elements of these lattices is decidable and L is width-bounded.

The present work shows that there are deep connections that arise from the theory of traces to different branches of mathematics. We finish the work with a list of problems that show up in the course of our considerations.