Logical Definability on Infinite Traces ^{∗}

Werner Ebinger and Anca Muscholl

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

Abstract

The main results of the present paper are the equivalence of definability by monadic second-order logic and recognizability for real trace languages, and that first-order definable, star-free, and aperiodic real trace languages form the same class of languages. This generalizes results on infinite words and on finite traces to infinite traces. It closes an important gap in the different characterizations of recognizable languages of infinite traces.

1 Introduction

In the late 70’s, A. Mazurkiewicz introduced the notion of trace as a suitable mathematical model for concurrent systems [16] (for surveys on this topic see also [1, 6, 10, 17]). In this framework, a concurrent system is seen as a set Σ of atomic actions together with a fixed irreflexive and symmetric independence relation I ⊆ Σ × Σ. The relation I specifies pairs of actions which can be carried out in parallel. It generates an equivalence relation on the set of sequential observations of the system. As this relation is actually a congruence relation, it defines a quotient monoid of Σ^{∗}, called trace monoid. These monoids are also called free partially commutative monoids and have been first studied in combinatorics by Cartier and Foata [5].

Actions in a sequential system are linearly ordered, whereas a concurrent run (trace) corresponds to a restricted Σ-labelled partial order. Traces can also be viewed as dependence graphs, i. e. as labelled, acyclic graphs, where vertices are labelled with actions and edges exist precisely between vertices with dependent labels.

A natural framework for studying non-terminating concurrent systems (e. g. operating systems, transaction systems) is provided by extending Mazurkiewicz traces to infinite traces. Infinite traces are given immediately by considering the extension to infinite dependence graphs. In this paper we are concerned only with dependence graphs where every vertex has a finite past, i. e. every action can be performed within a finite delay. Infinite traces corresponding to this kind of dependence graphs are called real traces. Alternatively, real traces can be viewed as the ideal completion (with respect to the prefix order) of the monoid of finite traces [17].

∗This research has been supported by the EBRA working group No. 6317 ASMICS II.

The family of recognizable real trace languages has been first investigated by P. Gastin [12] from the viewpoint of recognition by saturating homomorphisms. Consequently, the extension of Ochmański’s theorem from finitary trace languages to infinitary trace languages provided a characterization by concurrent-rational expressions [14]. Concerning recognition by means of finite state automata, a suitable model for trace languages is given by automata with distributed control, namely asynchronous (cellular) automata [26, 27]. With appropriate extensions of classical acceptance conditions (Büchi, Muller), it has been shown that the class of recognizable real trace languages corresponds to the family of languages accepted by non-deterministic Büchi [13], respectively deterministic Muller asynchronous (cellular) automata [9]. Solely the logical characterization of recognizability in terms of monadic second-order formulae remained open so far and is provided by this paper.

Motivated by applications in the field of verification and specification of distributed systems (e. g. model checking), the question of determining the expressive power of logic in the context of infinite traces is of particular interest. In the present paper we provide answers to some of the remaining open problems in the theory of real traces [8, for some recent open problems]. We show for example that monadic second-order logic corresponds to recognizability, thus being decidable. Our approach is independent of any model of trace automata.

In the weaker first-order logic framework, we give again a proper generalization from the theory of (ω-) words and finite traces and show that the family of star-free (aperiodic, respectively) sets of real traces coincides with the family of first-order definable languages.

The paper is organized as follows: In Section 2 we recall some basic notions of trace theory, together with some properties of recognizable sets. In Section 3 we show the equivalence of monadic second-order logic and recognizability for real trace languages, extending the characterization for languages of finite traces [25]. Together with a result obtained in Section 4 this provides a new proof for Métivier’s [18, Theorem 2.3] and Ochmański’s [19, Lemma 8.2] result on the recognizability of the Kleene-iteration of connected recognizable languages of finite traces. In Section 4, we consider first-order logic on real traces. First we provide direct transformations between formulae interpreted on finite words and formulae interpreted on finite traces. Then we show that first-order definable languages are exactly the star-free languages. Finally, we show the equivalence of star-freeness and aperiodicity extending characterizations obtained for languages of finite traces [15]. Some of our ideas have been proposed independently by H. J. Hoogeboom, W. Thomas, and W. Zielonka (personal communication).

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. The notations D(a) = { b ∈ Σ | (a, b) ∈ D } and D(Σ′) = ⋃_{a∈Σ′} D(a), Σ′ ⊆ Σ, will be used throughout the paper.

The monoid of finite traces, IM(Σ, D), is defined as a quotient monoid with respect to the congruence relation generated by the independence relation I, i. e. IM(Σ, D) = Σ^{∗}/{ ab ≡ ba | (a, b) ∈ I }. The empty trace (and the empty word as well) will be denoted by 1. A trace can be identified with its dependence graph, i. e. with (an isomorphism class of) a labelled, acyclic, directed graph [V, E, ℓ], where V is a set of vertices labelled by ℓ : V → Σ and E is a set of edges between vertices with dependent labels. More precisely, we have for every x, y ∈ V, (ℓ(x), ℓ(y)) ∈ D if and only if x = y or (x, y) ∈ E or (y, x) ∈ E. Thus, we associate to every word a_{1} ⋯ a_{n}, a_{i} ∈ Σ, the vertex set V = {1, …, n} labelled as ℓ(i) = a_{i}, together with the edge set E = {(i, j) | 1 ≤ i < j ≤ n, (a_{i}, a_{j}) ∈ D}. This notion provides a natural definition of infinite traces by means of infinite dependence graphs. We denote by G(Σ, D) the set of dependence graphs with a countable set of vertices V, such that ℓ^{−1}(a) is well-ordered for every a ∈ Σ.

G(Σ, D) is a monoid with respect to the concatenation [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 additional edges (v_{1}, v_{2}) ∈ V_{1} × V_{2}, whenever (ℓ_{1}(v_{1}), ℓ_{2}(v_{2})) ∈ D holds. The identity is the empty graph 1 = [∅, ∅, ∅]. The concatenation is immediately extendable to finite and infinite products. Let (g_{n})_{n≥0} ⊆ G(Σ, D). The infinite product g = g_{0}g_{1} … ∈ G(Σ, D) is the disjoint union of the g_{n}, together with additional edges from g_{n} to g_{m} for n < m between vertices with dependent labels. Thus, we define the ω-iteration of A ⊆ G(Σ, D) as A^{ω} = { g_{0}g_{1} … | g_{n} ∈ A, ∀n ≥ 0 } (note that for 1 ∈ A we have A^{ω} = A^{∗} ∪ (A \ 1)^{ω}).

We denote by Σ^{ω} the set of infinite words over the alphabet Σ (i. e. mappings from IN to Σ), and by Σ^{∞} the set of finite and infinite words Σ^{∗}∪Σ^{ω}. The canonical mapping φ : Σ^{∗} → IM(Σ, D) associating to a sequence its trace (dependence graph) can be naturally extended to Σ^{∞}, i. e. φ : Σ^{∞} → G(Σ, D). The image φ(Σ^{∞}) ⊆ G(Σ, D) is called the set of real traces and is denoted by IR(Σ, D). Real traces correspond to (in)finite graphs, where every vertex has finitely many predecessors. A word w ∈ Σ^{∞} is called a representative of t ∈ IR(Σ, D) if φ(w) = t. Throughout this paper we abbreviate IR(Σ, D) (IM(Σ, D), respectively) by IR (IM, respectively).

Observe that IR is not a submonoid of G(Σ, D), as e.g. a^{ω}a is not a real trace anymore. A semantically satisfactory definition of the concatenation operation is given by extending the theory to complex traces [7]. Since we consider real traces only, we have chosen here the approach of viewing the concatenation as a partially defined operation on IR, i. e., t = t_{1}t_{2} for t_{1}, t_{2} ∈ IR is defined only if t ∈ IR. Note that this condition is always satisfied if t_{1} is a finite trace.

A word language L ⊆ Σ^{∞} is said to be closed (with respect to (Σ, D)) if L = φ^{−1}φ(L) for the canonical mapping φ : Σ^{∞} → IR.

We denote by alph(t) the set of letters occurring in a trace t. We also use the abbreviation (t, u) ∈ I for alph(t) × alph(u) ⊆ I.

A trace is called connected if its dependence graph is connected. A language is called connected if all its elements are connected. Every trace t ∈ IR can be decomposed into connected components t = t_{1} ˙∪ … ˙∪ t_{n}, i. e. every t_{i} is a connected factor of t = t_{1} ⋯ t_{n} and (t_{i}, t_{j}) ∈ I, for 1 ≤ i ≠ j ≤ n. Let A ⊆ IM, then the language of its connected components is defined as CC(A) = { u ∈ IM | u is a connected component of some t ∈ A }.

The set of letters occurring infinitely often in a real trace t is denoted alphinf(t). We conclude this section with an example. Consider two concurrent processes

P_{1}, P_{2}, given by the instruction sequences

P_{i} : while true do x_{i} := f_{i}(x_{i}, y); y := i endwhile .

We have four (atomic) instructions a = (x_{1} := f_{1}(x_{1}, y)), b = (y := 1), c = (x_{2} := f_{2}(x_{2}, y)) and d = (y := 2), with the independence relation I = {(a, c), (c, a)}. Sequences of instructions satisfying that no process is idle forever are given e.g. by the real trace language {t ∈ {ab, cd}^{ω} | {b, d} ⊆ alphinf(t)}.

2.2 Recognizable Infinitary Word and Trace Languages

In this section we recall some properties of the family of recognizable subsets of Σ^{∞} and IR, denoted by Rec(Σ^{∞}) and Rec(IR), respectively. Recognizable infinitary word languages can be characterized in several ways. The most familiar one involves finite-state automata, equipped with suitable acceptance conditions. These conditions specify (possibly partially) the set of states which have to occur infinitely often on an accepting path. A further characterization is given by ω-rational expressions, which are formed over finite languages of finite words by using the operations union, concatenation, Kleene-star and ω-iteration. Following the definition of the infinite product for dependence graphs, we have for A ⊆ Σ^{∗}, A^{ω} = { w ∈ Σ^{∞} | w = w_{0}w_{1} …, with w_{n} ∈ A for n ≥ 0 }. In particular, if the empty word belongs to A, then A^{ω} = A^{∗} ∪ (A \ {1})^{ω}.

Finally, from the logical viewpoint, recognizability of (infinitary) word languages corresponds to definability in the monadic second-order logic framework studied by Büchi [4].

One possible way to define recognizable real trace languages is by saturating homomorphisms [12]. Let η : IM → S be a homomorphism to a finite monoid S. A real trace language A ⊆ IR is recognized by η if for any sequence (t_{n})_{n≥0} ⊆ IM the following saturation property holds:

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

The saturation property leads, together with a standard Ramsey argument, to a representation of A as A = ⋃_{(s,e)∈P_{A}} η^{−1}(s) η^{−1}(e)^{ω} with P_{A} = { (s, e) ∈ S^{2} | se = s, e^{2} = e and η^{−1}(s) η^{−1}(e)^{ω} ∩ A ≠ ∅ }. An equivalent definition uses Arnold’s syntactic congruence [3]. For A ⊆ IR, two finite traces u, v ∈ IM are congruent if and only if :

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

We denote the syntactic congruence by ≡_{A} and consider the canonical homomorphism η : IM → Synt(A), where Synt(A) = IM/ ≡_{A} is the syntactic monoid of A. Then A ∈ Rec(IR) if and only if the syntactic congruence ≡_{A} has finite index and η : IM → Synt(A) recognizes A. Furthermore, for A ⊆ IR we have Synt(A) = Synt(φ^{−1}(A)) [12].

Due to the partial commutativity there can be no equivalence between recognizability and rational expressions with the Kleene-star as iteration operator. The solution to this problem was given by E. Ochmański [19], who introduced the concept of concurrent iteration. With this notion the family of recognizable finitary trace languages shows to coincide with the family of c-rational (or co-rational) languages. In the infinitary case, ω-rational expressions (formed by using in addition the ω-iteration) precisely characterize recognizable ω-word languages. Again, the result has its counterpart for real trace languages, by using the concurrent ω-iteration instead of the usual ω-iteration [14]. For further details on c-rational real trace languages, we refer to Section 3.1.

3 Monadic Second-Order Logic over Real Traces

In order to specify properties of real trace languages by logical formulae, a real trace t ∈ IR will be identified with its dependence graph. Logical formulae are defined over structures of the form (V, <, (P_{a})_{a∈Σ}), corresponding to dependence graphs [V, E, ℓ], where < is the partial order induced by E and P_{a} = {v ∈ V | ℓ(v) = a}, a ∈ Σ (recall that the restriction of < to P_{a} is a well-founded total order). We allow the empty structure (V = ∅) in order to include the empty trace. We use first-order variables x, y, z, … ranging over the vertex set V and set variables X, Y, Z, … ranging over sets of vertices. Formulae are defined inductively as follows.

• Atomic formulae are given by the first-order predicates x < y, P_{a}(x) and the (monadic) second-order predicate x ∈ X, with x, y, X denoting variables (X is a set variable) and a ∈ Σ.

• Logical connectives: If ψ_{1} and ψ_{2} are formulae, then (ψ_{1} ∨ ψ_{2}) and (¬ψ_{1}) are formulae, too.

• Quantifiers: If ψ is a formula, x is a first-order variable, and X is a monadic second-order variable, then ∃xψ and ∃Xψ are formulae, too.

We refer to the monadic second-order logic system introduced above as MSO. We freely use also ∧, →, ∀ and abbreviations like X ⊆ Y for ∀x (x ∈ X → x ∈ Y) and x = y for ¬(x < y) ∧ ¬(y < x) ∧ ( ⋁_{a∈Σ}(P_{a}(x) ∧ P_{a}(y))). A real trace t is a model for a sentence ψ (i. e. a formula without free variables), if ψ is satisfied by t under the canonical interpretation (in symbols t ⊧ ψ). This means that variables are interpreted by vertices, respectively sets of vertices of the dependence graph G(t) of t, the predicate P_{a}(x) is “x is labelled with a ∈ Σ”, the predicate < is interpreted as the partial order of G(t), and y ∈ X is “y belongs to X”. The real trace language defined by a MSO sentence ψ is given by {t ∈ IR | t ⊧ ψ}. The logical framework introduced above will also be used for defining languages of finite and infinite words. The difference consists in the interpretation of < as a total order in models corresponding to words.

Example 1 The property “ab is a (trace) factor” can be expressed by the sentence

∃x ∃y (P_{a}(x) ∧ P_{b}(y) ∧ ¬(y < x) ∧ ¬ ∃z (x < z ∧ z < y)) .

Note that the expressive power of monadic second-order logic with respect to trace properties does not depend on whether the partial order relation < or the edge relation E_{H} of the Hasse diagram of a trace (or the edge relation of the dependence graph) are chosen to be part of the logical framework, since one can be expressed into the other. The edge relation E_{H} generalizes the successor relation on words and is expressible by the partial order (even in first-order logic):

x E_{H} y iff x < y ∧ ¬ ∃z (x < z ∧ z < y) ,

and conversely (in second-order logic):

x < y iff ∃x′(x E_{H} x′ ∧
∀X(x′ ∈ X ∧ ∀z∀z′(z ∈ X ∧ z E_{H} z′ → z′ ∈ X)
→ y ∈ X)) .

Therefore we are free to use both, the partial order < and the Hasse diagram edge relation, in monadic second-order formulae.

3.1 Equivalence of Recognizability and Monadic Second-Order Logic

The aim of this section is to show the equivalence of recognizability and definability in monadic second-order logic for real trace languages. One possible way to obtain this result is by using automata-theoretic characterizations. We use here a different approach, which turns out to be more elegant. Our proof is based on the characterization of recognizability by c-rational languages [19, 14], which we describe in the following. First, let us define for A ⊆ IM the concurrent iteration A^{c∗} ⊆ IM, respectively concurrent ω-iteration A^{cω} ⊆ IR by A^{c∗} := (CC(A))^{∗}, respectively A^{cω} := (CC(A))^{ω} (recall the notation CC(A) for the connected components of elements of A).

Now, c-rational trace languages form the least family cRat(IR) of subsets of IR satisfying

• ∅ and the singletons {t}, t ∈ IM, belong to cRat(IR).

• If A ⊆ IM and B, C ⊆ IR are in cRat(IR), then also the product A B and the union B ∪ C belong to cRat(IR).

• If A ⊆ IM is in cRat(IR), then also the concurrent iteration A^{c∗} and the concurrent ω-iteration A^{cω} belong to cRat(IR).

Actually we shall use in the following a slight modification of the above definition, which is easily shown to be equivalent [14]: we replace the closure by the two concurrent iteration operators by the following closure property:

• If A ⊆ IM is connected and belongs to cRat(IR), then also the Kleeneiteration A^{∗} and the ω-iteration A^{ω} belong to cRat(IR).

In the proof of the theorem below we use the equivalence between recognizability and MSO definability for ω-word languages [4]. Furthermore, the proof is based on the equivalence between Rec(IR) and cRat(IR) [14].

Theorem 2 Let A ⊆ IR be a real trace language. Then A is recognizable if and only if it is definable in monadic second-order logic.

Proof: The figure below sketches the situation considered. Recall that φ denotes the canonical mapping φ : Σ^{∞} → → IR.

φ^{−1}(A) is  φ^{−1}(A) is
definable  ⟺^{(Büchi)}  recog-
⟹^{(1)}  in MSO  nizable  ⟺^{[12]}
A is  A is
definable  recog-
in MSO  nizable
⟸^{(2)} A is ⟺^{[14]}

c-rational (1): Clearly, we can not use the same formula for both models, traces and words, as the underlying interpretation of the predicate < is different. For example the formula

∃x ∃y ∃z (P_{a}(x) ∧ P_{c}(y) ∧ P_{b}(z) ∧ x < z ∧ y < z ∧ (x < y ∨ y < x))

over the dependence alphabet (Σ, D) = a — b — c is not true for the trace acb, but it is true for both representatives acb and cab of this trace. However, it suffices to express the partial order on traces by the linear order on words.

Given a MSO formula ψ defining A ⊆ IR, we replace every subformula x < y in ψ by a subformula x <_{lin} y given below, obtaining a MSO formula ψ′ satisfying for all t ∈ IR: t ⊧ ψ if and only if w ⊧ ψ′, for all w ∈ Σ^{∞} with t = φ(w).

Note that in any dependence graph [V, E, ℓ], we have for vertices x, y ∈ V: x < y, if and only if there is a sequence x = x_{1} < ⋯ < x_{k} < x_{k+1} = y, k ≥ 1, x_{i} ∈ V, such that (ℓ(x_{i}), ℓ(x_{i+1})) ∈ D, for every 1 ≤ i ≤ k. Moreover, due to the reflexivity of D, we may clearly restrict to the case k ≤ |Σ|. This yields the following definition of x <_{lin} y:

⋁_{1≤k≤|Σ|}  ⋁_{a_{1},...,a_{k+1}∈Σ with (a_{i}, a_{i+1}) ∈ D for 1 ≤ i ≤ k} ∃x_{2} … ∃x_{k}(P_{a_{1}}(x) ∧ P_{a_{2}}(x_{2}) ∧ … ∧ P_{a_{k}}(x_{k}) ∧ P_{a_{k+1}}(y) ∧
x < x_{2} < ⋯ < x_{k} < y) .

(2): This implication is shown by induction over c-rational expressions. Note that we consider both finite and infinite traces as models. Every formula ψ_{A} given below which defines a real trace language A ⊆ IR can be expressed as the disjunction of subformulae satisfied either only by finite or only by non-finite traces.

• For A = ∅ let ψ_{∅} = ∃x(x < x) define A; for A = {t}, t ∈ IM, let ψ_{{t}} be a formula satisfied by the trace t ∈ IM, only.

• A ∪ B for c-rational sets A and B: Combine the formulae ψ_{A} and ψ_{B} for A and B to ψ_{A∪B} = ψ_{A} ∨ ψ_{B}.

• A·B for c-rational sets A ⊆ IM and B ⊆ IR, defined by ψ_{A}, respectively ψ_{B}: For a formula ψ we use in the following relativizations ψ|_{R} of ψ with respect to a unary predicate R. Recall the inductive definition of ψ|_{R}: ψ|_{R} = ψ for atomic formulae ψ; (¬ψ)|_{R} = ¬ψ|_{R}, (ψ_{1} ∨ ψ_{2})|_{R} = ψ_{1}|_{R} ∨ ψ_{2}|_{R}, respectively (∃x ψ)|_{R} = ∃x(R(x) ∧ ψ|_{R}) and (∃X ψ)|_{R} = ∃X(X ⊆ R ∧ ψ|_{R}), where X ⊆ R abbreviates x ∈ X → R(x). The unary predicate R used below is given as a set property. Let ψ_{A·B} be defined as

⋁_{0≤k≤|Σ|} ∃x_{1} … ∃x_{k}(ψ_{A}|_{{x| ∨_{1≤i≤k} x≤x_{i}}} ∧ ψ_{B}|_{{x| ∧_{1≤i≤k} ¬x≤x_{i}}}) .

It is easy to see that ψ_{A·B} defines exactly the product A·B. The meaning of the variables x_{1}, …, x_{k} is to include the maximal vertices of the left factor, which is supposed to belong to A.

• A^{∗}, A^{ω} for a connected c-rational set A ⊆ IM: Let ψ_{A} denote a sentence defining the connected language A ⊆ IM and assume for sake of simplicity 1 ∉ A .

The idea for a formula defining the (finite or ω-) iteration of a language A is to colour the vertices of the dependence graph of the considered trace t, such that the colouring corresponds to a factorization in connected factors t = t_{1} t_{2} …, where every factor t_{i} ∈ IM belongs to A. The identification of (A-) factors will be provided by the property of being one-coloured and by the restriction that for any two different factors having the same colour there is no edge of the Hasse diagram connecting them. Two factors t_{i}, t_{j} will have the same colour only if alph(t_{i}) = alph(t_{j}). For every Σ′ ⊆ Σ we take two colours and colour alternatingly the factors t_{i} with the colours of alph(t_{i}).

We define ψ_{A^{∗}} and ψ_{A^{ω}} as

∃X_{1} … ∃X_{k} (ψ_{1} ∧ ψ_{2} ∧ ψ_{3} ∧ ψ_{4}) ,

where X_{1}, …, X_{k} are supposed to represent the vertex colouring, with k = 2 · 2^{|Σ|}.

The formula ψ_{1} states that V is the disjoint union of all X_{i}. For the next two subformulae we define below the abbreviation mocs(X), which expresses that X is a “maximal one-coloured connected subgraph” of the Hasse diagram. Formally, let mocs(X) be

⋁_{1≤i≤k} (X ⊆ X_{i} ∧ “X is connected”
∧ ∀y∀z ((y ∈ X ∧ z ∈ X_{i} ∧ (z E_{H} y ∨ y E_{H} z)) → z ∈ X)),

where E_{H} is the edge relation of the Hasse diagram. The (first-order) subformula “X is connected” simply requires that the set of labels occurring in X is a connected subalphabet Γ ⊆ Σ.

The formula ψ_{2} ensures that every mocs-component is an element of A and is defined as

∀X (mocs(X) → ψ_{A}|_{X}) ,

where ψ_{A}|_{X} denotes the relativization of the sentence defining A with respect to the predicate x ∈ X. Note that since A is a language of finite traces, the mocs-components satisfying ψ_{2} will be finite.

The underlying interpretation of the mocs-components is that they are factors of the given trace belonging to A. It remains to provide that the mocs-components can be ordered, thus corresponding to a factorization. Let us define the relation X ≺ Y as

∃x∃y (x ∈ X ∧ y ∈ Y ∧ x < y) .

Due to the reflexivity of the dependence relation D it suffices to forbid cycles of mocs-components Y_{1} ≺ Y_{2} ≺ ⋯ ≺ Y_{k} ≺ Y_{k+1} = Y_{1} with k ≤ |Σ|. Consider otherwise a cycle as above, with Y_{i} ≠ Y_{j} for i ≠ j, and vertices x_{i}, y_{i} ∈ Y_{i} with x_{i} < y_{i+1}, for 1 ≤ i ≤ k. For k > |Σ| we obtain by considering equal labels in {x_{1}, … x_{k}} indices 1 ≤ i ≠ j ≤ k with Y_{i} ≺ Y_{j} and Y_{i} ≺ Y_{j+1}. It is easy to see that these relations yield a smaller cycle. The formula ψ_{3} ensures that the relation ≺ restricted on mocs-components is acyclic:

¬ ⋁_{2≤k≤|Σ|} ∃Y_{1} … ∃Y_{k}( ⋀_{1≤i≤k} mocs(Y_{i}) ∧

Y_{1} ≺ Y_{2} ∧ … ∧ Y_{k−1} ≺ Y_{k} ∧ Y_{k} ≺ Y_{1}) .

Finally ψ_{4} determines whether its trace models are finite or not, depending on the type of iteration (Kleene-star or ω). For the ω-iteration e.g., we have ψ_{4} = ⋁_{a∈Σ} (∀x(P_{a}(x) → ∃y(x < y ∧ P_{a}(y)))).

□

The proof of Theorem 2 can also be provided using the classical automatonbased approach given by Büchi [24]. Using the characterization of recognizability by nondeterministic asynchronous (cellular) automata with local Büchi acceptance [13], one can view a run of an asynchronous automaton as a labelling of a dependence graph with local states. This allows to show that a trace language A ⊆ IR is accepted by some Büchi asynchronous cellular automaton if and only if A is definable in MSO [11] (respectively [25] for finite traces).

4 First-Order Logic on Real Traces

For (ω-) word languages the restriction of the logical framework to quantifying only over first-order variables turns out to yield a subclass of recognizable languages with various interesting properties. First-order definable (ω-) word languages are closely related to temporal logic of linear time and show to coincide with the star-free languages. Moreover, they can be captured by an algebraic property (aperiodicity) [24, for an overview]. For languages of finite traces we have the equivalence between aperiodicity and star-freeness [15], respectively between star-freeness and first-order definability, as shown by Thomas and Zielonka [personal communication].

The first-order logical framework we consider (denoted by FO) restricts for the present signature the quantification of formulae to variables x, y, …, only. In the following we first exhibit a direct transformation between formulae interpreted on finite trace models and formulae interpreted on finite word models (the result also holds for higher order logic). For the general case of real trace languages we obtain the equivalence stated in Proposition 3 below by the characterizations of Sections 4.1, 4.2. A direct construction as presented below is of independent interest.

In the proof of the following proposition we use the same approach for both formulae transformations. In particular, we replace every subformula x < y of a sentence ψ, which is interpreted on words, by a formula suitable for the partial order interpretation. However, it is not possible to unify different interpretations of a formula on the representatives of a trace to one interpretation for the trace model itself. Consider e.g. the formula ∀x ∀y (x ≤ y ∨ y ≤ x), which is false on any dependence graph containing two incomparable vertices, but is always true on word models.

The idea is to fix a representative of each trace and to express the total order of the fixed representative by the partial order of the dependence graph. As representative of a trace we choose the lexicographic normal form. (The use of the lexicographic normal form here was observed independently by W. Zielonka.) Given a linear ordering <_{Σ} of Σ, the lexicographic normal form of a trace t ∈ IM (in symbols lnf(t)) is lexicographically the first representative w ∈ φ^{−1}(t). Equivalently, a word w ∈ Σ^{∗} is the lexicographic normal form of its trace φ(w) if and only if for each factor aub of w with a, b ∈ Σ, u ∈ Σ^{∗}, and (au, b) ∈ I, we have a <_{Σ} b [2].

Proposition 3 A trace language A ⊆ IM is definable in first-order logic if and only if φ^{−1}(A) ⊆ Σ^{∗} is definable in first-order logic.

Proof: Given a first-order sentence defining A ⊆ IM we obtain directly from the proof of Theorem 2 a first-order sentence defining φ^{−1}(A).

Suppose now we are given a first-order sentence ψ defining a closed word language A = φ^{−1}φ(A) ⊆ Σ^{∗}.

As outlined above, we replace every subformula x < y occurring in the sentence ψ defining A ⊆ Σ^{∗} by the subformula lex(x, y) given below. The new sentence ψ′ will satisfy t ⊧ ψ′ if and only if lnf(t) ⊧ ψ. Due to A being a closed word language, this will yield the result.

Let x, y be vertices in the dependence graph of t and let lex(x, y) denote the predicate expressing that x precedes y in the lexicographic normal form of t, lnf(t). Assume that lex(x, y) holds and let x_{0} ⋯ x_{n} correspond to the factor in lnf(t) satisfying x_{0} = x and x_{n} = y. Let i be minimal, 0 ≤ i ≤ n, such that x_{i} ≤ y holds in the partial order of the dependence graph. Then we have (x_{0} ⋯ x_{i−1}, x_{i}) ∈ I and hence ℓ(x_{0}) ≤_{Σ} ℓ(x_{i}). It is easy to see now that lex(x, y) is equivalent to ∃z (ℓ(x) ≤_{Σ} ℓ(z) ∧ z ≤ y ∧ lex(x, z)). This observation leads to defining lex(x, y) as ⋁_{a,b∈Σ} (P_{a}(x) ∧ P_{b}(y) ∧ lex_{a,b}(x, y)), where lex_{a,b}(x, y) is defined recursively as

lex_{a,b}(x, y) = \{ \begin{matrix}x < y & for a = b , \\ ¬ lex_{b,a}(y, x) & for a <_{Σ} b , \\ ∃z ( ⋁_{c≥_{Σ}a} (P_{c}(z) ∧ z ≤ y ∧ lex_{a,c}(x, z))) & for a >_{Σ} b . \end{matrix}

Note that the recursion depth is at most 2 · |Σ|, yielding a first-order formula of exponential size in |Σ|. The quantifier depth is bounded by |Σ|. □

Remark 4 The result stated in Proposition 3 clearly also holds if we replace first-order by second-order logic. This, together with Theorem 2, provides a new proof for Métivier’s [18, Theorem 2.3] and Ochmański’s [19, Lemma 8.2] theorem on the recognizability of the Kleene-iteration of connected recognizable finitary trace languages.

Remark 5 Since the lexicographic normal form is in general undefined for real traces, the above proof can be extended directly to real traces only for the special case where the considered language contains only traces t where the set of letters occurring infinitely often in t is a connected subalphabet.

4.1 Equivalence of Star-Free Expressions and First-Order Logic

In this section we show the equivalence of star-freeness and definability in firstorder logic. We generalize the approach of Perrin and Pin [21] from words to real traces.

The family of star-free finitary trace languages SF(IM) is the closure of the sets {t}, t ∈ IM, by Boolean operations and concatenation [15].

Definition 6 The family SF(IR) of star-free real trace languages is the smallest family F of subsets of IR with

1. SF(IM) ⊆ F,

2. AB ∈ F for any A, B ∈ F with A ⊆ IM, B ⊆ IR, and

3. F is closed under Boolean operations (where the complementation is meant with respect to IR).

Note that since IM ∈ SF(IR) holds, the complementation of a finitary language A ∈ SF(IM) with respect to IM can be obtained by complementing with respect to IR and intersecting with IM.

We will consider formulae with free variables and interpret them on extended trace models. For a finite set W of variables we add to a structure (V, <, (P_{a})_{a∈Σ}) a mapping of variables σ : W → V, associating every variable with one vertex in the dependence graph of the trace. Thus we obtain a new structure (V, <, (P_{a})_{a∈Σ}, σ) of a trace with a set W of variables, denoted W -trace. Let a set of W -traces be denoted as a W -trace language. If W is empty, then the new structure (V, <, (P_{a})_{a∈Σ}, ∅) can be identified with the former one, (V, <, (P_{a})_{a∈Σ}). We denote by IM_{W} (resp. IR_{W}) the set of finite W -traces (resp. real W -traces).

The concatenation of a W -trace t and a W′-trace t′ is defined only if W ∩W′ = ∅; in this case, in addition to the usual concatenation of dependence graphs, the mapping of variables of tt′ is the disjoint union of the mapping of variables of t and t′. The complement of a real W -trace language A ⊆ IR_{W} is meant with respect to IR_{W}. The definition of star-free languages can now be immediately extended to star-free real trace languages over extended structures. Let SF_{e}(IM) denote the family of W -trace languages (for finite sets W) obtained from the sets {t} (t ∈ IM_{W} for finite W) by concatenation and Boolean operations, where the complement of a W -trace language is meant with respect to IM_{W}. Further, let SF_{e}(IR) denote the smallest family of subsets of IR_{W} (for finite sets W) containing SF_{e}(IM) and closed under concatenation and Boolean operations.

For the rest of the section, sets W of (first-order) variables are supposed to be finite. The following lemma states some useful properties of star-free trace languages over the extended structures defined above. The left and right quotients t^{−1}A and At^{−1} for t ∈ IR_{U}, A ⊆ IR_{W} are defined as usual, by t^{−1}A = { v | tv ∈ A } and At^{−1} = { v | vt ∈ A }. Note that the partial monoid of real traces IR is left-, but not right-cancellative: If uv, uv′, vu, and v′u are defined, we have uv = uv′ ⇒ v = v′, but vu = v′u does not imply v = v′. In particular it does not hold that {t}t^{−1} = {1}, for example {a^{ω}}(a^{ω})^{−1} = a^{∗} ≠ {1}.

Lemma 7 1. For any Σ′ ⊆ Σ and any set W, the languages {t ∈ IM_{W} |

alph(t) ⊆ Σ′} respectively {t ∈ IR_{W} | alph(t) ⊆ Σ′} are star-free.

2. Taking left and right quotients commutes with ∪ and ∩. Moreover, let t ∈ IR_{U} and A ⊆ IR_{W} with U ⊆ W. Then we have \overline{t^{−1}A} = t^{−1}\overline{A} ∪ \{u ∈ IR_{W \U} | tu ∉ IR_{W} \}, respectively \overline{At^{−1}} = \overline{A}t^{−1} ∪ \{u ∈ IR_{W \U} | ut ∉ IR_{W} \}.

3. Let A ∈ SF_{e}(IR). Then the set of left (right) quotients { t^{−1}A | t ∈ IR_{U}, U } ({ At^{−1} | t ∈ IR_{U}, U }) is a finite subset of SF_{e}(IR).

Proof: 1: Obvious. 2: Note that for u ∈ IR_{W \U} we have u ∉ t^{−1}A if and only if either tu ∈ \overline{A} or tu is not a real trace. 3: Assume A ∈ SF_{e}(IR) ∩ IR_{W}. The proof is given by induction on the star-free expression for A. We denote the number of different languages t^{−1}A by n(A). If A = {u} for some u ∈ IM_{W}, then n(A) ≤ 2^{|u|}. If A = B∪C, then t^{−1}A = t^{−1}B∪t^{−1}C, hence n(A) ≤ n(B)·n(C) (∩ analogously). If A = \overline{B}, then with t^{−1}\overline{B} = \overline{t^{−1}B} \ \{v ∈ IR_{W \U} | alph(v) ∩ D(alphinf(t)) ≠ ∅\} we obtain n(A) ≤ n(B) · 2^{|Σ|}.

If A = BC, then t^{−1}(BC) = ⋃_{rs=t}(r^{−1}B ∩ F_{s})(s^{−1}C), where F_{s} = {p ∈ IR_{W′} | (p, s) ∈ I} ∈ SF_{e}(IR) (for some W′ ⊆ W), thus

{ t^{−1}(BC) | t ∈ IR_{U} } = { ⋃_{rs=t}(r^{−1}B ∩ F_{s})(s^{−1}C) | t ∈ IR_{U} } ,

with n(r^{−1}B ∩ F_{s}) ≤ n(B) · 2^{|Σ|} and n(A) ≤ 2^{n(B) 2^{|Σ|} n(C)}. Right quotients At^{−1} for A ∈ SF_{e}(IR) are handled symmetrically. □

Theorem 8 A trace language A ⊆ IR is definable in first-order logic if and only if it is star-free.

Proof: “⇐”: Set operations are replaced by the corresponding logical operations. For the concatenation we use the first-order formula from Section 3.

“⇒”: We give a proof by induction on formulae.

Predicates: The set of real W -traces satisfying x < y for some variables x, y ∈ W, is a star-free trace language of the following form (we omit the subscripts for IM, IR and a ∈ Σ_{X} denotes that the set of variables X is assigned to vertex a):

⋃_{finite} ⋃_{a_{1}∈Σ_{X},a_{l}∈Σ_{Y} , x∈X, y∈Y with (a_{i}, a_{i+1}) ∈ D for 1 ≤ i ≤ l − 1} IMa_{1}IMa_{2} ⋯ a_{l−1}IMa_{l}IR .

Note that the sets of variables assigned to the factors in the expression above form a partition of W and l ≤ |Σ|.

A real W -trace language satisfying P_{a}(x) is of the form ⋃_{finite} IMaIR with a ∈ Σ_{X} and x ∈ X. For x = y we have the representation ⋃_{finite} ⋃{a∈Σ_{X} \atop x,y∈X} IMaIR.

Formulae: For ∧, ∨, ¬ we use the corresponding set operations. Finally, for quantified formulae, if A ∈ SF_{e}(IR) ∩ IR_{W} is the language defined by a formula ψ with free variables W and x ∈ W, then we first express A using left and right quotients [21] (we omit again the subscript for IR)

A = ⋃_{{a∈Σ_{X}, ua∈IR, \atop x∈X⊆W}} B(u) a C(u)

with

C(u) = (ua)^{−1}A, B(u) = ⋂_{v∈C(u)} A(av)^{−1} .

By Lemma 7 the union above is finite. Finally, the real W \ {x}-trace language A′ defined by the formula ∃x ψ is

A′ = ⋃_{a∈Σ_{X\{x}}, ua∈IR} B(u) a C(u)

□

4.2 Aperiodic and Star-Free Real Trace Languages

A monoid is called aperiodic if it satisfies the equation x^{n} = x^{n+1} for some n > 0. Let A ⊆ IR be a real trace language. A is called aperiodic if there exists a homomorphism η : IM → S to an aperiodic, finite monoid S recognizing A (Equivalently, the syntactic monoid of A is finite and aperiodic, and the syntactic morphism recognizes A.).

We denote the family of aperiodic real (finitary, respectively) trace languages by AP(IR) (AP(IM), respectively). We use analogous notations for word languages. We recall Schützenberger’s result stating the equivalence between aperiodicity and star-freeness for finitary word languages [23]. The result has been extended to ω-word languages by Perrin [20] and for languages of finite traces by Guaiana et. al. [15].

Let us begin with some notations concerning recognizability by homomorphisms and consider η : IM → S to a finite monoid S. For s ∈ S we denote

M_{s} = η^{−1}(s)
P_{s} = M_{s} \ M_{s}IM_{+}, with IM_{+} = IM \ {1} .

Thus, IM_{s} is the set of all finite traces which are mapped to s by η and P_{s} is the subset of IM_{s}, consisting of traces having no proper prefix in IM_{s}. Finally, if we consider a homomorphism η : Σ^{∗} → S, then we use the notation X_{s} = η^{−1}(s), for s ∈ S.

Moreover, we may assume that alph(t) = alph(t′) for all t, t′ ∈ IM with η(t) = η(t′), since we may replace S with a submonoid of S × P(Σ), with the multiplication defined by (s, Γ)(s′, Γ′) = (ss′, Γ ∪ Γ′) and (1, ∅) as identity. Moreover we replace η(a) with (η(a), {a}) for a ∈ Σ. Hence, alph(s) for s ∈ S can be defined as alph(t) for some t ∈ η^{−1}(s). Note that any aperiodic monoid S remains aperiodic if we replace it with (a submonoid of) S × P(Σ).

For Σ′ ⊆ Σ, let IR_{Σ′} = { t ∈ IR | D(alphinf(t)) = D(Σ′) }. Note that in the word case (i. e. D = Σ × Σ) we have IR_{Σ′} = Σ^{ω}, for every ∅ ≠ Σ′ ⊆ Σ and IR_{∅} = Σ^{∗}. In particular, we denote by IR_{s} for s ∈ S the set IR_{Σ′} with Σ′ = alph(s).

Let A ⊆ IM. We define \overrightarrow{A} = \{ t ∈ IR | t = ⊔B with B directed and B ⊆ A \}. A non-empty set B ⊆ IM is called directed if for every t, t′ ∈ B, there exists a z ∈ B such that t and t′ are both prefixes of z.

The following lemma generalizes a lemma used in Schützenberger’s proof of McNaughton’s theorem for ω-word languages [22]. For real traces, the proof of the lemma becomes more involved and the reader is referred directly to [9].

Lemma 9 [9] Let S be a finite monoid, η : IM → S a homomorphism and e ∈ S such that e^{2} = e. Then we have IM_{e}^{ω} = \overrightarrow{IM_{e}P_{e}} ∩ IR_{e}.

Before stating the result of this section, let us define the I-shuffle K_{1} _{I} K_{2} of two (ω-) word languages K_{i} ⊆ Σ^{∞} by K_{1} _{I} K_{2} = { u_{0}v_{0}u_{1}v_{1} … | u_{n}, v_{n} ∈ Σ^{∗}, u_{0}u_{1} … ∈ K_{1}, v_{0}v_{1} … ∈ K_{2} and (v_{n}, u_{m}) ∈ I, for n < m }.

Theorem 10 The family of star-free real trace languages coincides with the family of aperiodic real trace languages.

Proof: “⇐”: Let us first show that every aperiodic language A ⊆ IR is star-free. To this purpose, consider η : IM → S a homomorphism to a finite, aperiodic monoid S recognizing A. Then we have A = ⋃_{(s,e)∈P} IM_{s}IM_{e}^{ω}, with P = { (s, e) ∈ S^{2} | se = s, e^{2} = e, IM_{s}IM_{e}^{ω} ∩ A ≠ ∅ }. Since IM_{s} ∈ SF(IM) [15], it suffices to show that IM_{e}^{ω} ∈ SF(IR). By Lemma 9, IM_{e}^{ω} = \overrightarrow{IM_{e}P_{e}} ∩ IR_{e}. Furthermore, IR_{e} ∈ SF(IR). More precisely, IR_{e} (with e ≠ 1) is a finite union of sets IMIM_{Σ′}^{ω} with Σ′ ⊆ Σ, IM_{Σ′} = \{t ∈ IM | alph(t) = Σ′\} and IM_{Σ′}^{ω} = (⋂_{b∉Σ′} \overline{IMbIR} ∩ ⋂_{a∈Σ′} \overline{IM\overline{IMaIR}}) \ IM, hence the result.

It remains to show \overrightarrow{IM_{e}P_{e}} ∈ SF(IR). More generally, if B ⊆ IM is recognized by a homomorphism η : IM → S to a finite monoid S, then we may write the complement of \overrightarrow{B} as follows (analogously to [20]):

\overline{\overrightarrow{B}} = ⋃_{p∈S}(IM_{p} \overline{⋃_{q with pq∈η(B)}IM_{q} IR}) .

The above expression simply states that t ∉ \overrightarrow{B} if and only if there exists a finite prefix u ≤ t such that for every v ∈ IM with uv ≤ t, uv ∉ B. Moreover, with S aperiodic we obtained \overrightarrow{B} ∈ SF(IR) by [15].

“⇒”: For this inclusion, it suffices to show that A ∈ SF(IR) implies φ^{−1}(A) ∈ SF(Σ^{∞}), since SF(Σ^{∞}) = AP(Σ^{∞}) [20] and Synt(A) = Synt(φ^{−1}(A)). We proceed by induction on the star-free expression denoting A ∈ SF(IR). For A ∈ SF(IM) we have A ∈ AP(IM) by [15], hence φ^{−1}(A) ∈ AP(Σ^{∗}) = SF(Σ^{∗}) [23]. Furthermore, let A = A_{1} ∪ A_{2} (A = A_{1} ∩ A_{2}, A = \overline{A_{1}} respectively) with φ^{−1}(A_{1}), φ^{−1}(A_{2}) ∈ SF(Σ^{∞}). Then φ^{−1}(A) ∈ SF(Σ^{∞}) holds, since φ^{−1} commutes with the Boolean operations.

Finally, let A = A_{1}A_{2} with A′_{1} = φ^{−1}(A_{1}) ∈ SF(Σ^{∗}), A′_{2} = φ^{−1}(A_{2}) ∈ SF(Σ^{∞}). Then, φ^{−1}(A) = A′_{1} _{I} A′_{2}, with _{I} denoting the I-shuffle operation. In particular, we have

A′_{1} _{I} A′_{2} = { u_{0}v_{0} … u_{n}v_{n}w | u_{k}, v_{k} ∈ Σ^{∗}, w ∈ Σ^{∞}, u_{0}u_{1} … u_{n} ∈ A′_{1},
v_{0}v_{1} … v_{n}w ∈ A′_{2} and (v_{i}, u_{k}) ∈ I, for i < k ≤ n } .

Since A′_{1} ∈ SF(Σ^{∗}) = AP(Σ^{∗}) and A′_{2} ∈ SF(Σ^{∞}) = AP(Σ^{∞}), let η : Σ^{∗} → S denote a homomorphism recognizing both A′_{1} and A′_{2}, with S an aperiodic, finite monoid (for A′_{2} this means that η recognizes A′_{2} ∩ Σ^{ω} and A′_{2} ∩ Σ^{∗}). Furthermore, we consider the set P = { (s, e) ∈ S^{2} | se = s, e^{2} = e, X_{s}X_{e}^{ω} ∩ A′_{2} ≠ ∅ }. Noting that X_{1} = {1} = X_{1}^{ω}, with 1 denoting the identity in S, we have A′_{2} = ⋃_{(s,e)∈P} X_{s}X_{e}^{ω}. Moreover, A′_{1} = η^{−1}η(A′_{1}). It is not hard to see that we may express A′_{1} _{I} A′_{2} by

A′_{1} _{I} A′_{2} = ⋃_{r∈η(A′_{1})} ⋃_{(s,e)∈P} (X_{r} _{I} X_{s})X_{e}^{ω} .

Since both X_{r} and X_{s} are aperiodic, closed finitary word languages (due to A′_{i} being closed), we have X_{r} _{I} X_{s} ∈ SF(Σ^{∗}) [15]. Moreover, since e is an idempotent element of S, with S aperiodic, we also have X_{e}^{ω} ∈ SF(Σ^{∞}) [20]. Hence, A′_{1} _{I} A′_{2} = φ^{−1}(A) ∈ SF(Σ^{∞}). □

Let us summarize: Since for every A ∈ Rec(IR), Synt(A) = Synt(φ^{−1}(A)) holds, we obtained by the results of Section 4 the following equivalent characterizations:

i) A is first-order definable.

ii) φ^{−1}(A) is first-order definable.

iii) A is star-free.

iv) Synt(A) is aperiodic and the syntactic homomorphism η : IM → Synt(A) recognizes A.

5 Conclusion

In this paper we have generalized the most important results concerning logic, recognizability, star-freeness and aperiodicity from word languages and finitary trace languages to the case of infinitary trace languages.

For star-free languages an extension to the quantifier alternation hierarchy of first-order formulae and dot-depth hierarchies of languages has been considered [11, contains also a temporal logic which is expressively equivalent to first-order logic for finite traces].

Acknowledgements

We want to thank V. Diekert, P. Gastin, H. J. Hoogeboom, D. Kuske, and W. Thomas for many interesting comments. We also thank the anonymous referees from ICALP and especially from Theoretical Computer Science for the valuable comments which helped improving the presentation of this paper.

References

[1] IJ. J. Aalbersberg and G. Rozenberg. Theory of traces. Theoretical Computer Science, 60:1–82, 1988.

[2] A. V. Anisimov and D. E. Knuth. Inhomogeneous sorting. International Journal of Computer and Information Sciences, 8:255–260, 1979.

[3] A. Arnold. A syntactic congruence for rational ω-languages. Theoretical Computer Science, 39:333–335, 1985.

[4] J. R. Büchi. On a decision method in restricted second order arithmetic. In E. Nagel et al., editors, Proc. Internat. Congress on Logic, Methodology and Philosophy of Science, pages 1–11. Stanford Univ. Press, Stanford, CA, 1960.

[5] 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.

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

[7] V. Diekert. On the concatenation of infinite traces. Theoretical Computer Science, 113:35–54, 1993. Special issue STACS‘91.

[8] V. Diekert and W. Ebinger, editors. Infinite Traces. Proceedings of a workshop of the ESPRIT Basic Research Action No 3166: Algebraic and Syntactic Methods in Computer Science (ASMICS), Tübingen, Germany, 1992, Bericht 4/92. Universität Stuttgart, Fakultät Informatik, 1992.

[9] V. Diekert and A. Muscholl. Deterministic asynchronous automata for infinite traces. Acta Informatica, 31:379–397, 1994. A preliminary version was presented at STACS’93, Lecture Notes in Computer Science 665 (1993).

[10] V. Diekert and G. Rozenberg, editors. The Book of Traces. World Scientific, Singapore, 1995.

[11] W. Ebinger. Charakterisierung von Sprachklassen unendlicher Spuren durch Logiken. Dissertation, Institut für Informatik, Universität Stuttgart, 1994.

[12] P. Gastin. Recognizable and rational trace languages of finite and infinite traces. In C. Choffrut 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.

[13] P. Gastin and A. 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, number 623 in Lecture Notes in Computer Science, pages 583–594, Berlin-Heidelberg-New York, 1992. Springer.

[14] P. Gastin, A. Petit, and W. Zielonka. An extension of Kleene’s and Ochmański’s theorems to infinite traces. Theoretical Computer Science, 125:167–204, 1994. A preliminary version was presented at ICALP’91, Lecture Notes in Computer Science 510 (1991).

[15] G. Guaiana, A. Restivo, and S. Salemi. Star-free trace languages. Theoretical Computer Science, 97:301–311, 1992. A preliminary version was presented at STACS’91, Lecture Notes in Computer Science 480 (1991).

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

[17] 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.

[18] Y. Métivier. Une condition suffisante de reconnaissabilité dans un monoïde partiellement commutatif. R.A.I.R.O. — Informatique Théorique et Applications, 20:121–127, 1986.

[19] E. Ochmański. Regular behaviour of concurrent systems. Bulletin of the European Association for Theoretical Computer Science (EATCS), 27:56– 67, Oct 1985.

[20] D. Perrin. Recent results on automata and infinite words. In M. P. Chytil and V. Koubek, editors, Proceedings of the 11th Symposium on Mathematical Foundations of Computer Science (MFCS’84), Praha (CSFR) 1984, number 176 in Lecture Notes in Computer Science, pages 134–148. Springer, Berlin-Heidelberg-New York, 1984.

[21] D. Perrin and J.-E. Pin. First-order logic and star-free sets. Journal of Computer and System Sciences, 32:393–406, 1986.

[22] D. Perrin and J. E. Pin. Mots Infinis. Tech. Rep. LITP 93.40, Université Paris 7 (France), 1993. Book to appear.

[23] M. P. Schützenberger. On finite monoids having only trivial subgroups. Information and Control, 8:190–194, 1965.

[24] W. Thomas. Automata on infinite objects. In J. v. Leeuwen, editor, Handbook of Theoretical Computer Science, chapter 4, pages 133–191. Elsevier Science Publishers B. V., 1990.

[25] W. Thomas. On logical definability of trace languages. In V. Diekert, editor, Proceedings of a workshop of the ESPRIT Basic Research Action No 3166: Algebraic and Syntactic Methods in Computer Science (ASMICS), Kochel am See, Bavaria, FRG (1989), Report TUM-I9002, Technical University of Munich, pages 172–182, 1990.

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

[27] W. Zielonka. Safe executions of recognizable trace languages by asynchronous automata. In A. R. Mayer et al., editors, Proceedings of the 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.