Deterministic asynchronous automata for infinite traces^{∗}

Volker Diekert Anca Muscholl

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

Abstract

This paper shows the equivalence between the family of recognizable languages over infinite traces and the family of languages which are recognized by deterministic asynchronous cellular Muller automata. 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 I-diamond deterministic Muller automaton.

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.

∗This research has been supported by the ESPRIT Basic Research Action No. 6317 AS-MICS 2.

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. Recognizable subsets form a well-studied family in the context of both free partially commutative monoids and (in)finite sequences. They may be defined by means of saturating morphisms to a finite monoid or, more commonly, by means of recognizability with finite automata. A further approach is based on rational (c-rational respectively) expressions, whereby equivalent characterizations are given by Kleene’s and Büchi’s theorems for word languages (Ochmanski’s theorem for trace languages, respectively). Finally, recognizability is equivalent to definability in certain monadic second order theories. As regards recognizable real trace languages, there exist equivalent characterizations by means of recognizing morphisms [Gas91] and by c-rational expressions [GPZ91]. Concerning characterizations by finite automata, P. Gastin and A. Petit investigated asynchronous (cellular) automata for infinite traces [GP92]. This type of automaton has been defined by W. Zielonka [Zie87, Zie89], who showed that for finite traces, the recognizable languages are exactly the languages recognized by deterministic asynchronous (cellular) automata. Asynchronous (cellular) automata have a decentralized control, which allows the parallel execution of independent actions. This concurrent behaviour makes them appropriate for the recognition of trace languages. 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 (cellular) Büchi automata. The major open problem which arose and which we are going to solve here was a characterization by some kind of deterministic 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. (In the theory of recognizable word languages the theorem of Mc-Naughton states the equivalence between nondeterministic Büchi automata and deterministic Muller automata.) Concretely, we show the equivalence between the family of recognizable real trace languages and the family of real trace languages which can be accepted by deterministic asynchronous cellular Muller automata. 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 basic notions. We also recall some facts about recognizable infinitary word and trace languages. Section 3 gives first a technical proposition which allows to follow the approach of Perrin/Pin [PP92]^{1} to McNaughton’s Theorem. We show as the main result of this section that the family of recognizable real trace languages is equivalent to the Boolean closure of a family of languages, which in the word case coincides with the family of deterministic word 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 deterministic asynchronous cellular Muller automata. As asynchronous automata are a special form of so-called I-diamond automata, we directly obtain that recognizable, closed (w.r.t. the independence relation I) infinitary word languages can be accepted by deterministic I-diamond Muller automata. I-diamond automata are a much weaker model for concurrency. They have global states only and concurrency is expressed by interleaving, i.e., for a global state q and a pair (a, b) of independent actions we have q · ab = q · ba. Although this is a weaker model, no direct proof for the existence of deterministic I-diamond automata is known up to now.

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} and D(A) = ⋃_{a∈A} D(a) for A ⊆ Σ. 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 are congruence classes of words, and they can be identified with their dependence graph, i.e. with (isomorphism classes of) labelled, acyclic, directed graphs [V, E, λ], where V is any set of vertices labelled by λ : V → Σ and E is a set of edges with the property that E ∪ E^{−1} ∪ id_{V} = λ^{−1}(D). Given a trace t = [a_{1} ⋯ a_{n}] ∈ IM, a_{i} ∈ Σ for 1 ≤ i ≤ n, we obtain the dependence graph of t by taking first a set of n vertices V = {v_{1}, …, v_{n}}. Then we label node v_{i} with a_{i}, i.e. λ(v_{i}) = a_{i}, for 1 ≤ i ≤ n and we define the edge set by E = {(v_{i}, v_{j}) | i < j and (λ(v_{i}), λ(v_{j})) ∈ D}. The notion of dependence graph can be extended to infinite dependence graphs. We denote by G(Σ, D) the set of infinite dependence graphs with a countable set of vertices V such that λ^{−1}(a) is well-ordered for all a ∈ Σ. The requirement that any subset of vertices with the same label should be well-ordered, allows us to represent vertices as pairs (a, i), with a ∈ Σ and i a countable ordinal, where (a, i) represents the (i + 1)-th node labelled by the letter a. This is called the standard representation. 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 identity 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 let Σ^{∞} = Σ^{∗} ∪ Σ^{ω}. Languages L ⊆ Σ^{∞} are called infinitary word languages (whereas subsets of Σ^{∗} are called finitary languages). The canonical homomorphism φ : Σ^{∗} → IM(Σ, D) can be extended to a mapping φ : Σ^{∞} → 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 for example, a^{ω} ∈ IR(Σ, D), a ∈ Σ, but the concatenation in G(Σ, D) yields a nonreal graph, where one node is transfinite. In fact, φ 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. For t ∈ IR we denote by alph(t) the set of letters occurring in t, and by |t|_{a} ∈ IN ∪ {ω}, a ∈ Σ, the number of a occurring in t. By alphinf(t) we denote the set of letters occurring infinitely often in t, i.e., alphinf(t) = {a ∈ Σ | |t|_{a} = ω}. 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. For traces t_{1}, t_{2} we denote by t_{1} ⊓ t_{2} their greatest lower bound. Whenever it exists, the least upper bound of a set Y ⊆ IR w.r.t. the prefix ordering is denoted by ⊔Y. The best way to understand our formal proofs is perhaps the graphical interpretation of traces. As an example let us sketch the proof for every directed set of real traces having a least upper bound [GR91, Kwi90]. Consider each trace t in its standard representation with V = {(a, i) | 0 ≤ i < |t|_{a}} and E = {((a, i), (b, j)) | the (i + 1)^{th} a is before the (j + 1)^{th} b in any representing word of t}. Then, for two traces t_{1} = [V_{1}, E_{1}, λ_{1}], t_{2} = [V_{2}, E_{2}, λ_{2}] we may define t_{1} ∪ t_{2} by the set theoretical union of the dependence graphs. In general, t_{1} ∪ t_{2} will be no trace. However, this is the case if t_{1} ≤ t and t_{2} ≤ t for some t. Indeed, in this case there will be no cycles in the resulting graph. More general, if X ⊆ IR is directed, then the union ⋃_{t∈X} t is a well-defined dependence graph of some real trace and we obtain ⊔X = ⋃_{t∈X} t. Another useful application of the dependence graph view is the identification of factors. Assume that we can write t = u_{1}u_{2}u_{3} for some u_{1}, u_{2} ∈ IM and u_{3} ∈ IR. Then we can identify the factors u_{1}, u_{2} and u_{3} with subgraphs of t (called subtraces). This generalizes in a natural way to more factors. If we have t = u_{1} ⋯ u_{m} = v_{1} ⋯ v_{n}, then we can define factors w_{ij} for 1 ≤ i ≤ m and 1 ≤ j ≤ n by the intersections u_{i} ∩ v_{j} in the dependence graph of t. We obtain u_{i} = w_{i1} ⋯ w_{in} and v_{j} = w_{1j} ⋯ w_{mj}. Furthermore, an inspection of the dependence graph of t shows that there are no edges from w_{ij} to w_{kl} whenever i < k and j > l (i > k and j < l, resp.). Hence, alph(w_{ij}) × alph(w_{kl}) ⊆ I in this cases. This is the main idea behind various proofs given below. For the formal reasonings however, it is in most case sufficient to consider the special case m = n = 2, which is exactly the well-known Levi’s Lemma, see Lemma 3.5 below.

1This work is not broadly available yet. Nevertheless, we give all relevant proofs directly.

2.2 Recognizable word languages

The family of recognizable infinitary word languages, denoted by Rec(Σ^{∞}), can be defined by means of recognizing morphisms or equivalently, by finite state automata with suitable acceptance conditions for infinite words (see [Tho90]). Let A = (Q, Σ, δ, q_{0}, F_{0}) 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_{0} is the set of accepting states. Let π = (q_{0}, a_{0}, q_{1}, a_{1}, …) with q_{n} ∈ Q, a_{n} ∈ Σ and q_{n+1} ∈ δ(q_{n}, a_{n}), denote an infinite transition path in A. Then inf(π) is the set of states occurring infinitely often in π. A Büchi automaton is a finite automaton augmented by a state set F ⊆ Q, i.e. A = (Q, Σ, δ, q_{0}, F_{0}, F). Having two types of final states A recognizes infinitary languages as follows. Finite words are accepted by reaching a final state in F_{0}. An infinite word w is accepted by the Büchi automaton A if there exists a transition path π of A labelled by w, i.e. w = a_{0}a_{1} …, such that f ∈ inf(π) for some final state f ∈ F. For the Muller acceptance condition, we have a state table T ⊆ P(Q) instead of the state set F. An infinite word w is accepted by the Muller automaton A = (Q, Σ, δ, q_{0}, F_{0}, T ) if there is a path π labelled by w such that inf(π) = T for some T ∈ T . Finite words are accepted by A as above, by reaching a final state of F_{0}. A language L ⊆ Σ^{∞} is called recognizable if it is accepted by some nondeterministic Büchi automaton. Furthermore, deterministic Büchi automata do not suffice for characterizing Rec(Σ^{∞}). However, the well-known theorem of Mc-Naughton [McN66] shows that Rec(Σ^{∞}) coincides with the family of infinitary word languages accepted by deterministic Muller automata (see e.g. [Tho90]). Finally, let us mention that for infinitary word languages Büchi’s theorem holds, i.e., the family of recognizable languages is identical with the family defined by rational expressions over Σ using the operations union, concatenation, ∗-iteration, and ω-iteration.

2.3 Recognizable Real Trace Languages

One possible way to define the family of recognizable infinitary trace languages, denoted by Rec(IR), is by recognizing morphisms [Gas91]. Let η : IM → S be a morphism to a monoid S. A real trace language L ⊆ IR is recognized by η if for any sequence of finite traces (t_{n})_{n≥0} ⊆ IM the following saturation condition 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} is the syntactic monoid of L. The following definition summarizes some of the equivalent characterizations of Rec(IR) (see [Gas91], [GP92]).

Definition 2.1 A real trace language L is recognizable, L ∈ Rec(IR), if one of the following equivalent conditions holds:

1. There exists a morphism η : IM → S to a finite monoid S recognizing L.

(Moreover, L can be represented as L = ⋃_{(s,e)∈P} η^{−1}(s) η^{−1}(e)^{ω} with

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

2. φ^{−1}(L) ⊆ Σ^{∞} is a recognizable word language, i.e. φ^{−1}(L) ∈ Rec(Σ^{∞}).

3. The syntactic congruence ≡_{L} has finite index and η : IM → Synt(L) recognizes L.

(Moreover, we have Synt(L) = Synt(φ^{−1}(L)).)

4. L is accepted by a nondeterministic Büchi asynchronous cellular automaton (see the definition below).

Remark 2.2 For the first condition above note that if η : IM → S recognizes a language L, then we have for any s, e ∈ S: (η^{−1}(s) η^{−1}(e)^{ω} ∩ L ≠ ∅) ⟹ (η^{−1}(s) η^{−1}(e)^{ω} ⊆ L).

Languages L ⊆ IM of finite traces are called finitary in the following. For the family of finitary recognizable trace languages Rec(IM), W. Zielonka introduced the concept of asynchronous (cellular) automata ([Zie87], [Zie89]) and showed the deep result of the equivalence between Rec(IM) and the family of finitary trace languages accepted by deterministic asynchronous (cellular) automata. 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 local 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} ((q_{b})_{b∈A}, resp.) by Q_{A} (q_{A}, resp.), where A ⊆ Σ. In particular, for a ∈ Σ we mean by q_{D(a)} the local states tuple (q_{b})_{b∈D(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 a-component 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 (Concurrent Read Owner Write, CROW). In [GP92] a suitable counterpart of the Büchi and Muller acceptance conditions has been defined for infinite traces. Consider an infinite transition path π = (q_{0}, a_{0}, q_{1}, a_{1}, …) in A, with q_{n} ∈ Q_{Σ}, a_{n} ∈ Σ and q_{n+1} ∈ δ(q_{n}, a_{n}) for n ≥ 0. The acceptance conditions will concern the sets of local states which occur infinitely often in π. Consider for each a ∈ Σ the set of local a-states inf_{a}(π) = { q_{a} ∈ Q_{a} | q_{n,a} = q_{a} for infinitely many n }. If A is deterministic, then we will write directly inf_{a}(t) instead of inf_{a}(π), where t = φ(a_{0}a_{1} …). In order to accept infinite traces, an asynchronous cellular automaton is augmented by a table 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 A with a Büchi condition if there exist an infinite transition path π = (q_{0}, a_{0}, q_{1}, a_{1}, …) labelled by some representing word of t (i.e. t = φ(a_{0}a_{1} …) holds) and a set T ∈ T such that inf_{a}(π) ⊇ T_{a} for every a ∈ Σ. The automaton A accepts t ∈ IR with a Muller condition if there exist an infinite path π and a set T ∈ T as above with inf_{a}(π) = T_{a} for every a ∈ Σ. Thus, the difference is that the Muller condition specifies exactly the set of (local) states which have to be repeated infinitely often.

Finite traces are accepted in the usual way, by reaching a final state. Let us illustrate the acceptance mode by a very simple example:

Example 2.3 Let b, c ∈ Σ, b ≠ c and consider A = ((Q_{a})_{a∈Σ}, (δ_{a})_{a∈Σ}, q_{0}, F, T ) with

1. Q_{a} = {q_{0,a}} and δ_{a}(q_{D(a)}) = q_{0,a} for every q ∈ Q_{Σ} and a ≠ b, c.

2. For x ∈ {b, c} let Q_{x} = {q_{0,x}, q_{1,x}} and

δ_{x}(q_{D(x)}) = \{ \begin{matrix}q_{1,x} & if q_{x} = q_{0,x} \\ q_{0,x} & if q_{x} = q_{1,x} \end{matrix}

3. F = ∅.

4. T = {T } with T = (∏_{a∈Σ\{b,c}} Q_{a}) × Q_{b} × {q_{0,c}}.

Clearly we have using the Muller acceptance condition: L(A) = {t ∈ IR | b ∈ alphinf(t), |t|_{c} finite, even}, whereas using the Büchi condition, L(A) = {t ∈ IR | b ∈ alphinf(t), and (|t|_{c} = ω or |t|_{c} even)}. Note also that the family of languages accepted by deterministic asynchronous cellular Muller automata is closed under Boolean operations. Moreover, for every A ⊆ Σ we can exhibit deterministic asynchronous cellular Muller automata recognizing the sets Inf(A) := {t ∈ IR | alphinf(t) = A} resp. IR_{A} := {t ∈ IR | D(alphinf(t)) = D(A)} = ⋃_{B: D(B)=D(A)} Inf(B). It is enough to modify the automaton above correspondingly.

Note that the acceptance conditions are inherently local, thus being suitable for automata with decentralized control. Moreover, the word language accepted by asynchronous cellular automaton with the above acceptance conditions is closed [GP92], a property which we implicitly used in the definition of the acceptance of a trace. Gastin/Petit showed the equivalence between Rec(IR) and the family of real trace languages which are accepted by nondeterministic Büchi asynchronous cellular automata (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 construction (even considering different acceptance conditions) in order to obtain a deterministic automaton. The construction below is based on a totally different approach. In this paper we consider only asynchronous cellular Muller automata, due to their elementary internal structure, together with a simple construction allowing the transformation of asynchronous cellular Muller automata into equivalent asynchronous Muller automata. Therefore our results will hold for asynchronous Muller automata as well.

3 Algebraic Results on Recognizable Real Trace Languages

In this section we consider a trace language L ∈ Rec(IR) which is recognized by a homomorphism η : IM → S to a finite monoid S and we use the following notations:

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} consisting of traces having no proper prefix in IM_{s}. Throughout the whole section we will assume that η is surjective and that we have alph(t) = alph(t′) for all t, t′ ∈ IM with η(t) = η(t′). This can be easily achieved, since we may replace S by a submonoid of S × P(Σ), with the multiplication defined by (s, A)(s′, A′) = (ss′, A ∪ A′) and (1, ∅) as identity and where the morphism is replaced by t ↦ (η(t), alph(t)). Moreover, we define alph(s) for s ∈ S by alph(s) = alph(t) for some t ∈ η^{−1}(s). From the theory of finite monoids we will need only basic tools, such as the quasiorder relation ≤_{R} defined as a ≤_{R} b if and only if aS ⊆ bS and the equivalence relation R defined as aRb if and only if aS = bS. Furthermore, let E(S) denote the subset of S of idempotent elements, E(S) = { e ∈ S | e = e^{2} }. For s ∈ S define the partial order relation ≤ on the set {e ∈ E(S) | se = s} by f ≤ e if and only if ef = f (actually, f ≤ e is equivalent to f ≤_{R} e). By f < e we mean f ≤ e and e ≰ f. In fact, everytime we will use languages of the type IM_{s}IM_{e}^{ω} or IM_{s}IP_{e} we will suppose implicitly that the relations se = s and e ∈ E(S) hold. Back to infinite traces, recall the notations from the previous section

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

where for t ∈ IR, alphinf(t) is the set of letters occurring infinitely often in t. In particular, we denote by Inf(s) and IR_{s} respectively, for s ∈ S, the sets Inf(A) and IR_{A} respectively, 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_{∅} = Σ^{∗}. Therefore we prefer to use IR_{s} instead of Inf(s), since so we obtain the analogous results for infinite words as a special case of our results.

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

As shown in [GR91, Kwi90] every directed set of real traces admits a least upper bound, see also Section 2.1.

Definition 3.3 Let L ⊆ IM. We define \overrightarrow{L} := \{ t ∈ IR | t = ⊔Y for some directed Y ⊆ L \}.

Remark 3.4 i) The classical definition of \overrightarrow{L} in the word case considers only

infinite words. It corresponds to the intersection \overrightarrow{L} ∩ Σ^{ω} in our definition. Here we have L ⊆ \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 two parts separately. For traces, these intersections will be replaced by intersections with IR_{A} for A ⊆ Σ. It is also via these intersections how one can easily extend the results to complex traces. ii) Note that every \overrightarrow{L} with L ∈ Rec(IM) is recognizable. 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 = { (s, e) | s ∈ η(L), se = s, e^{2} = e }.

The following technical propositions represent important tools for all our results. We begin by recalling the well-known decomposition lemma (Levi’s Lemma) for traces:

Lemma 3.5 ([CP85]) Let t_{1}, t_{2}, x_{1}, x_{2} ∈ IM satisfying t_{1}x_{1} = t_{2}x_{2}. Then

t_{1} = pf, t_{2} = pg, x_{1} = gy, and x_{2} = fy

for p = t_{1} ⊓ t_{2} and some f, g, y ∈ IM such that alph(f) × alph(g) ⊆ I.

Lemma 3.6 Let (t_{n})_{n≥0} ⊆ IM be a sequence admitting a least upper bound. Then there exists an infinite index set J ⊆ IN such that (t_{i})_{i∈J} is an increasing sequence (w.r.t. the prefix order).

Proof. Since ⨆_{n≥0} t_{n} exists, let us consider for i < j the greatest lower bounds p_{i,j} := t_{i} ⊓ t_{j} and traces f_{i,j}, g_{i,j} such that according to Lemma 3.5 the following holds:

t_{i} = p_{i,j} f_{i,j}, t_{j} = p_{i,j} g_{i,j} and alph(f_{i,j}) × alph(g_{i,j}) ⊆ I

Fixing i clearly allows us to assume p_{i,j} = p_{i} (resp. f_{i,j} = f_{i}) for some p_{i} (resp. f_{i}) and every j > i. (This can be achieved by taking an appropriate (infinite) subsequence of indices.) Hence we may rewrite the above equations:

t_{i} = p_{i}f_{i}, t_{j} = p_{i} g_{i,j} and alph(f_{i}) × alph(g_{i,j}) ⊆ I

Observe now that p_{i} ≤ p_{j} for every i ≤ j, since by construction, p_{i} ≤ t_{j} and p_{i} ≤ t_{k}, for every k ≥ j. Thus, p_{i} ≤ p_{j} ( = t_{j} ⊓ t_{k} for every k ≥ j). Furthermore we have for every i < j:

t_{j} = p_{i} g_{i,j} = p_{j}f_{j}.

Together with alph(f_{j}) ⊆ alph(g_{i,j}) (since p_{i} ≤ p_{j}), this yields alph(f_{i})×alph(f_{j}) ⊆ I. Since Σ is a finite alphabet, this implies that f_{i} = 1 for all but finitely many i. By a further restriction of the index set such that f_{i} = 1 for every i ∈ J we obtain an (infinite) increasing sequence (t_{i})_{i∈J}. □

Remark 3.7 Note that the lemma above does not claim ⨆_{i∈J} t_{i} = ⨆_{n≥0} t_{n}. It is easy to find counterexamples. Consider Σ = {a, b, c}, D = {(a, a), (b, b), (c, c)} and

t_{n} = \{ \begin{matrix}a^{2}bc^{n} & for even n \\ ab^{2}c^{n} & for odd n \end{matrix}

Now one has ⨆_{n≥0} t_{n} = a^{2}b^{2}c^{ω}, but neither ⨆_{n≥0} t_{2n} = a^{2}bc^{ω} nor ⨆_{n≥0} t_{2n+1} = ab^{2}c^{ω} is equal to a^{2}b^{2}c^{ω}.

Proposition 3.8 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} 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, j the following conditions:

t_{n_{i}} = s_{0}u_{0} ⋯ s_{i−1}u_{i−1}s_{i},
w_{n_{i}} = u_{i}v_{0} ⋯ v_{i−1}v_{i}
and  alph(v_{i}) × alph(s_{j}u_{j}) ⊆ I, for i < j.

Proof. Since the set { t_{n}w_{n} | n ≥ 0 } is directed, we may assume by switching to an appropriate infinite subsequence of indices that t_{n}w_{n} ≤ t_{n+1}w_{n+1} for all n ≥ 0. Moreover, applying Lemma 3.6 allows us to consider (t_{n})_{n≥0} as an increasing sequence, too. Therefore, for 0 ≤ i < j we can define (x_{i,j})_{i,j≥0} ⊆ IM such that t_{j} = t_{i} x_{i,j}. By the left-cancellation property of IM the above relations yield w_{i} ≤ x_{i,j} w_{j}. Applying now Levi’s Lemma to this inequation we obtain traces u_{i,j}, s_{i,j}, y_{i,j} such that alph(s_{i,j}) × alph(y_{i,j}) ⊆ I and

w_{i} = u_{i,j} y_{i,j}, x_{i,j} = u_{i,j} s_{i,j}, y_{i,j} ≤ w_{j}.

As we are interested in an (infinite) subsequence of indices, for a fixed i ≥ 0 we may assume u_{i,j} = u_{i} and y_{i,j} = y_{i} for some u_{i}, y_{i} ∈ IM and for every i < j. Hence, we may rewrite the above relations as alph(s_{i,j}) × alph(y_{i}) ⊆ I and

w_{i} = u_{i}y_{i}, x_{i,j} = u_{i} s_{i,j}, y_{i} ≤ w_{j}.

Let us denote s_{i,i+1} by s_{i+1} and x_{i,i+1} by x_{i}, then we obtain using x_{i,j} = u_{i} s_{i,j},

x_{i,j} = x_{i}x_{i+1} ⋯ x_{j−1} = (u_{i}s_{i+1})(u_{i+1}s_{i+2}) ⋯ (u_{j−1}s_{j}) = u_{i} s_{i,j},

hence, s_{i,j} = s_{i+1}u_{i+1}s_{i+2} ⋯ u_{j−1}s_{j}. Together with the above alphabetical relation, this implies alph(y_{i}) × alph(s_{j}u_{j}) ⊆ I for every 0 ≤ i < j. Moreover, we know y_{i} ≤ w_{i+1} = u_{i+1}y_{i+1}, thus y_{i} ≤ y_{i+1}, for every i ≥ 0, since alph(y_{i}) × alph(u_{i+1}) ⊆ I. Let us define finally v_{i} by y_{i+1} = y_{i}v_{i+1} (and v_{0} = y_{0}).

[figure: s_{0}; u_{0}; v_{0}; s_{1}; u_{1}; v_{1}; s_{i−1}; u_{i−1}; v_{i−1}; s_{i}; u_{i}; v_{i}; …; …; t_{i}; w_{i}]

Figure 1: The factorization of t_{i}w_{i}, where w_{i} consists of the marked regions.

Summarizing our results we obtain alph(v_{i}) × alph(s_{j}u_{j}) ⊆ I for j > i ≥ 0, and (see Fig. 1)

t_{i} = t_{0}x_{0} ⋯ x_{i−1} = s_{0}u_{0}s_{1} ⋯ u_{i−1}s_{i} (with s_{0} := t_{0}),
w_{i} = u_{i}y_{i} = u_{i}v_{0}v_{1} ⋯ v_{i}.
□

Remark 3.9 By grouping factors together and appropriately renumbering we can even obtain the stronger independence relations alph(v_{i}) × alph(s_{j}u_{j}) ⊆ I, for i ≥ 0, j > 0. Yet we will not make use of this.

Example 3.10 Let (Σ, D) = a − b − c − d and consider the sequences (t_{n})_{n≥0}, (w_{n})_{n≥0} ⊆ IM defined by t_{n} = c(ba)(b^{2}a) ⋯ (b^{n}a)b and w_{n} = d^{n+1}b^{n}a. Then x = ⨆_{n≥0}(t_{n}w_{n}) = cd^{ω}(ba)(b^{2}a) . . .. With the notations of the preceeding proposition we have s_{0} = cb, s_{i} = b for i ≥ 1, u_{i} = b^{i}a and v_{i} = d for i ≥ 0. For the following considerations it is worth noting that the sequence (w_{n})_{n≥0} is prefix-free. However, there is no recognizable, prefix free set K containing (w_{n})_{n≥0}. Replacing the sequence (w_{n})_{n≥0} by the sequence (w′_{n})_{n≥0} with w′_{n} = db^{n}a changes the v_{i} to v′_{0} = d and v′_{i} = 1 for i ≥ 1. The following corollary states that v′_{0} ≠ 1 is possible due to d ∉ D(alphinf(x)).

Corollary 3.11 Given L, K ⊆ IM with K ∈ Rec(IM) such that K is prefix free, i.e. KIM_{+} ∩ K = ∅. Let (t_{n})_{n≥0} ⊆ L, (w_{n})_{n≥0} ⊆ K such that { t_{n}w_{n} | n ≥ 0 } is an infinite, directed set with x = ⨆{ t_{n}w_{n} | n ≥ 0 }. Assume additionally D(alph(y)) ⊆ D(alphinf(x)), for every y ∈ K. Then there exist a subsequence of indices (n_{i})_{i≥0} 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

t_{n_{i}} = s_{0}u_{0} ⋯ s_{i−1}u_{i−1}s_{i}  and  w_{n_{i}} = u_{i}.

Proof. According to Prop. 3.8, there exist a subsequence of indices (n_{i})_{i≥0} 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 }, t_{n_{i}} = s_{0}u_{0} ⋯ s_{i−1}u_{i−1}s_{i}, w_{n_{i}} = u_{i}v_{0} ⋯ v_{i−1}v_{i}, and alph(v_{i})×alph(s_{j}u_{j}) ⊆ I, for 0 ≤ i < j. We show that the property of K of being prefix-free and the condition about alphinf(x) allow us to take v_{i} = 1 for every i. 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). Now, we have u_{i}v_{0} ⋯ v_{i−2}v_{i−1} ≤ w_{n_{i}} ∈ K for i ≥ 1. Moreover, due to η(u_{i}) = η(u_{i−1}), it follows that η(u_{i}v_{0} ⋯ v_{i−2}v_{i−1}) = η(u_{i−1}v_{0} ⋯ v_{i−2}v_{i−1}) = η(w_{i−1}), hence u_{i}v_{0} ⋯ v_{i−2}v_{i−1} ∈ K for i ≥ 1. Therefore v_{i} = 1, since traces in K have no proper prefix in K. Additionally, since alph(v_{0}) × alph(s_{i}u_{i}) ⊆ I for every i > 0, we have alph(v_{0}) ∩ D(alphinf(x)) = ∅. Hence, since alph(v_{0}) ⊆ alph(w_{i}) with w_{i} ∈ K, v_{0} ≠ 1 would contradict the hypothesis D(alphinf(x)) ⊇ D(alph(y)) for every y ∈ K. 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 [PP92]) 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 e ≠ 1) we obtain indeed the result for Σ^{ω} as a special case of the next proposition (recall Rem. 3.1).

Proposition 3.12 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 x = x_{0}x_{1} … with x_{0} ∈ IM_{s} and x_{n} ∈ IM_{e} for n ≥ 1 we can choose some x′_{n} ∈ IP_{e} such that x′_{n} ≤ x_{n},

n ≥ 1. Hence, x = ⨆\{ x_{0}x_{1} ⋯ x_{n−1}x′_{n} | n ≥ 1 \} ∈ \overrightarrow{IM_{s}IP_{e}} ∩ IR_{e}.

Consider now x ∈ \overrightarrow{IM_{s}IP_{e}}∩IR_{e}, i.e., D(alphinf(x)) = D(alph(e)) and x = ⨆\{ t_{n}w_{n} | n ≥ 0, t_{n} ∈ IM_{s}, w_{n} ∈ IP_{e} }, with the right side being a directed set. By Corollary 3.11 we may assume

t_{n_{i}} = s_{0}u_{0} ⋯ s_{i−1}u_{i−1}s_{i} and w_{n_{i}} = u_{i},

for some index sequence (n_{i})_{i≥0} and trace sequences (s_{i})_{i≥0}, (u_{i})_{i≥0} ⊆ IM. In particular, we have x = s_{0}u_{0}s_{1}u_{1} ⋯ s_{i−1}u_{i−1}s_{i} . . .. We can apply Ramsey’s Theorem in the usual way (e.g. as in [Gas91]) in order to obtain a factorization (m_{i})_{i≥0} of x,

x = (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 every 0 ≤ i < j, and η(s_{0}u_{0} ⋯ s_{m_{1}}) =: s′, hence f ∈ E(S) and s′f = s′, since s′ ∈ Sf. Obviously we have s′ = s. Moreover, f ∈ η(u_{n})S = eS implies f ≤ e, so x ∈ IM_{s}IM_{f}^{ω} with f ≤ e. □

Corollary 3.13 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.12, 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 for sf = s and f ∈ E(S) :

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 ≠ ∅ } associated to L ∈ Rec(IR). Two pairs (s, e), (s′, e′) ∈ S^{2} are called conjugated ([PP92]) if for some x, y ∈ S the equalities s′ = sx, e = xy and e′ = yx hold.

Lemma 3.14 Let L = ⋃_{(s,e)∈P_{L}} IM_{s}IM_{e}^{ω} be recognized by a morphism η : IM → S onto a finite monoid S, with the set P_{L} defined as above. Then for all pairs (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. The direction from right to left is clear due to the definition of conjugated pairs and to η being surjective. 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 group together 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 IM being 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}). Let now 0 ≤ i < j be such that η(s_{i}) = η(s_{j}) =: x (S is finite), and let additionally y := η(u_{i}s_{i+1} ⋯ u_{j−1}). The following relations show that (s, e) and (s′, e′) are conjugated pairs:

s = η(t_{0}t_{1} ⋯ t_{i}) = η(t′_{0}t′_{1} ⋯ t′_{i}) η(s_{i}) = s′x,
e = η(u_{i}s_{i+1} ⋯ u_{j−1}s_{j}) = yx,
e′ = η(s_{i}u_{i} ⋯ s_{j−1}u_{j−1}) = xy.
□

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 languages \{\overrightarrow{L} ∩ IR_{A} | L ∈ Rec(IM), A ⊆ Σ\}. We obtain the well-known result for words as a special case of this theorem.

Theorem 3.15 Let L ∈ Rec(IR) be recognized by η : IM → S onto a finite monoid S, 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). Since (s, e) and (s, f) are conjugated with x = e and y = f (f = xy, e = yx, s = sx), by Lemma 3.14 and Rem. 2.2 we obtain (s, f) ∈ P_{L}. 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

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.14) 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}^{ω}
=^{Cor.3.13} ⋃_{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.16 Rec(IR) is equivalent to the Boolean closure of the family of real

trace languages of type \overrightarrow{L} ∩ IR_{A}, where L ∈ Rec(IM) and A ⊆ Σ.

Proof. Every language \overrightarrow{L} ∩ IR_{A}, L ∈ Rec(IM) and A ⊆ Σ, is recognizable and Rec(IR) is closed under Boolean operations. The other direction is Theorem 3.15.

□

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 (see Example 2.3), we will obtain at the end the equivalence between Rec(IR) and the family of languages accepted by deterministic asynchronous cellular Muller automata. Recall also that the family of languages accepted by asynchronous cellular Muller automata is closed under Boolean operations. 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 partition in connected components for A ⊆ Σ, i.e.,

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.12. 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. Furthermore we write each u_{n} as a product u_{n} = u_{n,1} ⋯ u_{n,k}, where alph(u_{n,i}) = A_{i} for every 1 ≤ i ≤ k. For each n ≥ 1 and 1 ≤ i ≤ k consider the sequence u_{n,i}u_{n+1,i} . . .. Due to A_{i} being connected, this sequence has a least prefix u′_{n,i} such that max(u′_{n,i}) = {a_{i}} and alph(u′_{n,i}) = A_{i}. 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 x = ⨆{ t_{n}w_{n} | t_{n} ∈ L, w_{n} ∈ IP_{A,1} ⋯ IP_{A,k}, n ≥ 0 } with alphinf(x) = A. By Corollary 3.11 (note that IP_{A,1} ⋯ IP_{A,k} ∈ Rec(IM) and IP_{A,1} ⋯ IP_{A,k}IM_{+} ∩ IP_{A,1} ⋯ IP_{A,k} = ∅) we obtain for a subsequence of indices (n_{i})_{i≥0} with x = ⨆_{i≥0} t_{n_{i}}w_{n_{i}}:

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},

for some sequences of finite traces (s_{i})_{i≥0}, (u_{i})_{i≥0}.

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

Before stating the main theorem of this section, let us recall some important concepts of the construction of Zielonka for asynchronous cellular automata 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} }  and  ∂_{A}(t) = ⨆_{a∈A} ∂_{a}(t)
(in particular ∂_{∅}(t) = 1 and ∂_{Σ}(t) = ∂_{max(t)} = t).

Zielonka’s construction is based on the concept of asynchronous mapping (see e.g. [Die90]). 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 μ(∂_{a}(ta)) (= μ(∂_{D(a)}(ta))) is uniquely determined by a and μ(∂_{D(a)}(t)).

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]). The initial state of A is q_{0} = (μ(1))_{a∈Σ} 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 the basic step in the construction of Zielonka of an asynchronous cellular automaton accepting K is to provide an asynchronous mapping μ : IM → Q to a finite set Q, such that the morphism η factorizes through μ, i.e. η = π ∘ μ for a mapping π : Q → S. The asynchronous cellular automaton is then defined as above, with R = π^{−1}(η(K)). A crucial feature of the construction is the fact that for any finite trace t, the local states reached by the resulting asynchronous cellular automaton after having read t, which correspond to the maximal elements of t, already determine whether t is being accepted or not. This follows with t = ∂_{max(t)}(t), hence μ(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 Lemma 4.1, it will suffice to construct a deterministic asynchronous Muller automaton accepting the language \overrightarrow{LIP_{A,1} ⋯ IP_{A,k}} ∩ Inf(A), for 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 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 ) such that L_{A,f} ⊆ L(A) ⊆

\overrightarrow{LIP_{A,1} ⋯ IP_{A,k}} ∩ Inf(A). 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 ∈ Σ. Recall that inf_{a}(t) denotes the set of local a-states which occur infinitely often on the computation path labelled by t (if existent). 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})_{a∈Σ} ∈ (ZZ/2ZZ)^{Σ}
(i) T_{a} = {(f_{a}, i_{a})} for a ∈ Σ \ A,
(ii) (f_{a}, i_{a}) ∈ T_{a} and |T_{a}| ≥ 2, for a ∈ A

The inclusion L_{A,f} ⊆ L(A) is not hard to be seen.

Now 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})_{a∈Σ} ∈ (ZZ/2ZZ)^{Σ}:

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}}, 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 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}. □

Remark 4.3 Note that our result above differs from the situation encountered in the case of words, where the languages \overrightarrow{L}, with L ⊆ Σ^{∗} recognizable, are precisely those recognized by deterministic Büchi automata (therefore called deterministic languages). Here we need the more powerful Muller automata, due to the crucial knowledge of the alphabet occurring infinitely often.

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

Corollary 4.4 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.15, 4.2. The other way round, if L ⊆ IR is accepted by a (deterministic) asynchronous cellular Muller automaton then L can be expressed as a Boolean combination of languages accepted by Büchi asynchronous cellular automata. □

Due to asynchronous automata being automatically I-diamond, we immediately obtain:

Corollary 4.5 Every recognizable, closed infinitary word language can be accepted by a deterministic I-diamond Muller automaton.

5 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 Thm. 3.15 can be improved, i.e. by showing that every recognizable real trace language is already a Boolean combination of languages \overrightarrow{L} with L ∈ Rec(IM). The question, which class of deterministic I-diamond Muller automata accepts closed languages will constitute the subject of a forthcoming paper.

Acknowledgements: We thank Paul Gastin and Jean-Eric Pin for fruitful discussions and Wiesław Zielonka who told us that independently he has developed similar ideas. We also thank the anonymous referees for many valuable comments which helped improving the readability of this paper, in particular concerning the proof of Proposition 3.8.

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. Number 85 in Lecture Notes in Mathematics. 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.

[CP85] R. Cori and D. Perrin. Automates et commutations partielles. R.A.I.R.O. — Informatique Théorique et Applications, 19:21–32, 1985.

[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, Berlin-Heidelberg-New York, 1991. Springer. To appear 1993 in Theoret. Comput. Sci.

[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, Berlin-Heidelberg-New York, 1991. Springer.

[GP92] P. Gastin and A. Petit. Asynchronous cellular 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. Also available as Tech. Rep. 91-68, LITP, Université Paris 6, France, 1991.

[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, Berlin-Heidelberg-New York, 1991. Springer.

[GR91] P. Gastin and B. Rozoy. The poset of infinitary traces. Tech. Rep. LITP 91.07, Université Paris 6 (France), 1991. To appear in Theoret. Comp. Sci.

[Kwi90] M. Kwiatkowska. A metric for traces. Information Processing Letters, 35:129–135, 1990.

[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, Berlin-Heidelberg-New York, 1987. Springer.

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

[PP92] D. Perrin and J.E. Pin. Mots Infinis. Tech. Rep. LITP 92.17, Université Paris 6 (France), 1992. Book to appear.

[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, Berlin-Heidelberg-New York, 1989. Springer.