CLOSURE PROPERTIES OF LOCALLY FINITE ω-LANGUAGES ⋆

Olivier Finkel ∗

Equipe de Logique Mathématique CNRS et Université Paris 7, U.F.R. de Mathématiques 2 Place Jussieu 75251 Paris cedex 05, France.

Dedicated to Denis Richard for his 60 th Birthday

Abstract

Locally finite ω-languages, defined via second order quantifications followed by a first order locally finite sentence, were introduced by Ressayre in [Res88]. They enjoy very nice properties and extend ω-languages accepted by finite automata or defined by monadic second order sentences. We study here closure properties of the family LOC_{ω} of locally finite omega languages. In particular we show that the class LOC_{ω} is neither closed under intersection nor under complementation, giving an answer to a question of Ressayre [Res89].

Key words: Formal languages; logical definability; infinite words; locally finite languages; closure properties.

1 Introduction

In the sixties J.R. Büchi was the first to study ω-languages recognized by finite automata in order to prove the decidability of the monadic second order theory of one successor over the integers [Büc62]. In the course of his proof he showed that an ω-language, i.e. a set of infinite words over a finite alphabet, is accepted by a finite automaton with the now called Büchi acceptance condition if and only if it is defined by an (existential) monadic second order sentence.

⋆ Partially supported by Intas 00-447.

∗ Corresponding author Email address: finkel@logique.jussieu.fr (Olivier Finkel).

Preprint submitted to Elsevier Science

Algorithms have been found to give such an automaton from the monadic second order sentence and conversely. Thus the above cited decision problem is reduced to the decidability of the emptiness problem for Büchi automata which is easily shown to be decidable. The equivalence between definability by monadic second order sentences and acceptance by finite automata holds also for languages of finite words [Büc60], and has been extended to languages of words of length α, where α is a countable ordinal ≥ ω [BS73].

The research area, now called “descriptive complexity”, found its origin in the above cited work of Büchi as well as in the fundamental result of Fagin who proved that the class NP is characterized by existential second order formulas, [Fag74]. Since then, a lot of work has been achieved about the logical definability of classes of formal languages of finite or infinite words, or of relational structures like graphs, see [Fag93] [Pin96] [Tho96] [Imm99] for a survey about this field of research.

Several extensions of existential monadic second order logic over words have been studied.

Lauteman, Schwentick and Therien proved that context free languages are characterized by existential second order formulas in which the second order quantifiers bear only on matchings, i.e. pairing relations without crossover, [LST94].

Parigot and Pelz, and more recently Yamasaki, extended monadic second order logic with two second order relation symbols and characterized classes of Petri net (ω)-languages [PP85] [Pel87] [Yam99].

Eiter, Gottlob and Gurevich studied the relationship between monadic second order logic and syntactic fragments of existential second order logic over (finite) words [EGG00]. Distinguishing prefix classes, they determined which of them define only regular languages and which of them have the same expressive power as monadic second order logic.

Another extension has been introduced by Ressayre, in order to apply some powerful tools of model theory to the study of formal languages, [Res88]. He defined locally finite sentences (firstly called local). A locally finite sentence φ is a first order sentence which is equivalent to a universal one and whose models satisfy simple structural properties: closure under functions takes a finite number n_{φ} of steps. These syntaxic and semantic restrictions allow a meaningful use of the notion of indiscernables and lead to beautiful stretching theorems connecting the existence of some well ordered infinite models of φ with the existence of some finite models generated by indiscernables [FR96].

Locally finite languages are defined by second order formulas in the form ∃R̄ ∃f̄ φ where φ is a locally finite sentence and R̄ (respectively, f̄) represent the relation (respectively, function) symbols in the signature of φ. These second order quantifications are much more general than the monadic ones as the following results show:

• Each regular language is locally finite, [Res88], and many context free as well as non context free languages are locally finite [Fin01].

• Each regular ω-language is a locally finite ω-language, [Fin01] [Fin89], and there exist many more locally finite ω-languages as we shall see below.

• This result is extended to languages of transfinite length words: if α is an ordinal < ω^{ω}, each regular α-language is also locally finite [Fin01].

But a pumping lemma, following from a stretching theorem, makes locally finite ω-languages keep important properties of regular ω-languages, [Res88] [FR96]. It is an analogue for each locally finite ω-language of the property:

“ A regular ω-language is non empty if and only if it contains an ultimately periodic word ”.

This lemma implies in a similar manner the decidability of the emptiness problem for locally finite ω-languages. Moreover for each countable ordinal α < ω^{ω}, the decidability of the emptiness problem for locally finite α-languages follows from similar arguments, [FR96]. Other decidability results, as the decidability of the problem: “is a given finitary locally finite language infinite?” follow from stretching theorems of [Res88][FR96].

These interesting properties of locally finite languages naturally lead to the question of the richness of the class of locally finite languages: how large is this class? What are its closure properties?

The study of locally finite languages of finite words was begun by Ressayre in [Res88] and continued in [Fin01]. We focus in this paper on the class LOC_{ω} of locally finite ω-languages and study classical closure properties for this class. In particular, we show that LOC_{ω} is neither closed under intersection, nor under complementation. The proof uses the notion of rational cone of finitary languages which is important in formal language theory and the notion of indiscernables in a structure, often used in model theory. This gives an answer to a question of Ressayre, [Res89]. Of course we would have preferred a positive answer to this question which would have provided a useful class of sentences for specification and verification of properties of non-terminating systems. But this leaves still open, for further study, the possibility to find such a useful class of sentences as a subclass of the class of locally finite sentences.

In section 2, we give the first definitions and some examples of locally finite ω-languages. In section 3, closure properties for ω-languages are investigated. We show that the class LOC_{ω} is not closed under intersection with regular ω-languages thus LOC_{ω} is neither closed under intersection, nor under complementation (because LOC_{ω} is closed under union). Then we prove that LOC_{ω} is closed under λ-free morphism and λ-free substitution of locally finite (finitary) languages.

2 Definitions and examples

2.1 Definitions

We briefly indicate now some basic facts about first order logic and model theory. See for example [CK73] for more background on this subject.

We consider here formulas of first order logic. The language of first order logic contains (first order) variables x, y, z, … ranging over elements of a structure, logical symbols: the connectives ∧ (and), ∨ (or), → (implication), ¬ (negation), and the quantifiers ∀ (for all), and ∃ (there exists), and also the binary predicate symbol of identity =. A signature is a set of constant, relation ( different from = ) and function symbols. we shall consider here only finite signatures.

Let Sig be a finite signature. We define firstly the set of terms in the signature Sig which is built inductively as follows:

(1) A variable is a term.

(2) A constant symbol is a term.

(3) If F is a m-ary function symbol and t_{1}, t_{2}, …, t_{m} are terms, then F (t_{1}, …, t_{m}) is a term.

We then define the set of atomic formulas which are in the form given below:

(1) If t_{1} and t_{2} are terms, then t_{1} = t_{2} is an atomic formula.

(2) If t_{1}, t_{2}, …, t_{m} are terms and R is a m-ary relation symbol, then R(t_{1}, …, t_{m}) is an atomic formula.

Finally the set of formulas is built inductively from atomic formulas as follows:

(1) An atomic formula is a formula.

(2) If φ and ψ are formulas, then φ ∧ ψ, φ ∨ ψ, φ → ψ and ¬φ are formulas.

(3) If x is a variable and φ is a formula, then ∀xφ and ∃xφ are formulas.

An open formula is a formula with no quantifier.

We assume the reader to know the notion of free and bound occurrences of a variable in a formula. Then a sentence is a formula with no free variable. A sentence in prenex normal form is in the form φ = Q_{1}x_{1} … Q_{n}x_{n}φ_{0}(x_{1}, …, x_{n}), where each Q_{i} is either the quantifier ∀ or the quantifier ∃ and the formula φ_{0} is an open formula. It is well known that every sentence is equivalent to a sentence written in prenex normal form. A sentence is said to be universal if it is in prenex normal form and each quantifier is the universal quantifier ∀.

We then recall the notion of a structure in a signature Sig: A structure is in the form:

M = (|M|, (a^{M})_{a∈Sig})

Where |M| is a set called the universe of the structure, and for a ∈ Sig, a^{M} is the interpretation of a in M: If f is a m-ary function symbol in Sig, then f^{M} is a function: M^{m} → M. If R is a m-ary relation symbol in Sig, then R^{M} is a relation: R^{M} ⊆ M^{m}. If a is a constant symbol in Sig, then a^{M} is a distinguished element in M.

In order to simplify the notations we shall sometimes write a instead of a^{M} when the meaning is clear from the context.

When M is a structure and φ is a sentence in the same signature Sig, we write M ⊧ φ for “ M is a model of φ ”, which means that φ is satisfied in the structure M. A detailed exposition of these notions may be found in [CK73].

When M is a structure in the signature Sig and Sig_{1} is another signature such that Sig_{1} ⊆ Sig, then the reduction of M to the signature Sig_{1} is denoted M|Sig_{1}. It is a structure in the signature Sig_{1} which has same universe |M| as M, and the same interpretations for symbols in Sig_{1}. Conversely an expansion of a structure M in the signature Sig_{1} to a structure in the signature Sig has same universe as M and same interpretations for symbols in Sig_{1}.

When M is a structure in a signature Sig and X ⊆ |M|, we define: cl^{1}(X, M) = X ∪ ⋃_{{f n−ary function of Sig }} f^{M}(X^{n}) ∪ ⋃_{{a constant of Sig }} a^{M} cl^{n+1}(X, M) = cl^{1}(cl^{n}(X, M), M) for an integer n ≥ 1 and cl(X, M) = ⋃_{n≥1} cl^{n}(X, M) is the closure of X in M.

Let us now define locally finite sentences. We shall denote S(φ) the signature of a first order sentence φ, i.e. the set of non logical symbols appearing in φ.

Definition 2.1 A first order sentence φ is locally finite if and only if:

a) M ⊧ φ and X ⊆ |M| imply cl(X, M) ⊧ φ

b) ∃n ∈ ℕ such that ∀M, if M ⊧ φ and X ⊆ |M|, then cl(X, M) = cl^{n}(X, M) (closure in models of φ takes less than n steps).

Notation. For a locally finite sentence φ, we shall denote by n_{φ} the smallest integer n ≥ 1 satisfying b) of the above definition.

Remark 2.2 Because of a) of Definition 2.1, a locally finite sentence φ is always equivalent to a universal sentence.

We now introduce some notations for finite or infinite words. Let Σ be a finite alphabet whose elements are called letters. A finite word over Σ is a finite sequence of letters: x = a_{0} … a_{n} where ∀i ∈ [0; n] a_{i} ∈ Σ. We shall denote x(i) = a_{i} the i + 1^{th} letter of x and x[i] = x(0) … x(i) for i ≤ n. The length of x is |x| = n + 1. The empty word will be denoted by λ and has 0 letter. Its length is 0. The set of finite words over Σ is denoted Σ^{⋆}. Σ^{+} = Σ^{⋆} − {λ} is the set of non-empty words over Σ. A (finitary) language L over Σ is a subset of Σ^{⋆}. Its complement (in Σ^{⋆}) is L^{−} = Σ^{⋆} − L. The usual concatenation product of u and v will be denoted by u.v or just uv. The set of non negative integers is denoted by ℕ. For V ⊆ Σ^{⋆}, we denote V^{⋆} = {v_{1} … v_{n} | ∀i ∈ [1; n] v_{i} ∈ V } ∪ {λ}.

The first infinite ordinal is ω. An ω-word over Σ is an ω-sequence a_{0}a_{1} … a_{n} …, where ∀i ≥ 0 a_{i} ∈ Σ. For σ ∈ Σ^{ω}, σ(n) is the n + 1^{th} letter of σ and σ[n] = σ(0)σ(1) … σ(n). The set of ω-words over the alphabet Σ is denoted by Σ^{ω}. An ω-language over Σ is a subset of Σ^{ω}. The ω-power of a finitary language V ⊆ Σ^{⋆} is the ω-language V^{ω} = {σ = u_{1} … u_{n} … ∈ Σ^{ω} | ∀i ≥ 1 u_{i} ∈ V }. For a subset A ⊆ Σ^{ω}, the complement of A (in Σ^{ω}) is Σ^{ω} − A denoted A^{−}. The concatenation product is extended to the product of a finite word u and an ω-word v: the infinite word u.v is then the ω-word satisfying: (u.v)(k) = u(k) if k < |u| , and (u.v)(k) = v(k − |u|) if k ≥ |u|.

A word over Σ may be considered as a structure in the usual manner:

Let Σ be a finite alphabet. For each letter a ∈ Σ we denote P_{a} a unary predicate and Λ_{Σ} the signature {<, (P_{a})_{a∈Σ}}. The length |σ| of a non-empty finite word σ ∈ Σ^{⋆} may be written |σ| = {0, 1, …, |σ| − 1}. σ is identified to the structure (|σ|, <^{σ}, (P_{a}^{σ})_{a∈Σ}) of signature Λ_{Σ} where P_{a}^{σ} = {i < |σ| | the i + 1^{th} letter of σ is an a}.

In a similar manner if σ is an ω-word over the alphabet Σ, then ω is the length of the word σ and we may write |σ| = ω = {0, 1, 2, 3, …}. σ is identified to the structure (ω, <^{σ}, (P_{a}^{σ})_{a∈Σ}) of signature Λ_{Σ} where P_{a}^{σ} = {i < ω | the i + 1^{th} letter of σ is an a}.

Definition 2.3 Let Σ be a finite alphabet and L ⊆ Σ^{⋆}. Then [L is a locally finite language ] ⟷

there exists a locally finite sentence φ in a signature Λ ⊇ Λ_{Σ} such that σ ∈ L iff ∃M, M ⊧ φ and M|Λ_{Σ} = σ]. We then denote L = L^{Σ}(φ) and, if there is no ambiguity, L = L(φ) the locally finite language defined by φ. The class of locally finite languages will be denoted LOC.

The empty word λ has 0 letters. It is represented by the empty structure. Recall that if L(φ) is a locally finite language then L(φ)−{λ} and L(φ)∪{λ} are also locally finite [Fin01].

Definition 2.4 Let Σ be a finite alphabet and L ⊆ Σ^{ω}. Then [ L is a locally finite ω-language ] ⟷ [ there exists a locally finite sentence φ in a signature Λ ⊇ Λ_{Σ} such that ∀σ ∈ Σ^{ω} σ ∈ L iff ∃M, M ⊧ φ and M|Λ_{Σ} = σ ]. We then denote L = L_{ω}^{Σ}(φ), and, if there is no ambiguity, L = L_{ω}(φ) the locally finite ω-language defined by φ. The class of locally finite ω-languages will be denoted LOC_{ω}.

Remark 2.5 The notion of locally finite (ω)-language is very different of the usual notion of local (ω)-language which represents a subclass of the class of rational (ω)-languages. But from now on, as in [Fin01], things being well defined and precised, we shall call simply local (ω)-languages (respectively, local sentences) the locally finite (ω)-languages (respectively, locally finite sentences).

2.2 Examples of local ω-languages

The following example should not be skipped because it is crucial to Theorem 2.9 below.

Example 2.6 The ω-language which contains only the word σ = abab^{2}ab^{3}ab^{4} … (where the i-th occurrence of a is followed by the factor b^{i}a) is a local ωlanguage over the alphabet {a, b}.

Proof. Let the signature S(φ) = {P_{a}, P_{b}, <, p, p′, f}, where p and p′ are unary function symbols, f is a binary function symbol. And let φ be the following sentence, conjunction of:

(1) ∀xyz[(x ≤ y∨y ≤ x)∧(x ≤ y∧y ≤ x ↔ x = y)∧(x ≤ y∧y ≤ z → x ≤ z)],

(2) ∀x[P_{a}(x) ↔ ¬P_{b}(x)],

(3) ∀xy[(x < y ∧ P_{a}(x) ∧ P_{a}(y)) → P_{b}(f(xy))],

(4) ∀xy[x ≥ y → f(xy) = x],

(5) ∀xy[¬P_{a}(x) ∨ ¬P_{a}(y) → f(xy) = x],

(6) ∀x[P_{a}(p(x)) ∧ P_{a}(p′(x))],

(7) ∀x[¬P_{a}(x) → p(x) < p′(x)],

(8) ∀x[P_{a}(x) → p(x) = p′(x) = x], (9) ∀x[¬P_{a}(x) → x = f(p(x)p′(x))],

(10) ∀xx′y ∈ P_{a}[x < x′ < y → f(x′y) < f(xy) < y],

(11) ∀xyy′ ∈ P_{a}[x ≤ y′ < y → y′ < f(xy) < y].

Above sentence (1) means that “< is a linear order ”. The sentence (2) expresses that P_{a}, P_{b} form a partition in any model M of φ. The sentence (3) says that f is a function from {(x, y) | x < y ∧ P_{a}(x) ∧ P_{a}(y)} into P_{b} while sentences (4)-(5) express that the function f is trivially defined elsewhere. Sentences (6)-(7) say that p and p′ are functions defined from ¬P_{a} = P_{b} into P_{a} and (8) states that p and p′ are trivially defined on P_{a}. The projections p and p′ are used to say that the function f is surjective from {(x, y) | x < y ∧ P_{a}(x) ∧ P_{a}(y)} onto P_{b}; this is implied by sentence (9). The 10^{th} and 11^{th} conjunctions are used to order the elements of f(P_{a} × P_{a}) in order to obtain the word σ = abab^{2}ab^{3}ab^{4} … when the reduction to the signature of words is considered. Notice that (10)-(11) imply also that f is injective hence is in fact a bijection from {(x, y) | x < y ∧ P_{a}(x) ∧ P_{a}(y)} into P_{b}. □

Remark 2.7 We have defined the functions f and p, p′, in a trivial manner (like f(xy) = x or p(x) = x) where they were not useful for defining the local ω-language {σ}, (see the conjunctions (4), (5) and (8)). This will imply that closure in models of φ takes at most a finite number of steps. This method will be applied in the construction of other local sentences in the sequel of this paper.

We can easily check that φ is equivalent to a universal formula and that closure in its models takes at most n_{φ} = 2 steps: one takes closure under the functions p, p′ then by f. Hence φ is a local sentence and by construction: L_{ω}^{{a,b}}(φ) = {abab^{2}ab^{3} …}.

Let us give some examples of closure in a model M of φ such that M|Λ_{{a,b}} = σ = abab^{2}ab^{3}ab^{4} …

Let X_{n} ⊆ |M| be the segment of M corresponding to the segment ab^{n}a of σ. Then the closure of X_{n} under the functions p, p′ is the set X_{n} ∪ Z_{n} where Z_{n} corresponds to the set of the (n − 1) first letters a of σ. cl(X_{n}, M) is the closure of X_{n} ∪ Z_{n} under f and it is the initial segment of M corresponding to the initial segment abab^{2}ab^{3}ab^{4} … ab^{n}a of σ.

Let now Y ⊆ |M| be the segment of M corresponding to the three last letters b^{2}a of the segment ab^{n}a of σ, for some integer n ≥ 3. Then the closure of Y under the functions p, p′ is Y ∪ Z where Z corresponds to the set of the two first letters a of σ. The closure of Y ∪ Z under f is the set cl(Y, M) which induces the word abab^{2}a but which is not a segment of M because it contains the two first letters a and the (n + 1)-th letter a of σ but not any other letter a of σ.

We are going now to get more examples of local ω-languages. Recall first the following:

Definition 2.8 The ω-Kleene closure of a family L of finitary languages is:

ω-KC(L) = {∪_{i=1}^{n}U_{i}.V_{i}^{ω} | ∀i ∈ [1, n] U_{i}, V_{i} ∈ L}

This notion of ω-Kleene closure appears in the characterization of the class REG_{ω} of regular ω-languages (respectively, of the class CF_{ω} of context free ωlanguages) which is the ω-Kleene closure of the family REG of regular finitary languages (respectively, of the family CF of context free finitary languages),

[Tho90] [PP02] [Sta97].

A natural question arises: does a similar characterization hold for local languages? The answer is given by the following:

Theorem 2.9 The ω-Kleene closure of the class LOC of finitary local languages is strictly included into the class LOC_{ω} of local ω-languages.

Proof. We have already proved that ω-KC(LOC) ⊆ LOC_{ω} in [Fin01]. In order to show that the inclusion is strict, remark that if an ω-language L belongs to ω-KC(LOC), then L contains at least an ultimately periodic word, i.e. a word in the form u.v^{ω} where u and v are finite words. Now we can easily check that the local ω-language given in example 2.6 does not contain any ultimately periodic word because its single word is not ultimately periodic. □

A first consequence of Theoreme 2.9 is that every regular ω-language is a local ω-language, i.e. REG_{ω} ⊆ LOC_{ω}, because every finitary regular language is local [Res88]. We had shown in [Fin01] that many context free languages are local thus CF_{ω} = ω-KC(CF) implies that many context free ω-languages are local. The problem to know whether each context free language is local is still open but by Theorem 2.9, CF ⊆ LOC would imply that CF_{ω} ⊆ LOC_{ω}.

The ω-language given in example 2.6 is local but non context free because every context free ω-language contains at least one ultimately periodic word. We proved in [Fin01] that the finitary language U = {a^{n}b^{n^{2}} | n ≥ 1} ⊆ {a, b}^{⋆} is local. Thus the ω-language U.c^{ω} ⊆ {a, b, c}^{ω} is local but U.c^{ω} is not context free because U ∉ CF, [CG77]. These two examples show that the inclusion LOC_{ω} ⊆ CF_{ω} does not hold.

3 Closure properties of locally finite omega languages

Theorem 3.1 The class of locally finite omega languages is not closed under intersection with a regular ω-language in the form L.a^{ω} where L is a rational language, L ⊆ Σ^{⋆} and a ∉ Σ. Hence LOC_{ω} is neither closed under intersection nor under complementation.

To prove this theorem, we shall proceed by successive lemmas. We shall assume that every language considered here is constituted of words over a finite alphabet included in a given countable set Σ_{D}.

We firstly define the family I of finitary languages by: for a finitary language L ⊆ Σ^{⋆}, where Σ ⊆ Σ_{D} is a finite alphabet, L ∈ I if and only if L.a^{ω} ∈ LOC_{ω} whenever a is a letter of Σ_{D} − Σ.

It is easy to see that if L.a^{ω} is a local ω-language and a ∈ Σ_{D} − Σ, then for all b ∈ Σ_{D} − Σ, it holds that L.b^{ω} ∈ LOC_{ω}. It suffices to replace the predicate P_{a} by P_{b} in the sentence defining L.a^{ω}.

Lemma 3.2 I is closed under inverse alphabetic morphism.

Proof. Let L ∈ I , i.e. L ⊆ Γ^{⋆} for some finite alphabet Γ, a ∉ Γ and L.a^{ω} = L_{ω}^{Γ∪{a}}(φ) for a local sentence φ. Let h be the alphabetic morphism: Σ^{⋆} → Γ^{⋆} , defined by h(c) ∈ Γ ∪ {λ} for c ∈ Σ, where λ is the empty word. And let Σ′ = {c ∈ Σ | h(c) = λ}. We assume, possibly changing a, that a ∉ Σ. We first replace in φ the letter predicates (P_{c})_{c∈Γ} by (Q_{c})_{c∈Γ}.

The language h^{−1}(L).a^{ω} is then defined by the following sentence ψ, in the signature S(ψ) = {P, A, (P_{c})_{c∈Σ}, P_{a}} ∪ S(φ), where S(φ) contains the letter predicates Q_{c} for c ∈ Γ ∪ {a}, P is a unary predicate symbol and A is a constant symbol. ψ is the conjunction of:

• ( < is a linear order ),

• ((P_{c})_{c∈Σ}, P_{a}) form a partition,

• ∀x_{1}...x_{n} ∈ P [φ_{0}(x_{1}...x_{n}) ∧ ⋀_{c∈Γ}(Q_{c}(x_{1}) ↔ ⋁_{d∈h^{−1}(c)} P_{d}(x_{1})) ∧ (Q_{a}(x_{1}) ↔ P_{a}(x_{1}))], where φ = ∀x_{1}...x_{n}φ_{0}(x_{1}...x_{n}) with φ_{0} an open formula,

• ∀x_{1}...x_{k}[(⋁_{1≤j≤k} ¬P (x_{j})) → g(x_{1}...x_{k}) = x_{1}] , for each k-ary function g of S(φ),

• (P_{c})_{c∈Σ′} form a partition of ¬P,

• P (B), for each constant B of S(φ),

• ∀xy[¬P_{a}(y) ∧ P_{a}(x) → y < x],

• P_{a}(A). ψ is equivalent to a universal sentence and closure in its models takes at most n_{φ} + 1 steps. Hence ψ is local and by construction L_{ω}^{Σ∪{a}}(ψ) = h^{−1}(L).a^{ω} .□

Lemma 3.3 I is closed under non erasing alphabetic morphism.

Recall that an alphabetic morphism h : Σ^{⋆} → Γ^{⋆}, defined by h(c) ∈ Γ ∪ {λ}, for c ∈ Σ is said to be non erasing if ∀c ∈ Σ, h(c) ∈ Γ.

Proof. Let L ∈ I, L ⊆ Σ^{⋆}. Let a ∉ Σ and L.a^{ω} = L_{ω}^{Σ∪{a}}(φ) for a local sentence φ. Let h be a non erasing alphabetic morphism given by h : Σ → Γ. Moreover we assume that a ∉ Γ (possibly changing a). Then the language h(L).a^{ω} is defined by the following formula ψ, in the signature S(ψ) = S(φ) ∪ {(Q_{c})_{c∈Γ}}. The sentence ψ is the conjunction of:

• φ,

• ∀x[⋀_{c∈Σ}(P_{c}(x) → Q_{h(c)}(x))],

• [(Q_{c})_{c∈Γ}, (P_{a})] form a partition.

ψ is local and if the predicates (Q_{c})_{c∈Γ}, P_{a}, are the letter predicates, ψ defines the ω-language L_{ω}^{Γ∪{a}}(ψ) = h(L).a^{ω} . □

Lemma 3.4 I contains the finitary local languages.

Proof. LOC_{ω} contains the omega Kleene closure of the class LOC of finitary local languages, and for each letter a the language {a} is local. □

Recall now the definitions of the Antidyck language and of a rational cone of languages.

Definition 3.5 The Antidyck language over two sorts of parentheses is the language Q_{2}^{′⋆} = {v ∈ (Y ∪ Ȳ)^{⋆} | v →^{⋆} λ}, where Y = {y_{1}, y_{2}}, Ȳ = {ȳ_{1}, ȳ_{2}} and →^{⋆} is the transitive closure of → defined in (Y ∪ Ȳ)^{⋆} by: ∀y ∈ Y yv_{1}ȳv_{2} → v_{1}v_{2} if and only if v_{1} ∈ Y^{⋆}.

The Antidyck language Q_{2}^{′⋆} may be seen as the language containing words with two sorts of parentheses, such that: “the first parenthesis to be opened is the first to be closed”

Definition 3.6 ([Ber79]) A rational cone is a class of languages which is closed under morphism, inverse morphism, and intersection with a rational language. (Or, equivalently to these three properties, closed under rational transduction).

The notion of rational cone has been much studied. In particular the Antidyck language Q_{2}^{′⋆} is a generator of the rational cone of the recursively enumerable languages, [FZV80].

On the other hand Nivat’s Theorem states that a class of languages which is closed under alphabetic morphism, inverse alphabetic morphism, and intersection with a rational language, is a rational cone, [Ber79]. Moreover every rational transduction t is in the form t(u) = g[h^{−1}(u) ∩ R], where g et h are alphabetic morphisms and R is a rational language. Thus every recursively enumerable language may be written in the form g[h^{−1}(Q_{2}^{′⋆}) ∩ R], where R is a rational language, g and h are alphabetic morphisms. This result will be used here because the language Q_{2}^{′⋆} is local, [Fin01].

Return now to the proof of Theorem 3.1 and suppose that LOC_{ω} were closed under intersection with the languages R.a^{ω}, where R ⊆ Σ^{⋆} is a rational language and a ∉ Σ.

Claim 3.7 I would be closed under intersection with a rational language.

Proof. Let L ∈ I, L ⊆ Σ^{⋆}, R ⊆ Σ^{⋆} be a rational language and a ∉ Σ. L.a^{ω} is a local ω-language because L ∈ I and (L.a^{ω}) ∩ (R.a^{ω}) = (L ∩ R).a^{ω} would be a local ω-language, hence by definition of I, L ∩ R would belong to I. □

Claim 3.8 I would contain every language in the form g[h^{−1}(Q_{2}^{′⋆})∩R], where h is an alphabetic morphism, g is a non erasing alphabetic morphism and R is a rational language.

Proof. It follows from the lemmas 3.2, 3.3, 3.4, the fact that Q_{2}^{′⋆} is local and Claim 3.7. □

Claim 3.9 There would exist an erasing alphabetic morphism h and L ∈ I such that {0^{n}1^{p} | p > 2^{n}} = h(L), where an alphabetic morphism is said to be erasing if it is in the form h : Σ → Σ ∪ {λ}, with h(c) = c if c ∈ A and h(c) = λ if c ∈ Σ − A, for some subset A ⊆ Σ.

Proof. We know that every recursively enumerable language may be written in the form g[h^{−1}(Q_{2}^{′⋆}) ∩ R], where R is a rational language, g and h are alphabetic morphisms. But every alphabetic morphism may be obtained as composed firstly by a non erasing alphabetic morphism followed by an erasing alphabetic morphism. Thus it follows from Claim 3.8 that each recursively enumerable language, and in particular the language {0^{n}1^{p} | p > 2^{n}}, would be the image by an erasing alphabetic morphism of a language of I. □

Let then h be an erasing morphism Σ^{⋆} → Σ^{⋆} where {0, 1} ⊆ Σ, h(0) = 0 and h(1) = 1 and h(c) = λ if c ∈ Σ − {0, 1} and let L ⊆ Σ^{⋆} be a language such that h(L) = {0^{n}1^{p} | p > 2^{n}}. Assume that L belongs to I, so if a ∉ Σ, L.a^{ω} is a local ω-language and there exists a local sentence φ such that L.a^{ω} = L_{ω}^{Σ∪{a}}(φ). For all n ≥ 1 let M_{n} be a model of φ of order type ω such that M_{n} | Λ_{Σ∪{a}} = σ_{n}.a^{ω}, where σ_{n} ∈ Ł and the number of occurrences of 0 in σ_{n} is n and the number of occurrences of 1 in σ_{n} is p_{n} > 2^{n}. Let us now set the following definition in view of next lemma.

Definition 3.10 Let X be a set included in a structure M and P ⊆ |M|. X is a set of indiscernables above P for the atomic formulas of complexity ≤ k, i.e. whose terms result by at most k applications of function symbols, for k ∈ ℕ, if and only if:

i) X is linearly ordered by <. ii) Whenever x̄ and ȳ are some n-tuples of elements of X which are isomor-

phic for the order of (X, <), x̄ and ȳ satisfy the same atomic formulas of complexity ≤ k, with parameters in P.

Lemma 3.11 In the above conditions where M_{n} is defined for every integer n ≥ 1, there exists in M_{n} an infinite set X_{n} of indiscernables above P_{0}^{M_{n}} for the atomic formulas of complexity ≤ n_{φ}, with X_{n} ⊆ P_{a}^{M_{n}}

Proof. Let m(φ) be the maximum number of variables of the atomic formulas of complexity ≤ n_{φ} i.e. whose terms result by at most n_{φ} applications of function symbols. These terms form a finite set T_{φ} .

For all strictly increasing sequences x̄ and ȳ of length m(φ) of P_{a}^{M_{n}} , let us set x̄ ∼ ȳ if and only if x̄ and ȳ satisfy in M_{n} the same atomic formulas with parameters in P_{0}^{M_{n}} and of complexity ≤ n_{φ}.

P_{0}^{M_{n}} is a finite set of cardinal n, hence the set of atomic formulas with parameters in P_{0}^{M_{n}} and of complexity ≤ n_{φ} is also finite.

Then applying the infinite Ramsey Theorem, we can find X_{n} ⊆ P_{a}^{M_{n}} homogeneous for ∼ and infinite. This is the set we are looking for. □

We return now to the proof of Theorem 3.1 and consider in |M_{n}| the subset X_{n} ∪ P_{0}^{M_{n}} = Y_{n}. This subset is infinite hence it is of order type ω in M_{n} and it generates in M_{n} a model of order type ω too, which will be denoted by M_{n}(Y_{n}) = A_{n}.

This model of φ induces a word u_{n}.a^{ω} of L.a^{ω}, such that there are in u_{n}: n occurrences of the letter 0 and q_{n} ≤ p_{n} occurrences of the letter 1. But u_{n}.a^{ω} ∈ L.a^{ω} implies that 2^{n} < q_{n} also holds.

A_{n} is generated from Y_{n} by the use of only a finite set T_{φ} of terms of less than k_{φ} variables. If n is big enough with regard to k_{φ} and card(T_{φ}), because q_{n} > 2^{n}, there exist parameters a_{1}, …, a_{k}, elements of P_{0}^{M_{n}}, and some indiscernables x_{1}, …, x_{j}, and y_{1}, …, y_{j} of X_{n}, such that x_{1} < … < x_{j} and y_{1} < … < y_{j} and x̄ ≠ ȳ and a term t ∈ T_{φ} such that t(a_{1}, …, a_{k}, x_{1}, …, x_{j}) < t(a_{1}, …, a_{k}, y_{1}, …, y_{j}) and these two elements being in P_{1}^{M_{n}}.

But then we could find in X_{n} a sequence (x̄_{i})_{1≤i≤N}, with N arbitrarily large, such that for each i, 1 ≤ i ≤ N, x̄_{i}x̄_{i+1} is of the order type of x̄ȳ.

Then for all integers i such that 1 ≤ i ≤ N, P_{1}^{M_{n}}(t(a_{1}, …, a_{k}, x̄_{i})) and the terms t(a_{1}, …, a_{k}, x̄_{i}) are distinct two by two. This would imply that, for all integers N ≥ 1, card(P_{1}^{M_{n}}) ≥ N. So there would be a contradiction with card(P_{1}^{M_{n}}) = p_{n} and we have proved that L does not belong to I.

Thus we can infer Theorem 3.1 from Claim 3.9. The non closure under complementation of the class LOC_{ω} can be deduced from the non closure under intersection and the fact that LOC_{ω} is closed under union (see next Theorem) or from an example, deduced from preceding proof, of a local ω-language which complement is not local (see next remark). □

Remark 3.12 The above proof shows in particular that the ω-language A = {0^{n}1^{p}2^{ω} | p > 2^{n}} is not local. From which we can easily deduce that the local ω-language {0^{n}1^{p}2^{ω} | p ≤ 2^{n}} = L has a complement which is not a local ω-language. (This ω-language L is local because {0^{n}1^{p} | p ≤ 2^{n}} is a local finitary language [Fin01]). Indeed if its complement was ω-local, we would deduce, from a local sentence φ such that L_{ω}(φ) = L^{−}, another local sentence ψ such that L_{ω}(ψ) = A. For example the sentence ψ, conjunction of:

• φ ,

• ∀xy[(P_{0}(x) ∧ P_{1}(y)) → x < y] ,

• ∀xy[(P_{1}(x) ∧ P_{2}(y)) → x < y] ,

• ∀xy[(P_{0}(x) ∧ P_{2}(y)) → x < y] ,

• P_{2}(c), where c is a new constant symbol.

Now we establish that LOC_{ω} is closed under several operations.

Theorem 3.13 The class LOC_{ω} is closed under union, left concatenation with local (finitary) languages, λ-free substitution of local (finitary) languages, λ-free morphism.

Proof. Closure under union. Let φ_{1} and φ_{2} be two local sentences defining local ω-languages L_{ω}(φ_{1}) and L_{ω}(φ_{2}) over a finite alphabet Σ. Let us define a new local sentence φ_{1} ∪ φ_{2} which defines the local ω-language L_{ω}(φ_{1} ∪ φ_{2}) = L_{ω}(φ_{1}) ∪ L_{ω}(φ_{2}):

We may assume that S(φ_{1}) ∩ S(φ_{2}) = Λ_{Σ}. Then S(φ_{1} ∪ φ_{2}) will be S(φ_{1}) ∪ S(φ_{2}). And the sentence φ_{1} ∪ φ_{2} is the following sentence:

[φ_{1} ⋀_{n−ary function symbol f∈S(φ_{2})}(∀x_{1}, …, x_{n}f(x_{1}, …, x_{n}) = min(x_{1}, …, x_{n}))] ⋁[φ_{2} ⋀_{n−ary function symbol g∈S(φ_{2})}(∀x_{1}, …, x_{n}g(x_{1}, …, x_{n}) = min(x_{1}, …, x_{n}))]

Closure under left concatenation by a local finitary language. Consider a finitary local language L(φ) and a local ω-language L_{ω}(ψ) over the same alphabet Γ. We may easily assume that L_{ω}(φ) is empty, possibly adding a constant symbol c to the signature of φ and adding the conjunction ∀x[x ≤ c] to the sentence φ (this means that every model of φ has a greatest element). We may also assume that S(φ) ∩ S(ψ) = {<, (P_{a})_{a∈Γ}} = Λ_{Γ}. Let then P be a new unary predicate symbol not in S(φ) ∪ S(ψ), and let φ.ψ be the following sentence in the signature S(φ) ∪ S(ψ) ∪ {P }, which is the conjunction of:

• (< is a linear order ),

• ((P_{a})_{a∈Γ} form a partition),

• ∀xy[P (x) ∧ ¬P (y) → x < y],

• ∀x_{1}, …, x_{j} ∈ P [φ_{0}(x_{1}, …, x_{j})], where φ = ∀x_{1}, …, x_{j}φ_{0}(x_{1}, …, x_{j}) with φ_{0} an open formula,

• ∀x_{1}, …, x_{m} ∈ P [f(x_{1}, …, x_{m}) ∈ P], for each m-ary function f of S(φ),

• ∀x_{1}, …, x_{m}[⋁_{1≤i≤m} ¬P (x_{i}) → f(x_{1}, …, x_{m}) = min(x_{1}, …, x_{m})], for each m-ary function f of S(φ),

• P (c), for each constant c of S(φ),

• ∀x_{1}, …, x_{j} ∈ ¬P [ψ_{0}(x_{1}, …, x_{j})], where ψ = ∀x_{1}, …, x_{j}ψ_{0}(x_{1}, …, x_{j}) with ψ_{0} an open formula,

• ∀x_{1}, …, x_{m} ∈ ¬P [f(x_{1}, …, x_{m}) ∈ ¬P], for each m-ary function f of S(ψ),

• ∀x_{1}, …, x_{m}[⋁_{1≤i≤m} P (x_{i}) → f(x_{1}, …, x_{m}) = min(x_{1}, …, x_{m})], for each m-ary function f of S(ψ),

• ¬P (c), for each constant c of S(ψ),

This sentence φ.ψ is equivalent to a universal formula and closure in its models takes at most max(n_{φ}, n_{ψ}) steps, hence it is a local sentence and by construction it holds that L(φ.ψ) = L(φ).L(ψ). Moreover when ω-words are considered L_{ω}(φ.ψ) = L(φ).L_{ω}(ψ) holds because by hypothesis L_{ω}(φ) is empty.

Closure under λ-free substitution of local languages. The proof is very similar to our proof of the closure of the class LOC under substitution by local finitary languages in [Fin01]. We recall it now.

Recall first the notion of substitution: A substitution f is defined by a mapping Σ → P (Γ^{⋆}), where Σ = {a_{1}, ..., a_{n}} and Γ are two finite alphabets, f : a_{i} → L_{i} where ∀i ∈ [1; n], L_{i} is a finitary language over the alphabet Γ. The substitution is said to be λ-free if ∀i ∈ [1; n], L_{i} does not contain the empty word λ. It is a (λ-free) morphism when every language L_{i} contains only one (nonempty) word. Now this mapping is extended in the usual manner to finite words and to finitary languages: for some letters x(0), …, x(n) in Σ, f(x(0)x(1) … x(n)) = {u_{0}u_{1} … u_{n} | ∀i ∈ [0; n] u_{i} ∈ f(x(i))}, and for L ⊆ Σ^{⋆}, f(L) = ∪_{x∈L}f(x). If the substitution f is λ-free, we can extend this to ω-words and ω-languages: f(x(0)x(1) … x(n) …) = {u_{0}u_{1} … u_{n} … | ∀i ≥ 0 u_{i} ∈ f(x(i))} and for L ⊆ Σ^{ω}, f(L) = ∪_{x∈L}f(x).

Let then Σ = {a_{1}, …, a_{n}} be a finite alphabet and let f be a λ-free substitution of local languages: Σ → P (Γ^{⋆}), a_{i} → L_{i} where ∀i ∈ [1; n], L_{i} is a local language defined by the sentence φ_{i}, over the alphabet Γ. We may assume that L_{ω}(φ_{i}) is empty, possibly adding a constant symbol c_{i} to the signature of φ_{i} and adding the conjunction ∀x[x ≤ c_{i}] to the sentence φ_{i} (this means that every model of φ_{i} has a greatest element). We also assume that the signatures of the sentences φ_{i} verify S(φ_{i}) ∩ S(φ_{j}) = {<, (P_{a})_{a∈Γ}} for i ≠ j. Let now L ⊆ Σ^{ω} be a local ω-language defined by a local sentence φ. We shall denote Q_{a_{i}} the unary predicate of S(φ) which indicates the places of the letters a_{i} in a word of L, so if a_{i} ∈ Γ∩Σ for some indice i, there will be two distinct predicates Q_{a_{i}} and P_{a_{i}}. We may also assume that ∀i ∈ [1, …, n], S(φ_{i}) ∩ S(φ) = {<}. Then we can construct a local sentence ψ (already given in [Fin01]) such that L_{ω}(ψ) = f(L). ψ is the conjunction of the following sentences, which meaning is explained below:

• “ < is a linear order ”,

• ∀xy[(I(y) ≤ y) ∧ (y ≤ x → I(y) ≤ I(x)) ∧ (I(y) ≤ x ≤ y → I(x) = I(y))],

• ∀x[I(x) = x ↔ P (x)],

• P (c), for each constant c of S(φ),

• ∀x_{1}, …, x_{k}[R(x_{1}, …, x_{k}) → P (x_{1}) ∧ … ∧ P (x_{k})], for each predicate R(x_{1}, …, x_{k}) of S(φ),

• ∀x_{1}, …, x_{j}[(P (x_{1}) ∧ … ∧ P (x_{j})) → P (f(x_{1}, …, x_{j}))], for each j-ary function symbol f of S(φ),

• ∀x_{1}, …, x_{j}[(⋁_{1≤i≤j} ¬P (x_{i})) → f(x_{1}, …, x_{j}) = min(x_{1}, …, x_{j})], for each j-ary function symbol f of S(φ),

• ∀x_{1}, …, x_{m}[(P (x_{1}) ∧ … ∧ P (x_{m})) → φ_{0}(x_{1}, …, x_{m})], where φ = ∀x_{1}, …, x_{m}φ_{0}(x_{1}, …, x_{m}) with φ_{0} an open formula,

• ∀x_{1}, …, x_{j}[⋁_{i,k≤j}(I(x_{i}) ≠ I(x_{k})) → f(x_{1}, …, x_{j}) = min(x_{1}, …, x_{j})], for every function f of S(φ_{l}) for an integer l ≤ n,

• ∀xy_{1}, …, y_{j}[(⋀_{1≤l≤j} I(y_{l}) = I(x)) → I(f(y_{1}, …, y_{j})) = I(x)], for each j-ary function symbol f of S(φ_{i}) for an integer i ≤ n,

Finally, for each i ≤ n:

• ∀xy_{1}, …, y_{p}[(⋀_{1≤l≤p} I(y_{l}) = I(x) ∧ Q_{a_{i}}(I(x))) → φ_{i}^{0}(y_{1}, …, y_{p}) ∧ {(e_{j}(y_{1}) = I(x) ∧ f_{j}(y_{1}, …, y_{p}) = y_{1} ∧ ¬R_{j}(y_{1}, …, y_{p}) ∧ ⋀_{e_{i}∈S(φ_{i})} e_{i}(y_{1}) = e_{i}(x); where n ≥ j ≠ i, and e_{j}, f_{j}, R_{j} run over the constants, functions, and predicates of S(φ_{j})}],

Above , 1) to each constant e_{l} of S(φ_{l}) is associated a new unary function e_{l}(y) and 2) whenever φ_{i} = ∀y_{1}, …, y_{p}ψ_{i}(y_{1}, …, y_{p}) with ψ_{i} an open formula, φ_{i}^{0} is ψ_{i} in which every constant e_{i} has been replaced by the function e_{i}(y).

Construction of ψ : Using the function I which marks the first letters of the subwords, we divide an ω-word into omega (finite) subwords (the function I is constant on each subword and I(x) is the first letter of the subword containing x). In every model M of order type ω of ψ, the set of the “first letters of subwords” , P^{M}, grows richer in a model of order type ω of φ (therefore will constitute an ω-word of L). Then we “substitute”: for each letter a_{i} in P^{M}, we substitute a (finite) word of L_{i}, using for that the formula φ_{i}. If closure takes at most n_{φ} (respectively n_{φ_{i}}) steps in every model of φ (respectively of φ_{i}), then closure takes at most [1 + n_{φ} + sup_{i}(n_{φ_{i}})] steps in each model of ψ (one takes closure under the function I, then under the functions of S(φ), and finally under the functions of S(φ_{i}), 1 ≤ i ≤ n). Therefore ψ is a local sentence and by construction ψ defines the ω-language f(L).

Closure under λ-free morphism. It is just a particular case of the preceding one, when every language L_{i} contains only one non-empty finite word. □

Acknowledgments. Thanks to the anonymous referees for useful comments on the preliminary version of this paper.

References

[Ber79] J. Berstel, Transductions and Context Free Languages, Teubner Studienbücher Informatik, 1979.

[Büc60] J.R. Büchi, Weak Second Order Arithmetic and Finite Automata, Zeitschrift fur Mathematische Logik und Grundlagen der Mathematik, 6 (1960), pp 66-92.

[Büc62] J.R. Büchi, On a Decision Method in Restricted Second Order Arithmetic, Logic Methodology and Philosophy of Science, ( Proc. 1960 Int. Congr. ). Stanford University Press, 1962, 1-11.

[BS73] J.R. Büchi and D. Siefkes, The Monadic Second Order Theory of All Countable ordinals, Decidable Theories 2, 1973, S.L.N.M. , number 328.

[CG77] R. S. Cohen and A. Y. Gold, Theory of ω-Languages, Parts one and two, Journal of Computer and System Science 15 (1977) 2, 169-184 and 185-208.

[CK73] C.C. Chang and H.J. Keisler, Model Theory, American Elsevier Publishing Company, Inc, New York, 1973. (North Holland, Amsterdam, 3rd ed., 1990).

[DLT98] A. Durand, C. Lautemann and T. Schwentick, Subclasses of Binary-NP, Journal of Logic and Computation, vol. 8(2), 1998, p. 189-207.

[EF95] H. D. Ebbinghaus and J. Flum, Finite Model Theory, Springer Verlag, New York, 1995.

[EGG00] T. Eiter, G. Gottlob and Y. Gurevich, Existential Second-Order Logic over Strings, IEEE Symposium on Logic in Computer Science (LICS’98), Journal of the ACM, vol. 47, no. 1, Jan. 2000, 77–131.

[Fag74] R. Fagin, Generalized First-Order Spectra and Polynomial-Time Recogniza -ble Sets, in: R.M. Karp, ed., Complexity of Computation, SIAM-AMS Proc. 7 (1974) p. 43-73.

[Fag93] R. Fagin, Finite-Model Theory, A Personal Perspective, Theoretical Computer Science, Volume 116 (1993) p. 3-31.

[Fin89] O.Finkel, Langages de Büchi et ω-Langages Locaux, C.R.A.S. Paris, t.309, Série 1, p. 991-994, 1989.

[Fin93] O.Finkel, Théorie des Modèles des Formules Locales et Etude des Langages Formels qu’ elles Définissent, Ph. D. Thesis, University Paris 7, May 1993.

[FR96] O. Finkel and J-P. Ressayre, Stretchings, Journal of Symbolic Logic, Volume 61, number 2, June 1996, p. 563-585.

[Fin01] O. Finkel, Locally Finite Languages, Theoretical Computer Science, Volume 255 (1-2), March 2001, p.223-261.

[FZV80] P. Franchi-Zanettacci and B. Vauquelin, Automates à Files, Theoretical Computer Science, Volume 11 (1980), p.221-225.

[GKS00] G. Gottlob, P. G. Kolaitis, T. Schwentick, Existential Second-Order Logic over Graphs: Charting the Tractability Frontier, FOCS 2000, p. 664-674.

[Hac01] Y. Hachaichi, Contributions à la Théorie des Modèles Finis et à la Complexité Descriptive, Ph. D. Thesis, university Paris 7, July 2001.

[HU69] J.E. Hopcroft and J.D. Ullman, Formal Languages and their Relation to Automata, Addison-Wesley Publishing Company, Reading, Massachussetts, 1969.

[Imm87] N. Immerman, Languages That Capture Complexity Classes, SIAM J. of Computing 16:4 (1987), p. 347-354.

[Imm99] N. Immerman, Descriptive Complexity, Springer Graduate Texts in Computer Science, 1999.

[LST94] C. Lauteman, T. Schwentick and D. Therien, Logics for Context Free Languages, in the Proceedings of Computer Science Logic 94, p. 205-216.

[LT94] H. Lescow and W. Thomas, Logical Specifications of Infinite Computations, In:“A Decade of Concurrency” (J. W. de Bakker et al., eds), Springer LNCS 803 (1994), 583-621.

[PP85] M. Parigot and E. Pelz, A Logical Approach of Petri Net Languages, Theoretical Computer Science, Volume 39 (1985) p. 155-169.

[Pel87] E. Pelz, Infinitary Languages of Petri Nets and Logical Sentences, Advances in Petri Nets 1987 (Oxford, 1986), Lecture Notes in Comput. Sci., 266, Springer, Berlin, 1987, p. 224-237.

[PP02] D. Perrin and J.-E. Pin, Infinite Words, Book in preparation, available from http://www.liafa.jussieu.fr/∼jep/InfiniteWords.html

[Pin96] J-E. Pin, Logic, Semigroups and Automata on Words, Annals of Mathematics and Artificial Intelligence 16 (1996), p. 343-384.

[Res88] J-P. Ressayre, Formal Languages Defined by the Underlying Structure of their Words, Journal of Symbolic Logic, 53, number 4, December 1988, p. 1009-1026.

[Res89] J-P. Ressayre, Question posed during a Working Group on Automata and Logic at University Paris 7, 1989.

[Sta97] L. Staiger, ω-Languages, Chapter of the Handbook of Formal languages, Vol. 3, edited by G. Rozenberg and A. Salomaa, Springer-Verlag, Berlin.

[Tho90] W. Thomas, Automata on Infinite Objects, in: J. Van Leeuwen, ed., Handbook of Theoretical Computer Science, Vol. B ( Elsevier, Amsterdam, 1990 ), p. 133-191.

[Tho96] W. Thomas, Languages, Automata and Logic, in Handbook of Formal Languages Theory, Vol. 3, Edited by G. Rozenberg and A. Salomaa, Springer Verlag, 1996.

[Yam99] H. Yamasaki, Logical Characterization of Petri Net ω-Languages, Report 99-17, Department of Mathematics and Computer Science, Martin-Luther-Universität Halle-Wittenberg, 1999.