Deterministic asynchronous automata for infinite traces^{∗}

Volker Diekert Anca Muscholl

Universität Stuttgart Institut für Informatik Breitwiesenstr. 20-22 D-7000 Stuttgart 80

Draft version, July 1992. Submitted to STACS 93

Abstract

This paper shows the equivalence between the family of recognizable languages over infinite traces and the family of languages which are accepted by some asynchronous cellular Muller automaton. We thus give a proper generalization of McNaughton’s Theorem from infinite words to infinite traces. Thereby we solve one of the main open problems in this field. As a special case we obtain that every closed (w.r.t. the independence relation) word language is accepted by some deterministic Muller automaton. We also determine the complexity of deciding whether a I-diamond Muller automaton accepts a closed language.

1 Introduction

A. Mazurkiewicz introduced the concept of traces as a suitable semantics for concurrent systems [Maz77]. A concurrent system is given by a set of atomic actions Σ = {a, b, c, …} together with an independence relation I ⊆ Σ × Σ which specifies pairs of actions which can be performed concurrently. This leads to an equivalence relation on Σ^{∗} generated by the independence relation I. More precisely, if a and b denote independent actions, then for u, v ∈ Σ^{∗} uabv and ubav are equivalent. They can be interpreted as two sequential observations of the same concurrent run. Since this equivalence relation turns out to be a congruence, it defines a quotient monoid of Σ^{∗}, which is called trace monoid and is denoted by IM(Σ, D). In fact, these monoids have been introduced and studied independently by Cartier and Foata [CF69] in combinatorics and are also called free partially commutative monoids.

Hence, a trace is a congruence class of words. From a different point of view, a trace is a finite labelled acyclic graph, where the labels of vertices are actions and edges represent the ordering between dependent actions. Such a graph is called dependence graph and the semantics is that every execution of the concurrent run has to respect the induced partial order.

In order to describe non-sequential processes which never terminate, e.g. distributed operating systems, the notion of infinite trace was needed. One of the first explicit definition of infinite traces was given again by Mazurkiewicz [Maz87]. He defines an (infinite) trace as an (infinite) prefix closed directed subset of finite traces. This is the same as an (infinite) dependence graph where each vertex has finitely many predecessors only [Maz87, Thm.13]. In the following these objects are called here real traces. Unfortunately, there can be no convenient associative concatenation on real traces. This led to the definition of the monoid of complex traces [Die91]. It is a quotient monoid of the set of infinite dependence graphs under the largest congruence which respects real parts.

∗This research has been supported by the ESPRIT Basic Research Actions No. 3166 ASMICS.

Recognizable languages form an important family of a monoid. For finite traces and (in)finite words, there exist several characterizations of recognizable subsets. For instance, they can be defined by means of saturating morphisms to a finite monoid. A further approach is the characterization based on rational (co-rational, respectively) expressions, which is given by Kleene’s and Büchi’s theorems for words (Ochmanski’s theorem for traces, respectively). Finally, recognizable languages are commonly characterized by finite automata.

As regards recognizable real trace languages, there exist equivalent characterizations by means of recognizing morphisms [Gas91] and by co-rational expressions [GPZ91]. Furthermore, Gastin/Petit studied asynchronous automata for infinite traces [GP92]. More precisely, asynchronous (cellular) automata have been defined by Zielonka for finite traces ([Zie87], [Zie89]). They can describe concurrency in a very suitable way, due to their decentralized control which allows parallel execution of independent actions. For infinite traces, adequate acceptance conditions were needed. Gastin/Petit used a suitable Büchi condition which led to a characterization of recognizable real trace languages by nondeterministic asynchronous Büchi automata. The major open problem which arised and which we are going to solve here was a characterization by some kind of deterministic automata.

In the theory of recognizable word languages the theorem of McNaughton states the equivalence between nondeterministic Büchi automata and deterministic Muller automata. The main result of the present paper provides a positive answer to the open question of [GP92] and extends McNaughton’s Theorem to recognizable real trace languages. More precisely, we show the equivalence between the family of recognizable real trace languages and the family of real trace languages which can be accepted by a deterministic asynchronous cellular Muller automaton. In fact, all our results have a natural extension to complex traces. This is not done here for sake of simplicity and will be done elsewhere.

The paper is organized as follows. Section 2 provides some basic notions and notations. We also recall some definitions and facts about recognizable infinitary word and trace languages. Section 3 gives first a technical lemma which allows to follow the approach of Perrin/Pin [PP91] to McNaughton’s Theorem. We define deterministic real trace languages and show as the main result of this section that the family of recognizable real trace languages is equivalent to the Boolean closure of deterministic languages. The results we obtain are a proper generalization of the analogous results in the word case. Based on the foregoing result, we show in Section 4 that the family of recognizable real trace languages coincides with the family of languages accepted by some deterministic asynchronous cellular Muller automaton. In fact, this kind of automaton is a special form of so-called I-diamond automata, which play an important role in the case of finite traces. In Section 5 we give a characterization of Muller I-diamond automata accepting closed languages. This is related to the notion of trace automata introduced by Gastin/Petit [GP91]. We also consider the complexity of deciding this characterization.

2 Preliminaries

2.1 Basic Notions

We denote by (Σ, D) a finite dependence alphabet, with Σ being a finite alphabet and D ⊆ Σ × Σ a reflexive and symmetric relation called dependence relation. The complementary relation I = (Σ×Σ)\D is called independence relation. Let also D(a) = {b ∈ Σ | (a, b) ∈ D}.

The monoid of finite traces, IM(Σ, D), is defined as a quotient monoid with respect to the congruence relation induced by I, i.e., IM(Σ, D) = Σ^{∗}/{ ab = ba | (a, b) ∈ I }. Traces can be identified with their dependence graph, i.e., with (isomorphism classes of) labelled, acyclic, directed graphs [V, E, λ], where V is a set of vertices labelled by λ : V → Σ and E is a set of edges with the property that E ∪ E^{−1} ∪ id_{V} = λ^{−1}(D). This notion can be extended to infinite dependence graphs. We denote the set of infinite dependence graphs with a countable set of vertices V such that λ^{−1}(a) is well-ordered for all a ∈ Σ, by G(Σ, D). The requirement that any subset of vertices with the same label should be well-ordered, allows to represent the vertices as pairs (a, i), with a ∈ Σ and i a countable ordinal. Note that G(Σ, D) is a monoid with respect to the operation [V_{1}, E_{1}, λ_{1}][V_{2}, E_{2}, λ_{2}] = [V, E, λ], where [V, E, λ] is the disjoint union of [V_{1}, E_{1}, λ_{1}] and [V_{2}, E_{2}, λ_{2}] together with new edges (v_{1}, v_{2}) ∈ V_{1} × V_{2}, whenever (λ_{1}(v_{1}), λ_{2}(v_{2})) ∈ D holds. The neutral element is the empty graph [∅, ∅, ∅]. The concatenation is immediately extendable to infinite products. Let (g_{n})_{n≥0} ⊆ G(Σ, D), then g = g_{0}g_{1} … ∈ G(Σ, D) is defined as the disjoint union of the g_{n}, together with new edges from g_{n} to g_{m} for n < m between vertices with dependent labels. Thus, we can now define for any L ⊆ G(Σ, D) the ω-iteration as L^{ω} = { g_{0}g_{1} … | g_{n} ∈ L, ∀n ≥ 0 }.

We denote by Σ^{ω} the set of infinite words over the alphabet Σ (i.e., mappings from IN to Σ), and by Σ^{∞} the set of all words Σ^{∗} ∪Σ^{ω}. The canonical mapping φ : Σ^{∗} → IM(Σ, D) can be extended to Σ^{∞}, i.e., φ : Σ^{∞} → G(Σ, D). The image φ(Σ^{∞}) ⊆ G(Σ, D) is called the set of real traces and is denoted by IR(Σ, D). In other words, real traces can be identified with (in)finite graphs where every vertex has finitely many predecessors. Observe that IR(Σ, D) is not a submonoid of G(Σ, D), since, in general, φ commutes neither with concatenation nor with ω-iteration (if L, K ∈ Σ^{∞}, then φ(LK) = φ(L)φ(K) and φ(L^{ω}) = (φ(L))^{ω} hold if and only if L does not contain any infinite word). In the following we will denote IR(Σ, D) (IM(Σ, D) respectively) by IR (IM respectively). A word language L ⊆ Σ^{∞} is said to be closed (with respect to (Σ, D)) if L = φ^{−1}φ(L) for the canonical mapping φ : Σ^{∞} → IR.

Let us give now some further basic notations related to finite traces. For t ∈ IM, we denote by alph(t) the set of letters occuring in t, and by |t|_{a}, a ∈ Σ, the number of a occuring in t. Moreover, alph(L) = ⋃_{t∈L} alph(t). We shall often use the abbreviation (t, u) ∈ I for alph(t) × alph(u) ⊆ I. The set of maximal elements of a finite trace t ∈ IM, denoted by max(t), is defined as the set of labels corresponding to the maximal vertices of the dependence graph of t, i.e., max(t) = {a ∈ Σ | ∃x ∈ Σ^{∗} : φ(xa) = t}.

For (in)finite traces the prefix order ≤ is given by u ≤ t if and only if there exists a trace s with t = us. We shall often make use of intersections of prefixes of a given (in)finite trace in the following way: if t ∈ IR, u ≤ t and v ≤ t, then (u ∩ v) ≤ t, too. Hereby is u ∩ v the trace obtained by intersecting the dependence graphs of u and v within the dependence graph of t, where the intersection is meant with respect to the labelled vertex sets of u, v. We use in the same sense the greatest lower bound ⊓ (the least upper bound ⊔) of a set X ⊆ IR, whenever it exists.

2.2 Recognizable word languages

The family of recognizable infinitary word languages, denoted by Rec(Σ^{∞}), can be defined by means of finite state automata with suitable acceptance conditions for infinite words (see [Tho90]). More precisely, let A = (Q, Σ, δ, q_{0}, F) be a (nondeterministic) finite automaton where Q is the (finite) set of states, δ ⊆ Q×Σ×Q is the transition relation, q_{0} is the initial state and F is the set of accepting states.

If π denotes an infinite path in A, then inf(π) is the set of states occuring infinitely often in π (we sometimes also use the notation inf(q, w), q ∈ Q, w ∈ Σ^{ω}, if A is deterministic. This refers to inf(π), where π is the unique path labelled by w and starting with the state q). An infinite word w is accepted by A as a Büchi automaton if there exists a transition path π of A labelled by w such that for some final state f ∈ F, f ∈ inf(π). For the Muller acceptance condition, we have additionally a set of state tables T ⊆ P(Q). An infinite word w is accepted by A as a Muller automaton if there is a path π labelled by w such that for some T ∈ T , inf(π) = T. Finite words are accepted by A in the usual way, by reaching a final state of F.

A language L ⊆ Σ^{∞} is called recognizable if it is accepted by some (nondeterministic) Büchi automaton. Furthermore, the well-known theorem of McNaughton [McN66] states that Rec(Σ^{∞}) coincides with the family of infinitary word languages accepted by deterministic Muller automata (see e.g. [Tho90]). Equivalently, we can define recognizable infinitary word languages by means of recognizing morphisms. We will not mention any details here, since we will provide the analogue definitions for infinitary trace languages. Finally, let us mention that for infinitary word languages Büchi’s theorem holds, i.e., Rec(Σ^{∞}) = Rat(Σ^{∞}), which allows us to denote the family of recognizable (rational) infinitary word languages simply as regular languages, Reg(Σ^{∞}).

2.3 Recognizable Real Trace Languages

One possible way to define recognizable infinitary trace languages, denoted by Rec(IR), is by recognizing morphisms [Gas91]. Let η : IM → S be a morphism to a finite monoid S. A real trace language L ⊆ IR is recognized by η if for any sequence (t_{n})_{n≥0} ⊆ IM the following holds:

t_{0}t_{1}t_{2} … ∈ L ⟹ η^{−1}η(t_{0}) η^{−1}η(t_{1}) η^{−1}η(t_{2}) … ⊆ L

An equivalent definition uses the syntactic congruence of Arnold ([Arn85]). For L ⊆ IR, two finite traces u, v ∈ IM are syntactically congruent if and only if :

∀x, y ∈ IM : x(uy)^{ω} ∈ L ⇔ x(vy)^{ω} ∈ L
∀x, y, z ∈ IM : xuyz^{ω} ∈ L ⇔ xvyz^{ω} ∈ L

We denote the syntactic congruence by ≡_{L} and consider the canonical morphism η : IM → Synt(L), where Synt(L) = IM/ ≡_{L}.

Now, for the family of recognizable real trace languages Rec(IR) the following equivalent characterizations exist (see [Gas91], [GP92]):

1. L ∈ Rec(IR).

2. φ^{−1}(L) ∈ Rec(Σ^{∞}).

3. There exists a morphism η : IM → S to a finite monoid S recognizing L. Moreover, in this case L = ⋃_{(s,e)∈P} η^{−1}(s) η^{−1}(e)^{ω} with

P = { (s, e) ∈ S^{2} | se = s, e^{2} = e and η^{−1}(s) η^{−1}(e)^{ω} ∩ L ≠ ∅ }.

4. The syntactic congruence ≡_{L} has finite index and η : IM → IM/ ≡_{L} recognizes L. Moreover, Synt(L) = Synt(φ^{−1}(L)).

5. L is accepted by a nondeterministic Büchi asynchronous cellular automaton, which will be defined below.

For the family of finitary recognizable trace languages, Zielonka introduced asynchronous and asynchronous cellular automata ([Zie87], [Zie89]) and he showed the deep result of the equivalence between Rec(IM) and the family of finitary trace languages accepted by some deterministic asynchronous cellular automaton (or deterministic asynchronous automaton). An asynchronous cellular automaton is a tuple A = ((Q_{a})_{a∈Σ}, (δ_{a})_{a∈Σ}, q_{0}, F) where for each a ∈ Σ, Q_{a} is a finite set of states, q_{0} ∈ ∏_{a∈Σ} Q_{a} is the initial state, F ⊆ ∏_{a∈Σ} Q_{a} is the set of final states and δ_{a} ⊆ (∏_{b∈D(a)} Q_{b}) × Q_{a} is the local transition relation. We will denote in the following ∏_{b∈A} Q_{b} (∏_{b∈A} q_{b}, resp.) by Q_{A} (q_{A}, resp.), where A ⊆ Σ.

The global transition relation Δ ⊆ Q_{Σ} × Σ × Q_{Σ} of A is defined by:

q′ ∈ Δ(q, a) ⇔ q′_{a} ∈ δ_{a}(q_{D(a)}) and
q′_{c} = q_{c}for all c ≠ a

This means for a global state q and a ∈ Σ that a next state q′ ∈ Δ(q, a) exists if and only if δ_{a}(q_{D(a)}) is not empty and in this case, the action of a changes merely the acomponent of q and the new value q′_{a} depends only on the b components of q, for b ∈ D(a). Thus, asynchronous cellular automata have the ability of parallel execution of independent actions. Note that this is a typical situation where common read is allowed, whereas writing operations are exclusive and every processor has his own writing domain (CROW).

In [GP92] acceptance conditions have been defined for infinite traces. More precisely, if we have an infinite path π = (q_{0}, a_{0}, q_{1}, a_{1}, …) in A, with q_{n} ∈ Q_{Σ} and a_{n} ∈ Σ for every n ≥ 0, then let inf_{a}(π) = { q_{a} ∈ Q_{a} | ∃^{∞}n s.t. q_{n,a} = q_{a} } denote the set of local a-states which occur infinitely often in π.

Then, an asynchronous cellular automaton viewed as a Büchi (Muller, resp.) automaton is given a set of tables T ⊆ ∏_{a∈Σ} P(Q_{a}) i.e., A = ((Q_{a})_{a∈Σ}, (δ_{a})_{a∈Σ}, q_{0}, F, T ). An infinite trace t ∈ IR is accepted by the Büchi (Muller, respectively) automaton if there exists a path π labelled by t (i.e., by any w ∈ φ^{−1}(t)) and a set T ∈ T such that inf_{a}(π) ⊇ T_{a} (inf_{a}(π) = T_{a}, respectively), for every a ∈ Σ. Note that the acceptance conditions are inherently local, thus being appropriate for this kind of automata with decentralized control. Finite traces are accepted in the usual way, by reaching a final state. With these definitions, Gastin/Petit showed the equivalence between Rec(IR) and the family of real trace languages which are accepted by some Büchi asynchronous cellular automaton (an analogous result holds for Büchi asynchronous automata) [GP92]. However the construction of Gastin/Petit was inherently nondeterministic and so far there is no way to modify their approach in order to obtain a deterministic automaton.

3 Algebraic Results on Recognizable Infinitary Trace Languages

Let L ∈ Rec(IR) be recognized by a morphism η : IM → S to a finite monoid S. We define:

IM_{s} = η^{−1}(s),  for s ∈ S
IP_{s} = IM_{s} \ IM_{s}IM_{+}, with IM_{+} = IM \ {1}

Thus, IM_{s} is the set of all finite traces mapped by η to s ∈ S and IP_{s} is the subset of IM_{s} having no proper prefix in IM_{s}. Moreover, we may assume that alph(t) = alph(t′) for all t, t′ ∈ IM with η(t) = η(t′) holds, since we may replace S by S × P(Σ), with the multiplication defined by (s, A)(s′, A′) = (ss′, A ∪ A′) and (1, ∅) as neutral element. Hence, alph(s) for s ∈ S is well-defined. It can also be viewed as an abbreviation for alph(IM_{s}).

From the theory of finite monoids we will need only basic tools, such as the quasi-order relation ≤_{R} defined as a ≤_{R} b if and only if aS ⊆ bS. Furthermore, let E(S) denote the set of idempotent elements of S, E(S) = { e ∈ S | e = e^{2} } and define the following partial order relation on E(S): f ≤ e if and only if ef = f (in fact, f ≤ e holds if and only if f ≤_{R} e). By f < e we mean f ≤ e and e ≰ f.

Back to infinite traces, the following notation will be used frequently:

Inf(A) = { t ∈ IR | alphinf(t) = A },
IR_{A} = { t ∈ IR | D(alphinf(t)) = D(A) } for A ⊆ Σ.

where for t ∈ IR, alphinf(t) denotes the set of letters occurring infinitely often in t. In particular, we denote by Inf(s) and IR_{s} for s ∈ S the sets Inf(A) and IR_{A} with A = alph(s).

Remark 3.1 Note that in the word case (i.e., D = Σ × Σ) we have IR_{A} = Σ^{ω}, for every ∅ ≠ A ⊆ Σ and IR_{∅} = Σ^{∗}. We prefer to use IR_{s} instead of Inf(s), since thereby we obtain the analogous results for infinite words as a special case of our results.

Definition 3.2 Let L ⊆ IM. We define \overrightarrow{L} := \{ t ∈ IR | t = ⊔Y with Y directed and Y ⊆ L }.

(A set Y ⊆ IM is called directed if for every t, t′ ∈ Y, there exists an upper bound which also belongs to Y.)

In analogy to infinitary word languages, a deterministic real trace language is a language of type \overrightarrow{L} ∩ IR_{A}, where L ∈ Rec(IM) and A ⊆ Σ.

Remark 3.3 If t ∈ \overrightarrow{L}, there exists a sequence t_{0} ≤ t_{1} ≤ … such that (t_{n})_{n≥0} ⊆ L and t = ⨆{ t_{n} | n ≥ 0 }.

Remark 3.4 i) Note that every deterministic language is recognizable. Clearly, IR_{A} ∈ Rec(IR), where A ⊆ Σ. Moreover, let η : IM → S be a morphism recognizing L. Then it is easy to check that \overrightarrow{L} = ⋃_{(s,e)∈P} IM_{s}IM_{e}^{ω} holds, with P given by P = \{ (s, e) | s ∈ η(L), se = s, e^{2} = e }. ii) The classical definition in the word case considers only infinite words. Here we have L ⊆ \overrightarrow{L}. According to our definition, we obtain the classical definition by the intersection \overrightarrow{L} ∩ Σ^{ω}. At least if one deals with traces our definition seems to be more natural. In fact for word languages L ⊆ Σ^{∞} one usually intersects with Σ^{∗} and with Σ^{ω} and investigates the finitary and infinitary part separately. For traces, these intersections are replaced by intersections with IR_{A} for A ⊆ Σ. It is also via these intersections how one can easily extend the result to complex traces.

The following technical proposition is an important tool for all our results. It gives a characterization of infinite traces which belong to the set \overrightarrow{LK}, for L, K ⊆ IM.

Proposition 3.5 Given (t_{n})_{n≥0}, (w_{n})_{n≥0} ⊆ IM such that { t_{n}w_{n} | n ≥ 0 } is an infinite, directed set and let x = ⨆{ t_{n}w_{n} | n ≥ 0 }. Then there exist a subsequence of indices (n_{i})_{i≥0} ⊆ IN and sequences of finite traces (s_{i})_{i≥0}, (u_{i})_{i≥0}, (v_{i})_{i≥0} ⊆ IM such that x = ⨆{ t_{n_{i}}w_{n_{i}} | i ≥ 0 } satisfying for i ≥ 0 the following conditions:

t_{n_{i}} = s_{0}u_{0} … s_{i−1}u_{i−1}s_{i},
w_{n_{i}} = v_{0} … v_{i−1}u_{i}v_{i}
and  (v_{i}, s_{j}u_{j}) ∈ I, for i < j.

Proof: Since { t_{n}w_{n} | n ≥ 0 } is directed, let (n_{i})_{i≥0} be a subsequence of indices such that t_{n_{i}}w_{n_{i}} ≤ t_{n_{i+1}}w_{n_{i+1}} for all i ≥ 0 and x = ⨆{ t_{n_{i}}w_{n_{i}} | i ≥ 0 }. Let us define inductively four sequences of finite traces (s_{i})_{i≥0}, (u_{i})_{i≥0}, (v_{i})_{i≥0}, (f_{i})_{i≥0} ⊆ IM. Consider first for i > 0 the following traces defined by intersecting subgraphs within the dependence graph of x ∈ IR:

\begin{matrix}s_{0,i} := t_{n_{0}} ∩ t_{n_{i}} & u_{0,i} := w_{n_{0}} ∩ t_{n_{i}} \\ f_{0,i} := t_{n_{0}} ∩ w_{n_{i}} & v_{0,i} := w_{n_{0}} ∩ w_{n_{i}}. \end{matrix}

Since there exist only finitely many different traces s_{0,i} (f_{0,i}, …), we may assume without loss of generality that s_{0,i} = s_{0} (f_{0,i} = f_{0}, …) for some s_{0}, f_{0}, u_{0}, v_{0} ∈ IM and for every i ≥ 0. Hence, t_{n_{0}} = s_{0}f_{0}, w_{n_{0}} = u_{0}v_{0} and (u_{0}, f_{0}) ⊆ I.

Assume that we already have determined s_{k}, u_{k}, v_{k}, f_{k} for k < i and that for all k < i ≤ l the following holds:

s_{k}, u_{k} ⊆ t_{n_{l}}, f_{k}, v_{k} ⊆ w_{n_{l}},
t_{n_{k}} = s_{0}u_{0} … s_{k−1}u_{k−1}s_{k}f_{k}, w_{n_{k}} = f_{0}v_{0} … f_{k−1}v_{k−1}u_{k}v_{k}
and t_{n_{k}}w_{n_{k}} = (s_{0}u_{0}f_{0}v_{0}) … (s_{k}u_{k}f_{k}v_{k}).

Hence, there exist r_{i}, q_{i} ∈ IM such that the following holds (see Fig. 1):

\begin{matrix}t_{n_{i}} = s_{0}u_{0} … s_{i−1}u_{i−1}r_{i} \\ w_{n_{i}} = f_{0}v_{0} … f_{i−1}v_{i−1}q_{i}. \end{matrix}

Let us now define s_{i}, u_{i}, f_{i}, v_{i} by switching to an appropriate subsequence of indices such that we have for all l > i:

\begin{matrix}s_{i} := r_{i} ∩ t_{n_{l}} & u_{i} := q_{i} ∩ t_{n_{l}} \\ f_{i} := r_{i} ∩ w_{n_{l}} & v_{i} := q_{i} ∩ w_{n_{l}}. \end{matrix}

(the intersections above of dependence graphs are defined again within the dependence graph of x). We obtain thus

\begin{matrix}t_{n_{i}} = s_{0}u_{0} … s_{i−1}u_{i−1}s_{i}f_{i} \\ w_{n_{i}} = f_{0}v_{0} … f_{i−1}v_{i−1}u_{i}v_{i}. \end{matrix}

[figure: s_{j}; u_{j}; f_{j}; v_{j}; s_{0}; u_{0}; f_{0}; v_{0}; s_{k}; u_{k}; f_{k}; v_{k}; s_{i−1}; u_{i−1}; f_{i−1}; v_{i−1}; r_{i}; q_{i}; …; …; …; …] Figure 1: t^{n_{i}} = s^{0}u^{0} … s^{i−1}u^{i−1}r^{i}, w^{n_{i}} = f^{0}v^{0} … f^{i−1}v^{i−1}q^{i}.

Since

t_{n_{i}}w_{n_{i}} = (s_{0}u_{0}f_{0}v_{0}) … (s_{i}u_{i}f_{i}v_{i})
= (s_{0}u_{0} … s_{i−1}u_{i−1}s_{i}f_{i})(f_{0}v_{0} … f_{i−1}v_{i−1}u_{i}v_{i})

we have for 0 ≤ k < j the following independence relations, since any dependence would imply in either case the existence of an edge from right to left within the dependence graph of x ∈ IR (see also Fig. 1):

(f_{k}v_{k}, s_{j}u_{j}) ∈ I
(f_{k}v_{k}, s_{j}f_{j}) ∈ I

In particular, these conditions imply (f_{k}, f_{j}) ∈ I for every k ≠ j and (v_{k}, s_{j}u_{j}) ∈ I for every k < j. The first property means that there exists some i_{0} ≥ 0 such that f_{i} = 1 for i ≥ i_{0}. Hence, by starting the sequence of indices with i_{0} and redefining s_{i_{0}} as s_{0}u_{0} … s_{i_{0}−1}u_{i_{0}−1}s_{i_{0}} and v_{i_{0}} as f_{0}v_{0} … f_{i_{0}−1}v_{i_{0}−1}v_{i_{0}} we may assume that f_{i} = 1 for every i ≥ 0.

Corollary 3.6 Given L, K ⊆ IM with K ∈ Rec(IM) such that KIM_{+}∩K = ∅. Let (t_{n})_{n≥0} ⊆ L, (w_{n})_{n≥0} ⊆ K with { t_{n}w_{n} | n ≥ 0 } be an infinite, directed set with x = ⨆{ t_{n}w_{n} | n ≥ 0 }. Let additionally D(alphinf(x)) = D(alph(K)).

Then there exist a subsequence of indices (n_{i})_{i≥0} ⊆ IN and sequences of finite traces (s_{i})_{i≥0}, (u_{i})_{i≥0} ⊆ IM such that x = ⨆{ t_{n_{i}}w_{n_{i}} | i ≥ 0 } and, for i ≥ 0:

t_{n_{i}} = s_{0}u_{0} … s_{i−1}u_{i−1}s_{i},
w_{n_{i}} = u_{i}.

Proof: According to Proposition 3.5, there exist sequences of finite traces (s_{i})_{i≥0}, (u_{i})_{i≥0}, (v_{i})_{i≥0} ⊆ IM such that x = ⨆{ t_{n_{i}}w_{n_{i}} | i ≥ 0 } and , for i ≥ 0:

t_{n_{i}} = s_{0}u_{0} … s_{i−1}u_{i−1}s_{i},
w_{n_{i}} = v_{0} … v_{i−1}u_{i}v_{i}
and  (v_{i}, s_{j}u_{j}) ∈ I, for i < j.

We will show that the conditions (w_{n_{i}})_{i≥0} ⊆ K with KIM_{+} ∩ K = ∅ and D(alphinf(x)) = D(alph(K)) allow us to take v_{i} = 1 for i ≥ 0.

Consider a morphism η : IM → S to a finite monoid S recognizing K and observe that we may assume without loss of generality that η(u_{i}) = η(u_{j}) for all i, j (in order to achieve this, we may have to take a subsequence of indices (m_{i})_{i≥0} such that η(u_{m_{i}}) = η(u_{m_{j}}) for all i, j and then redefine s_{m_{i}} as s_{m_{i−1}+1}u_{m_{i−1}+1} … s_{m_{i}} and v_{m_{i}} as v_{m_{i−1}+1}v_{m_{i−1}+2} … v_{m_{i}}, respectively).

We have v_{0} … v_{i−2}v_{i−1}u_{i} ≤ w_{n_{i}} ∈ K, v_{0} … v_{i−2}v_{i−1}u_{i} = v_{0} … v_{i−2}u_{i}v_{i−1} for every i ≥ 1 (since (v_{i−1}, u_{i}) ∈ I) and η(v_{0} … v_{i−2}u_{i}v_{i−1}) = η(v_{0} … v_{i−2}u_{i−1}v_{i−1}) (since η(u_{i}) = η(u_{i−1})), hence v_{0} … v_{i−2}v_{i−1}u_{i} ∈ K and thus v_{i} = 1 because traces in K have no proper prefix in K. Additionally, since (v_{0}, s_{n}u_{n}) ∈ I for n > 0, we have alph(v_{0}) ∩ D(alphinf(x)) = ∅. Hence, since alph(v_{0}) ⊆ alph(K), v_{0} ≠ 1 would imply D(alphinf(x)) ≠ D(alph(K)), thus contradicting the hypothesis. Hence,

\begin{matrix}t_{n_{i}} = s_{0}u_{0} … s_{i−1}u_{i−1}s_{i} and \\ w_{n_{i}} = u_{i}. \end{matrix}

The next proposition generalizes the corresponding result for infinitary word languages (see also [PP91]) and will play a crucial role in the proof of the main result of this section. Apparently, the result differs from the analogous one for infinitary word languages, since we have an additional information about the alphabet at infinity. Nevertheless, observe that for D = Σ × Σ, since IR_{e} = Σ^{ω} (if alph(e) ≠ ∅) we obtain indeed the result for Σ^{ω} as a special case of the next proposition (recall Rem. 3.1).

Proposition 3.7 Let S be a finite monoid, η : IM → S a morphism and s, e ∈ S such that se = s and e ∈ E(S). Then we have the following inclusions:

IM_{s}IM_{e}^{ω} ⊆ \overrightarrow{IM_{s}IP_{e}} ∩ IR_{e} ⊆ ⋃_{f≤e} IM_{s}IM_{f}^{ω}

Proof: The first inclusion is clear, since for every infinite trace u = u_{0}u_{1} … with u_{0} ∈ IM_{s} and u_{n} ∈ IM_{e} for n ≥ 1 we can choose some u′_{n} ∈ IP_{e} such that u′_{n} ≤ u_{n}, n ≥ 1. Hence, u = ⨆\{ u_{0}u_{1} … u_{n−1}u′_{n} | n ≥ 1 \} ∈ \overrightarrow{IM_{s}IP_{e}} ∩ IR_{e}.

Consider now u ∈ \overrightarrow{IM_{s}IP_{e}} ∩ IR_{e}, i.e., D(alphinf(u)) = D(alph(e)) and u = ⨆\{ t_{n}w_{n} | n ≥ 0, t_{n} ∈ IM_{s}, w_{n} ∈ IP_{e} }, with the righthand-side being a directed set. Corollary 3.6 yields some sequences (n_{i})_{i≥0} ⊆ IN, (s_{i})_{i≥0}, (u_{i})_{i≥0} ⊆ IM such that

t_{n_{i}} = s_{0}u_{0} … s_{i−1}u_{i−1}s_{i},
w_{n_{i}} = u_{i}.

and u = ⨆{ t_{n_{i}}w_{n_{i}} | i ≥ 0 }. We can apply Ramsey’s Theorem in the usual way ([PP91]) in order to obtain a factorization (m_{i})_{i≥0} of u,

u = (s_{0}u_{0}s_{1} … s_{m_{0}}) (u_{m_{0}}s_{m_{0}+1} … s_{m_{1}}) (u_{m_{1}}s_{m_{1}+1} … s_{m_{2}}) …

with η(u_{m_{i}}s_{m_{i}+1} … s_{m_{j}}) = f for some f ∈ E(S) and every 0 ≤ i < j, and η(s_{0}u_{0} … s_{m_{1}}) = t for some t ∈ S such that tf = t. It is obvious that t = s. Moreover, f ∈ η(u_{n})S = eS implies f ≤ e, so u ∈ IM_{s}IM_{f}^{ω} with f ≤ e.

Corollary 3.8 Let S be a finite monoid, η : IM → S a morphism and s, e ∈ S such that se = s and e ∈ E(S). Then we have:

1. IM_{e}^{ω} = \overrightarrow{IM_{e}IP_{e}} ∩ IR_{e}

2. ⋃_{f≤e} IM_{s}IM_{f}^{ω} = ⋃_{f≤e}(\overrightarrow{IM_{s}IP_{f}} ∩ IR_{f}).

Proof: (1) Let s = e in Proposition 3.7, hence sf = s means ef = e. Moreover, f ≤ e means ef = f, thus e = f and

IM_{e}^{ω} ⊆ \overrightarrow{IM_{e}IP_{e}} ∩ IR_{e} ⊆ IM_{e}^{ω}.

(2) We know

IM_{s}IM_{f}^{ω} ⊆ \overrightarrow{IM_{s}IP_{f}} ∩ IR_{f} ⊆ ⋃_{h≤f} IM_{s}IM_{h}^{ω},

hence,

⋃_{f≤e} IM_{s}IM_{f}^{ω} ⊆ ⋃_{f≤e}(\overrightarrow{IM_{s}IP_{f}} ∩ IR_{f}) ⊆ ⋃_{f≤e} ⋃_{h≤f} IM_{s}IM_{h}^{ω} ⊆ ⋃_{h≤e} IM_{s}IM_{h}^{ω}

with the last inclusion due to the transitivity of ≤.

The following lemma expresses a property of the set P_{L} = { (s, e) ∈ S^{2} | e ∈ E(S), se = s and IM_{s}IM_{e}^{ω} ∩ L ≠ ∅ } belonging to L ∈ Rec(IR). Two pairs (s, e), (s′, e′) ∈ S^{2} are called conjugated ([PP91]) if for some x, y ∈ S the equalities s′ = sx, e = xy and e′ = yx hold.

Lemma 3.9 Let L = ⋃_{(s,e)∈P_{L}} IM_{s}IM_{e}^{ω} be recognized by a morphism η : IM → S, with P_{L} as above. Then for every elements s, s′ ∈ S, e, e′ ∈ E(S) with (s, e), (s′, e′) ∈ P_{L}, the following holds: IM_{s}IM_{e}^{ω} ∩ IM_{s′}IM_{e′}^{ω} ≠ ∅ if and only if (s, e) and (s′, e′) are conjugated.

Proof: Since the direction from right to left is clear due to the definition of conjugated pairs and to IM_{s}, IM_{e}, IM_{s′}, IM_{e′} ≠ ∅, let us consider t ∈ IM_{s}IM_{e}^{ω} ∩ IM_{s′}IM_{e′}^{ω}, i.e., there exist t_{0} ∈ IM_{s}, (t_{n})_{n≥1} ⊆ IM_{e}, t′_{0} ∈ IM_{s′}, (t′_{n})_{n≥1} ⊆ IM_{e′} with t = t_{0}t_{1} … = t′_{0}t′_{1} . . .. Since e, e′ ∈ E(S) we may merge consecutive t_{n}’s (t′_{n}’s) and assume for every n ≥ 0:

t′_{0}t′_{1} … t′_{n} ≤ t_{0}t_{1} … t_{n} ≤ t′_{0}t′_{1} … t′_{n+1}

Let us define 2 sequences of finite traces (s_{n})_{n≥0}, (u_{n})_{n≥0} by setting:

t_{0}t_{1} … t_{n} = t′_{0}t′_{1} … t′_{n}s_{n},
t′_{0}t′_{1} … t′_{n+1} = t_{0}t_{1} … t_{n}u_{n}

This yields the following equations, due to the fact that IM is left-cancellative:

t_{n+1} = u_{n}s_{n+1}
t′_{n+1} = s_{n}u_{n} and
t = t′_{0}s_{0}u_{0}s_{1}u_{1} …

for every n ≥ 0 (t_{0} = t′_{0}s_{0}).

Observe also that we may assume that η(u_{0}) = η(u_{1}), since there must exist i < j with η(u_{i}) = η(u_{j}) (redefine s_{0} (s_{1}, respectively) as s_{0}u_{0} … s_{i} (as s_{i+1}u_{i+1} … s_{j}, respectively), and redefine s_{k}, u_{k} as s_{k−j+1}, u_{k−j+1}, for k > j. Since e, e′ ∈ E(S), we still have s = η(t′_{0}s_{0}), e = η(u_{0}s_{1}) and e′ = η(s_{1}u_{1}).).

Letting now x = η(u_{0}) and y = η(s_{1}) provides us the desired result, since:

s′ = η(t′_{0}t′_{1}) = η(t′_{0}s_{0}u_{0}) =
= η(t′_{0}s_{0})x = η(t_{0})x = sx,
e = η(t_{1}) = η(u_{0}s_{1}) = xy and
e′ = η(t′_{2}) = η(s_{1}u_{1}) =
= η(s_{1}u_{0}) = yx.

The next theorem is the main result of this section. It shows that every recognizable real trace language belongs to the Boolean closure of the family of deterministic languages. We obtain the well-known result for words as a special case of this theorem.

Theorem 3.10 Let L ∈ Rec(IR) be recognized by the morphism η : IM → S with S a finite monoid and P_{L} = { (s, e) ∈ S^{2} | se = s, e ∈ E(S), IM_{s}IM_{e}^{ω} ∩ L ≠ ∅ }. Then we have:

L = ⋃_{(s,e)∈P_{L}} (⋃_{f≤e}(\overrightarrow{IM_{s}IP_{f}} ∩ IR_{f}) \ ⋃_{f<e}(\overrightarrow{IM_{s}IP_{f}} ∩ IR_{f}))

Proof: Consider (s, e) ∈ P_{L} and fRe with f ∈ E(S). Then, by Lemma 3.9, (s, f) ∈ P_{L}, since (s, e) and (s, f) are conjugated with x = e and y = f (f = xy, e = yx, s = sx). Hence,

L = ⋃_{(s,e)∈P_{L}} IM_{s}IM_{e}^{ω} ⊆ ⋃_{(s,e)∈P_{L}} ⋃_{fRe} IM_{s}IM_{f}^{ω} ⊆ L,

where the first inclusion is due to eRe. We obtain thus

L = ⋃_{(s,e)∈P_{L}} ⋃_{fRe} IM_{s}IM_{f}^{ω}.

Furthermore, we have fRe if and only if ef = f and fe = e, hence if and only if f ≤ e and f ≮ e.

Moreover, if f < e holds, then

IM_{s}IM_{e}^{ω} ∩ IM_{s}IM_{f}^{ω} = ∅.  (1)

Otherwise, (s, e) and (s, f) would be conjugated (by Lemma 3.9) so there would exist some x, y ∈ S such that sx = s, e = xy, f = yx. This would imply for n ≥ 0:

e = e^{2} = xyxy = xfy =^{f<e} xefy = x^{n}e(fy)^{n}

and, since S is finite, there exist n, q ∈ IN, q ≠ 0, with z^{n+q} = z^{n} for every z ∈ S. In this case, we would obtain e ∈ fS, since e = x^{n}e(fy)^{n+q} = e(fy)^{q} = ef(yf)^{q−1}y ∈^{ef=f} fS. This means f ≮ e, thus leading to a contradiction.

We may now conclude the proof:

⋃_{fRe} IM_{s}IM_{f}^{ω} = ⋃_{f≤e,f≮e} IM_{s}IM_{f}^{ω}
=^{(1)} ⋃_{f≤e} IM_{s}IM_{f}^{ω} \ ⋃_{f<e} IM_{s}IM_{f}^{ω}
= ⋃_{f≤e} IM_{s}IM_{f}^{ω} \ ⋃_{f<e} ⋃_{g≤f} IM_{s}IM_{g}^{ω}
=^{3.8} ⋃_{f≤e}(\overrightarrow{IM_{s}IP_{f}} ∩ IR_{f}) \ ⋃_{f<e} ⋃_{g≤f}(\overrightarrow{IM_{s}IP_{g}} ∩ IR_{g})
= ⋃_{f≤e}(\overrightarrow{IM_{s}IP_{f}} ∩ IR_{f}) \ ⋃_{f<e}(\overrightarrow{IM_{s}IP_{f}} ∩ IR_{f})

Corollary 3.11 Rec(IR) is equivalent to the Boolean closure of the family of deterministic real trace languages.

Proof: Since the inclusion from right to left is clear due to the previous theorem, let us point out that both \overrightarrow{L}, L ∈ Rec(IM), and IR_{A}, A ⊆ Σ, are recognizable:

1. Let η : IM → S be a morphism recognizing L. Then it is easy to check that \overrightarrow{L} = ⋃_{(s,e)∈P} IM_{s}IM_{e}^{ω} holds, with P given by P = { (s, e) | s ∈ η(L), se = s, e^{2} = e }. Moreover, the righthand-side of the above equation is recognizable.

2. For A ⊆ Σ note that it is easy to construct for every a ∈ Σ a Büchi asynchronous cellular automaton A_{a} such that L(A_{a}) = {t ∈ IR|a ∈ alphinf(t)}, hence Inf(A) ∈ Rec(IR) and thus IR_{A} ∈ Rec(IR), for every A ⊆ Σ.

We conclude the proof by noting that Rec(IR) is closed under Boolean operations.

4 Deterministic Asynchronous Automata for Rec(IR)

In this section we will construct deterministic asynchronous cellular Muller automata for languages of the form \overrightarrow{L} with L ∈ Rec(IM). Since for every IR_{A}, A ⊆ Σ, one can clearly exhibit a deterministic asynchronous cellular Muller automaton, we will obtain at the end the equivalence between Rec(IR) and the family of languages accepted by deterministic asynchronous cellular Muller automata.

We begin with a lemma which shows that we may restrict ourselves to a particular type of \overrightarrow{L} with L ∈ Rec(IM). Roughly speaking, we are interested in \overrightarrow{L} where the alphabet at infinity A is the same for all traces and where for every infinite trace in \overrightarrow{L}, its (infinitely many) L-prefixes have exactly one maximal element for each connected component of A.

Lemma 4.1 Let A = ⋃_{i=1}^{k} A_{i} be a decomposition in connected components for A ⊆ Σ, i.e.,

A = ˙⋃A_{i}
(A_{i}, A_{j}) ∈ I  for i ≠ j and
A_{i} is connected for every i = 1, …, k.

Choose a fixed a_{i} ∈ A_{i} for each i and let IM_{A,i} (IP_{A,i} respectively) denote the following recognizable subsets of IM:

IM_{A,i} = { t | alph(t) = A_{i} and max(t) = {a_{i}} }
IP_{A,i} = IM_{A,i} \ IM_{A,i}IM_{+}

Then we have for L ⊆ IM:

\overrightarrow{L} ∩ Inf(A) = \overrightarrow{LIP_{A,1} … IP_{A,k}} ∩ Inf(A).

Proof: The proof is similar to the proof of Proposition 3.7. Let us consider u ∈ \overrightarrow{L}, alphinf(u) = A = ⋃_{i=1}^{k} A_{i}. Then there exists a factorization of u, u = u_{0}u_{1}u_{2} … with the property that alph(u_{n}) = A for every n ≥ 1 and u_{0}u_{1} … u_{n} ∈ L for all n ≥ 0. Let us denote for every i = 1, … k by u_{n,i} the A_{i} projection of u_{n} and define for n ≥ 1:

u′_{n,i} = ⊓{ t ∈ IM | t ≤ u_{n,i}u_{n+1,i} …, max(t) = {a_{i}}, alph(t) = A_{i} }

The existence of u′_{n,i} is guaranteed by the fact that A_{i} = alphinf(u_{0}u_{1,i}u_{2,i} …), with A_{i} being connected. We define thus k sequences (u′_{n,i})_{n≥1} ⊆ IP_{A,i} such that for every n ≥ 1, u_{0} … u_{n−1}u′_{n,1} … u′_{n,k} ∈ LIP_{A,1} … IP_{A,k} and u = ⨆{ u_{0} … u_{n−1}u′_{n,1} … u′_{n,k} |

n ≥ 1 \}. Hence, u ∈ \overrightarrow{LIP_{A,1} … IP_{A,k}} ∩ Inf(A).

For the converse direction, consider u = ⨆{ t_{n}w_{n} | t_{n} ∈ L, w_{n} ∈ IP_{A,1} … IP_{A,k}, n ≥ 0 } with alphinf(u) = A and let us apply Corollary 3.6 (IP_{A,1} … IP_{A,k} ∈ Rec(IM) and IP_{A,1} … IP_{A,k}IM_{+} ∩ IP_{A,1} … IP_{A,k} = ∅) in order to obtain a sequence of indices (n_{i})_{i≥0} and 2 sequences of finite traces (s_{n})_{n≥0}, (u_{n})_{n≥0} such that u = ⨆{ t_{n_{i}}w_{n_{i}} | i ≥ 0 } and

t_{n_{i}} = s_{0}u_{0}s_{1} … s_{i−1}u_{i−1}s_{i} ∈ L
w_{n_{i}} = u_{i} ∈ IP_{A,1} … IP_{A,k}.

Hence, u = s_{0}u_{0}s_{1}u_{1} … with s_{0}u_{0} … s_{i} ∈ L for every i ≥ 0 and thus, u ∈ \overrightarrow{L}.

Before stating the main theorem of this section, let us recall some important concepts of Zielonka’s construction of asynchronous cellular automata for Rec(IM), which we will need in our construction (see also [Die90], [CMZ89]).

The a-prefix (A-prefix, respectively) ∂_{a}(t) (∂_{A}(t), respectively) of a finite trace t has been defined as the minimal prefix of t containing all a (all letters a ∈ A, respectively), which occur in t. More precisely, for every a ∈ Σ, A ⊆ Σ and t ∈ IM,

∂_{a}(t) = ⊓{ u ≤ t | |t|_{a} = |u|_{a} }, ∂_{A}(t) = ⨆_{a∈A} ∂_{a}(t) (in particular ∂_{∅}(t) = 1).

Zielonka’s construction is based on the concept of asynchronous mapping (see e.g. [Die90], p. 49). It is a mapping φ : IM → Q to a set Q satisfying the following 2 conditions, for every t ∈ IM, a ∈ Σ and A, B ⊆ Σ:

• The value of φ(∂_{A∪B}(t)) is uniquely determined by φ(∂_{A}(t)) and φ(∂_{B}(t)).

• The value of φ(∂_{D(a)}(ta)) is uniquely determined by φ(∂_{D(a)}(t)) and by a.

Given an asynchronous mapping φ : IM → Q and a set R ⊆ Q, then an asynchronous cellular automaton A = (Q^{Σ}, δ, q_{0}, F) with the following partial transition function accepts φ^{−1}(R):

\begin{matrix}δ : Q^{Σ} × IM → Q^{Σ}, \\ δ((φ(∂_{b}(t)))_{b∈Σ}, a) = (φ(∂_{b}(ta)))_{b∈Σ} \end{matrix}

(It is easy to check that δ is well-defined and satisfies the requirement for the partially defined transition function of an asynchronous cellular automaton, see e.g. [Die90], Prop. 2.4.4). The initial state of A is q_{0} = (φ(1), …, φ(1)) and F is given by F = { (φ(∂_{a}(t)))_{a∈Σ} | φ(t) ∈ R }. Moreover, we have δ(q_{0}, t) = (φ(∂_{a}(t)))_{a∈Σ}. Finally, suppose we are given a finitary recognizable language K ⊆ IM recognized by a morphism η : IM → S onto a finite monoid S. Then, Zielonka’s construction of an asynchronous cellular automaton accepting K provides an asynchronous mapping φ : IM → Q to a finite set Q and a mapping π : Q → S such that η = π ∘ φ. A crucial feature of the construction is the fact that the global state of the asynchronous cellular automaton based on φ which is reached after having read a finite trace t, can be reconstructed by using the local states corresponding to the maximal elements of t: since t = ∂_{max(t)}(t) holds, we have φ(t) = φ(∂_{max(t)}(t)), which means that φ(t) is exactly determined by { φ(∂_{a}(t)) | a ∈ max(t) } (since φ is an asynchronous mapping).

Theorem 4.2 Let L ∈ Rec(IM) be a recognizable finitary trace language. Then \overrightarrow{L} can be recognized by a deterministic asynchronous cellular Muller automaton.

Proof: Since we have

\overrightarrow{L} = ⋃_{A⊆Σ}(\overrightarrow{L} ∩ Inf(A))
=^{4.1} ⋃_{A⊆Σ}(\overrightarrow{LIP_{A,1} … IP_{A,k}} ∩ Inf(A)),

with IP_{A,1}, … IP_{A,k} depending on A and defined as in the previous lemma, it will suffice to

construct a deterministic Muller automaton accepting \overrightarrow{LIP_{A,1} … IP_{A,k}} ∩ Inf(A). Let η : IM → S be a morphism to a finite monoid recognizing LIP_{A,1} … IP_{A,k}, and let φ : IM → Q be the asynchronous mapping to the finite set Q such that there exists a mapping π with η = π ∘ φ. Finally, consider the deterministic asynchronous cellular automaton A′ = ((Q′_{a})_{a∈Σ}, (δ′_{a})_{a∈Σ}, q′_{0}, F) accepting LIP_{A,1} … IP_{A,k}, which is obtained by Zielonka’s construction. In particular, we have δ′(q′_{0}, t) = (φ(∂_{a}(t)))_{a∈Σ}, for every t ∈ IM, a ∈ Σ. Furthermore, consider for every f ∈ F the language

L_{A,f} = { t ∈ IR | alphinf(t) = A, t = ⨆{ t_{n} | n ≥ 0 } with t_{0} ≤ t_{1} ≤ … infinite,
t_{n} ∈ LIP_{A,1} … IP_{A,k} and δ′(q′_{0}, t_{n}) = f, for every n ≥ 0 }

Clearly, \overrightarrow{LIP_{A,1} … IP_{A,k}} ∩ Inf(A) = ⋃_{f∈F} L_{A,f} holds, since \overrightarrow{K_{1} ∪ K_{2}} = \overrightarrow{K_{1}} ∪ \overrightarrow{K_{2}}, for K_{1}, K_{2} ⊆ IM. Therefore, it suffices to construct a deterministic asynchronous cellular Muller automaton A = ((Q_{a})_{a∈Σ}, (δ_{a})_{a∈Σ}, q_{0}, T ) accepting L_{A,f}. Let us define for a ∈ Σ:

Q_{a} = Q′_{a} × ZZ/2ZZ
δ_{a}((q, i)_{D(a)}) = (δ′_{a}(q_{D(a)}), i_{a} + 1)
q_{0} = (q′_{0}_{a}, 0)_{a∈Σ}

The ZZ/2ZZ component of the local states of A is used in order to distinguish whether a letter belongs or not to the alphabet at infinity, since we have δ_{a}(s_{D(a)}) ≠ s_{a}, for every s_{a} ∈ Q_{a}, a ∈ Σ. Thus, |inf_{a}(t)| ≥ 2 if and only if a ∈ alphinf(t), for each a ∈ Σ. We now define the table T :

T = (T_{a})_{a∈Σ} ∈ T if and only if for some i_{a} ∈ ZZ/2ZZ
T_{a} = {(f_{a}, i_{a})} for a ∈ Σ \ A,
(f_{a}, i_{a}) ∈ T_{a} and |T_{a}| ≥ 2, for a ∈ A

Let us consider t ∈ L_{A,f} with alphinf(t) = A, t = ⨆{ t_{n} | n ≥ 0 }, t_{0} ≤ t_{1} ≤ … infinite, t_{n} ∈ LIP_{A,1} … IP_{A,k} and δ′(q′_{0}, t_{n}) = f, for every n ≥ 0. Clearly, we can assume alph(t_{n}) = A for n ≥ 1, hence we have for every a ∉ alphinf(t), inf_{a}(t) = { δ(q_{0}, t_{0})_{a} } = { (δ′(q′_{0}, t_{0})_{a}, i_{a}) } = { (f_{a}, i_{a}) } for some i_{a} ∈ ZZ/2ZZ. Furthermore, if a ∈ alphinf(t), then |inf_{a}(t)| ≥ 2. Additionally, δ′(q′_{0}, t_{n}) = f implies δ(q_{0}, t_{n})_{a} = (f_{a}, i_{a}) for some i_{a} ∈ ZZ/2ZZ and infinitely many n. Thus, (f_{a}, i_{a}) ∈ inf_{a}(t) for some i_{a} ∈ ZZ/2ZZ, a ∈ A. Hence, there exists some T ∈ T by which t is accepted. Conversely, let t ∈ L(A) be accepted by T ∈ T . Clearly, alphinf(t) = { a ∈ Σ | |T_{a}| ≥ 2 } = A, so let us factorize t as t = t_{0}t_{1} … such that for some i_{a} ∈ ZZ/2ZZ, a ∈ Σ:

alph(t_{n}) = A  for n ≥ 1,
δ(q_{0}, t_{0}t_{1} … t_{n})_{a} = (f_{a}, i_{a})  for a ∈ (Σ \ A) ∪ {a_{1}, …, a_{k}} and n ≥ 0,
max(t_{0} … t_{n}) ∩ A = {a_{1}, …, a_{k}} for n ≥ 0.

(such a factorization exists because of the definition of the table T together with a_{i} ∈ A_{i}, with (A_{i}, A_{j}) ∈ I, for i ≠ j). We will show that t_{0}t_{1} … t_{n} ∈ LIP_{A,1} … IP_{A,k}, n ≥ 0. Evidently, δ′(q′_{0}, t_{0} … t_{n})_{a} = f_{a}, for a ∈ (Σ \ A) ∪ {a_{1}, …, a_{k}}, n ≥ 0. From the definition of A′, we know f = (φ(∂_{a}(u)))_{a∈Σ} for some u ∈ LIP_{A,1} … IP_{A,k}. Note also that max(u) ∩ A = {a_{1}, …, a_{k}} and that for every n ≥ 0, a ∈ (Σ \ A) ∪ {a_{1}, …, a_{k}} the following holds:

(δ′(q′_{0}, t_{0} … t_{n})_{a} =) φ(∂_{a}(t_{0} … t_{n})) = φ(∂_{a}(u)) (= f_{a})

Since max(u), max(t_{0} … t_{n}) ⊆ (Σ \ A) ∪ {a_{1}, … a_{k}}, the observation made before we stated the theorem yields φ(t_{0} … t_{n}) = φ(u), hence η(t_{0} … t_{n}) = η(u), thus implying t_{0} … t_{n} ∈ LIP_{A,1} … IP_{A,k}.

We can now state the generalization of McNaughton’s theorem for infinitary trace languages, which is the main result of the paper.

Corollary 4.3 The family of recognizable real trace languages is equivalent to the family of languages, which are accepted by deterministic asynchronous cellular Muller automata.

Proof: The inclusion from left to right is due to Theorems 3.10, 4.2. The other way round, if L ⊆ IR is accepted by a (deterministic) asynchronous cellular Muller automaton A = ((Q_{a})_{a∈Σ}, (δ_{a})_{a∈Σ}, T ), then L can be expressed as a Boolean combination of languages accepted by Büchi asynchronous cellular automata (we assumed without loss of generality that L contains no finite traces):

L = ⋃_{T ∈T} (L(A^{B}) ∩ ⋂_{a∈Σ, q_{a}∈Q_{a}\T_{a}} \overline{L(A_{q_{a}})}),

with A^{B} being defined as A but as a Büchi automaton. A_{q_{a}} denotes a Büchi asynchronous cellular automaton with table containing every T′ ⊆ ∏_{b∈Σ} P(Q_{b}) with T′_{a} = {q_{a}}.

5 Deterministic I-diamond Muller automata

The rest of the paper can be read independently of the first part. It can also be omitted if the reader is interested only in the existence of deterministic automata. We have included this section in this paper since due to the previous section we know for the first time that every closed recognizable language of Σ^{ω} can be recognized by some deterministic I-diamond Muller automaton. We also think that complexity questions have not been paid much attention so far in trace theory.

Let M be any monoid, then the classical definition [Eil74] defines a language L ⊆ M to be recognizable if it is accepted by some deterministic M-automaton. In the case of M = IM = IM(Σ, D) an IM-automaton A is the same as a deterministic finite automaton A = (Q, δ, q_{0}, F) over Σ which satisfies the I-diamond property (see also Fig. 2):

∀q ∈ Q, (a, b) ∈ I : q · ab = q · ba

In some sense I-diamond finite automata do not accept traces directly, but they accept

[figure: a; b; b; a; q_{1}; q_{2}; q_{3}; q_{4}; ∀(a, b) ∈ I :]

Figure 2: The I-diamond property

any representing word. So they accept closed languages.

In this section we will show that we can define a natural class of I-diamond Muller automata which accept exactly the family of recognizable real trace languages. More precisely this class will accept the closed regular languages of Σ^{∞}.

First, let us show that the I-diamond property does not ensure that the accepted language is closed. This is well-known and the following example is due to Gastin/Petit.

Example 5.1 Let (Σ, D) = a − c − b and see Fig. 3:

Any state can be initial, say state q_{1} is initial. For the Muller table we take only one entry which consists of all states T = {q_{1}, q_{2}, q_{3}, q_{4}}. Then the automaton A is I-diamond

[figure: A :; c; q_{1}; q_{2}; q_{4}; q_{3}; a; a; b; b] Figure 3:

and in fact even the restriction to T is I-diamond. However L(A) is not closed. We have (abcbac)^{ω} ∈ L(A), but (abc)^{ω} ∉ L(A). The next example is due to Klaus Reinhardt. It shows an even worse behavior of I-diamond Muller automata. In general, it is not true that the closure [L(A)] ⊆ Σ^{∗} is regular. This is a significant difference to the Büchi-acceptance condition where [L(A)] can be shown to be always regular.

Example 5.2 Let (Σ, D) = a − c − b as above,

[figure: A :; a; b; a; b; b; a; c; c; 1; 2; 3; 4]

Figure 4: T = {T } with T = {2, 3, 4}, q_{0} = {3}

The automaton is I-diamond and we have L(A) ⊆ Σ^{∗}((ba)^{∗}cc)^{ω}. The language L(A) is not closed and its closure [L(A)] is not regular anymore, since for [L(A)] ∩ ({a, b}^{∗}cc)^{ω} between any two cc there is an equal number of a and b.

It is clear from the examples above that we need some restriction of the tables in order to accept closed languages. We will give these restrictions for reduced tables, only.

Definition 5.3 Let A = (Q, δ, q_{0}, T ) be a Muller automaton. The table T is called reduced if for every T ∈ T there is some u ∈ Σ^{ω} such that in inf(q_{0}, u) = T.

It is trivial to verify that every table can effectively be reduced. From our main result of the previous section we immediately obtain the following result.

Corollary 5.4 Let L ∈ Rec(IR) be a recognizable real trace language. Then there exists a deterministic I-diamond Muller automaton with reduced table accepting the closed language φ^{−1}(L) ∩ Σ^{ω} for the canonical mapping φ : Σ^{∞} → IR.

The syntactic condition of the table satisfied by the automaton above will be established in the next proposition. For this we use the following definition.

Definition 5.5 Let A = (Q, δ, q_{0}, T ) be a Muller automaton.

i) For q ∈ Q, v ∈ Σ^{∗} we define τ(q, v) = { qu | u is a prefix of v }. Thus, τ(q, v) is the set of states visited on the path starting by q and labelled with v. ii) The table T is called closed if for all T ∈ T , q ∈ T and v ∈ Σ^{∗} such that qv = q and T = τ(q, v) the following condition holds: if w ∈ Σ^{∗} denotes the same trace as v, then we have τ(q, w) ∈ T .

The next proposition is a special case of [GP91].

Proposition 5.6 (Gastin/Petit) Let A = (Q, δ, q_{0}, T ) be a deterministic I-diamond Muller automaton where T is reduced. Then A accepts a closed language if and only if the table T is closed.

It is also stated in [GP91] that it is effectively decidable whether a reduced table is closed. However the decision procedure of [GP91] is based on the observation that the path length can be bounded. This does not yield any practical algorithm. Here we provide a polynomial time algorithm, more precisely we show the NL completeness of the decision procedure.

Proof: Assume that the accepted language L(A) is closed and let T ∈ T . Since T is reduced there are u, v ∈ Σ^{∗}, q ∈ Q such that q_{0}u = q, qv = q, and τ(q, v) = T. Let w ∈ Σ^{∗} be any word which denotes the same trace as v. Then we have uw^{ω} ∈ L(A) since uv^{ω} ∈ L(A) and L(A) is closed. Since the automaton is deterministic I-diamond we have qw = q and therefore inf(q_{0}, uw^{ω}) = τ(q, w). Hence we must have τ(q, w) ∈ T .

For the other direction assume that the table T is closed. We show that ab ≡ ba for all (a, b) ∈ I, where ≡ is Arnold’s syntactic congruence of L(A).

Let uabvw^{ω} ∈ L(A) and (a, b) ∈ I. Since the automaton is I-diamond we have q_{0}uabv = q_{0}ubav and hence ubavw^{ω} ∈ L(A). Finally, consider u(abv)^{ω} ∈ L(A) for some u, v ∈ Σ^{∗}, (a, b) ∈ I. Then there exist r, s ≥ 0 such that q_{0}u(abv)^{r} = q, q(abv)^{s} = q and inf(q_{0}, u(abv)^{ω}) = τ(q, (abv)^{s}) ∈ T . Since T is closed, we have τ(q, (bav)^{s}) ∈ T and it follows u(bav)^{ω} ∈ L(A). Hence ab ≡ ba for all (a, b) ∈ I. By [DGP91][Thm. 2.6] it follows that L(A) is closed.

Remark 5.7 One can verify directly that the closure of T implies the closure of L(A). However, this is more involved since in some sense one has to redo the proof of [DGP91][Thm. 2.6].

The proposition above answers completely the question which deterministic I-diamond Muller automata accept closed languages. It is not difficult to see that we can decide whether a table is closed. However, in order to decide this efficiently we give another characterization of closed tables.

Theorem 5.8 Let A = (Q, δ, q_{0}, T ) be a deterministic I-diamond Muller automaton where T is reduced. Then T is closed if and only if the following two conditions hold.

1. For all T ∈ T , q ∈ Q, (a, b) ∈ I such that q, qa, qab ∈ T, we have (T ∪ {qb}) ∈ T , too.

2. For all T ∈ T , q ∈ Q, (a, b) ∈ I such that q, qa, qab ∈ T, we have ((T \ {qa}) ∪ {qb}) ∈ T , too, if τ(qab, v) = (T \ {qa}) ∪ {qb} for some v ∈ Σ^{∗} with qabv = q.

Proof: Assume that T is closed. Let T ∈ T , (a, b) ∈ I such that q, qa, qab ∈ T. Since T is reduced we find u, v, w ∈ Σ^{∗} such that q_{0}u = q, qv = q, τ(q, v) = T, qabw = q, and τ(q, abw) ⊆ T. Then we have τ(q, vabw) = T and hence τ(q, vbaw) = (T ∪ {qb}) ∈ T . Furthermore, if τ(qab, v) = (T \ {qa}) ∪ {qb} for some q ∈ T, v ∈ Σ^{∗}, qabv = q, then we have τ(q, abv) = T ∪ {qb} and τ(q, bav) = (T \ {qa}) ∪ {qb}. Hence, since T ∪ {qb} ∈ T (Condition 1), we have (T \ {qa}) ∪ {qb} ∈ T .

For the other direction assume that 1. and 2. hold. Let T ∈ T , q ∈ T, v ∈ Σ^{∗} such that τ(q, v) = T and qv = q. Let w ∈ Σ^{∗} be a word which denotes the same trace as v. We have to show τ(q, w) ∈ T . Clearly, we may assume v = v_{1}abv_{2}, w = v_{1}bav_{2} for some (a, b) ∈ I. Replace q by q_{1} = qv_{1}, then we have τ(q, v_{1}abv_{2}) = τ(q_{1}, abv_{2}v_{1}) = T and τ(q, w) = τ(q_{1}, bav_{2}v_{1}). Depending on the case whether or not q_{1}a ∈ τ(q_{1}ba, v_{2}v_{1}) we conclude with 1. or 2. that τ(q, w) ∈ T .

• If q_{1}a ∈ τ(q_{1}ba, v_{2}v_{1}), then τ(q, w) = {q_{1}, q_{1}b} ∪ τ(q_{1}ba, v_{2}v_{1}) = T ∪ {q_{1}b} ∈ T (Condition 1).

• Otherwise, we have τ(q, w) = (T \ {q_{1}a}) ∪ {q_{1}b} ∈ T (Condition 2).

5.1 Complexity results

In this subsection we show that it is NL - complete to decide whether a language specified by a deterministic I-diamond Muller automaton is closed. By NL we denote the class of problems decidable in non-deterministic logarithmic space, NSPACE (log(n)). We freely use the fact that NL is closed under complementation, [Imm88], [Sze88] and that the graph accessibility problem (for maximal outdegree 2), 2-GAP, is NL - complete.

Proposition 5.9 It is decidable in deterministic log-space whether on input A = (Q, δ, q_{0}, T ), (Σ, D) the automaton is deterministic and I-diamond.

Proposition 5.10 It is NL - complete to decide given a deterministic I-diamond Muller automaton A = (Q, δ, q_{0}, T ) over (Σ, D) whether the table T is reduced.

Proof: The containment in NL is easy to see. The completeness follows by a straightforward reduction of 2-GAP to this problem.

The proposition above shows that the preprocessing used to check the hypothesis of Proposition 5.6 is already NL-complete. However, the interesting fact is that even if we get this preprocessing for free, the test whether the accepted language is closed, is still NL-complete.

Proposition 5.11 There is an NL-algorithm to decide given a deterministic I-diamond Muller automaton A = (Q, δ, q_{0}, T ) over (Σ, D), whether L(A) ⊆ Σ^{ω} is closed.

For the hardness we may even restrict us to a three letter alphabet.

Theorem 5.12 Let (Σ, D) = a − c − b. It is NL-hard to decide given a deterministic I-diamond Muller automaton A = (Q, δ, q_{0}, T ) where T is reduced whether L(A) is closed.

Proof: Consider an instance G = ({p, q, x_{1}, …, x_{n}}, E) of 2-GAP where we ask for a directed path from p to q. Of course we may assume that the edges of E are labelled with b, c such that the instance can viewed as a part of a deterministic automaton over {b, c}^{∗}. Furthermore, we may assume that there is exactly one outgoing edge labelled b from p and that q has no outgoing edge at all but one incomming edge labelled c. We introduce new vertices r, s and the following additional edges: (q, b, r), (r, a, p), (q, a, s), (s, b, p), (p, c, s), (s, c, q), (q, c, x_{i}), (x_{i}, c, p) for 1 ≤ i ≤ n (see Fig. 5).

[figure: q; p; s; r; x_{i}; …; …; b; a; a; b; c; c; c; c; c; b] Figure 5:

In fact, the construction is not completely finished since it may happen that some vertices x_{i} have now two outgoing edges both labelled c. This problem can easily be resolved by replacing (x_{i}, c, y)(x_{i}, c, y′) for y ≠ y′ by (x_{i}, c, x′_{i})(x′_{i}, b, y), (x′_{i}, c, y′) and new vertices x′_{i}. Let q be the initial state and T = {T_{1}, T_{2}} with T_{1} = Q = {r, s, p, q, x_{i}, x′_{i} | 1 ≤ i ≤ n}, T_{2} = T_{1}\{s}. Then it is clear that A = (Q, δ, q, T ) is a deterministic I-diamond automaton where T is reduced. However, by Theorem 5.8 the table is closed if and only there is a path from p to q in G.

6 Conclusion

In this paper we gave a characterization of recognizable real trace languages by deterministic asynchronous Muller automata, thus answering one of the main open problems about infinite traces, see e.g. [GP92]. We showed that classical results of the theory of recognizable infinitary word languages have a natural extension in the case of real traces. One open problem which arises is whether there exists a characterization of \overrightarrow{L} with L ∈ Rec(IM) (i.e., without intersecting with sets IR_{A}) by means of deterministic asynchronous Büchi automata.

Due to the main result, it is reasonable to study the class of deterministic I-diamond Muller automata which accept closed languages. We gave a decision criterion for this question and studied the complexity of the decision procedure. A similar characterization for (nondeterministic) Büchi automata is still open.

Acknowledgements: We thank Paul Gastin for fruitful discussions and Wiesław Zielonka who told us that independently he has developed similar ideas.

References

[Arn85] A. Arnold. A syntactic congruence for rational ω-languages. Theoret. Comput. Sci., 39:333–335, 1985.

[CF69] P. Cartier and D. Foata. Problèmes combinatoires de commutation et réarrangements. Lecture Notes in Computer Science. Springer, Berlin-Heidelberg-New York, 1969.

[CMZ89] R. Cori, Y. Métivier, and W. Zielonka. Asynchronous mappings and asynchronous cellular automata. Tech. rep. 89-97, LABRI, Univ. Bordeaux, 1989.

[DGP91] V. Diekert, P. Gastin, and A. Petit. Recognizable complex trace languages. In A. Tarlecki, editor, Proceedings of the 16th Symposium on Mathematical Foundations of Computer Science (MFCS’91), Kazimierz Dolny (Poland) 1991, number 520 in Lecture Notes in Computer Science, pages 131–140. Springer, Berlin-Heidelberg-New York, 1991. Full version: Rapport de Recherche 640 (1991), Université de Paris Sud.

[Die90] V. Diekert. Combinatorics on Traces. Number 454 in Lecture Notes in Computer Science. Springer, Berlin-Heidelberg-New York, 1990.

[Die91] V. Diekert. On the concatenation of infinite traces. In Choffrut C. et al., editors, Proceedings of the 8th Annual Symposium on Theoretical Aspects of Computer Science (STACS’91), Hamburg 1991, number 480 in Lecture Notes in Computer Science, pages 105–117. Springer, Berlin-Heidelberg-New York, 1991.

[Eil74] S. Eilenberg. Automata, Languages and Machines, volume I. Academic Press, New York and London, 1974.

[Gas91] P. Gastin. Recognizable and rational trace languages of finite and infinite traces. In Choffrut C. et al., editors, Proceedings of the 8th Annual Symposium on Theoretical Aspects of Computer Science (STACS’91), Hamburg 1991, number 480 in Lecture Notes in Computer Science, pages 89–104. Springer, Berlin-Heidelberg-New York, 1991.

[GP91] P. Gastin and A. Petit. Büchi (asynchronous) automata for infinite traces. Tech. rep., LRI, Université Paris-Sud, 1991.

[GP92] Paul Gastin and Antoine Petit. Asynchronous automata for infinite traces. In W. Kuich, editor, Proceedings of the 19th International Colloquium on Automata Languages and Programming (ICALP’92), Vienna (Austria) 1992, Lecture Notes in Computer Science. Springer, Berlin-Heidelberg-New York, 1992.

[GPZ91] P. Gastin, A. Petit, and W. Zielonka. A Kleene theorem for infinite trace languages. In J. Leach Albert et al., editors, Proceedings of the 18th International Colloquium on Automata Languages and Programming (ICALP’91), Madrid (Spain) 1991, number 510 in Lecture Notes in Computer Science, pages 254–266. Springer, Berlin-Heidelberg-New York, 1991.

[Imm88] Neil Immerman. Nondeterministic space is closed under complement. SIAM J. Computing, 17:935–938, 1988.

[Maz77] A. Mazurkiewicz. Concurrent program schemes and their interpretations. DAIMI Rep. PB 78, Aarhus University, Aarhus, 1977.

[Maz87] A. Mazurkiewicz. Trace theory. In W. Brauer et al., editors, Petri Nets, Applications and Relationship to other Models of Concurrency, number 255 in Lecture Notes in Computer Science, pages 279–324. Springer, Berlin-Heidelberg-New York, 1987.

[McN66] R. McNaughton. Testing and generating infinite sequences by a finite automaton. Information and Control, 9:521–530, 1966.

[PP91] D. Perrin and J.E. Pin. Mots Infinis. Technical Report, LITP 91.06, Université de Paris 6, 1991. Book to appear.

[Sze88] Robert Szelepcényi. A method of forced enumeration for nondeterministic automata. Acta Informatica, 26:279–284, 1988.

[Tho90] W. Thomas. Automata on infinite objects. In Jan van Leeuwen, editor, Handbook of theoretical computer science, pages 133–191. Elsevier Science Publishers, 1990.

[Zie87] W. Zielonka. Notes on finite asynchronous automata. R.A.I.R.O.-Informatique Théorique et Applications, 21:99–135, 1987.

[Zie89] W. Zielonka. Safe executions of recognizable trace languages by asynchronous automata. In A. R. Mayer et al., editors, Proceedings Symposium on Logical Foundations of Computer Science, Logic at Botik ’89, Pereslavl-Zalessky (USSR) 1989, number 363 in Lecture Notes in Computer Science, pages 278–289. Springer, Berlin-Heidelberg-New York, 1989.