Zoltán Ésik

Szabolcs Iván

MSO-definable properties of Muller context-free languages are decidable ⋆

We show that it is decidable given an MSO-definable prop-

Introduction

A word, called 'arrangement' in [START_REF] Courcelle | Frontiers of infinite trees[END_REF], is an isomorphism type of a countable labeled linear order. Such words form a generalization of the classic notions of finite and ω-words.

Finite automata on ω-words have by now a vast literature, see [START_REF] Perrin | Infinite Words: Automata, Semigroups, Logic and Games[END_REF] for a comprehensive treatment. Finite automata acting on well-ordered words longer than ω have been investigated in [START_REF] Bedon | Finite automata and ordinals[END_REF][START_REF] Büchi | The monadic second order theory of ω1[END_REF][START_REF] Choueka | Finite automata, definable sets, and regular expressions over ω n -tapes[END_REF][START_REF] Wojciechowski | Classes of transfinite sequences accepted by finite automata[END_REF][START_REF] Wojciechowski | Finite automata on transfinite sequences and regular expressions[END_REF], to mention a few references. In the last decade, the theory of automata on well-ordered words has been extended to automata on all countable words, including scattered and dense words. In [START_REF] Bedon | Logic and rational languages of words indexed by linear orderings[END_REF][START_REF] Bès | A kleene theorem for languages of words indexed by linear orderings[END_REF][START_REF] Bruyère | Automata on linear orderings[END_REF], both operational and logical characterizations of the class of languages of countable words recognized by finite automata were obtained.

Context-free grammars generating ω-words were introduced in [START_REF] Cohen | Theory of ω-languages, parts one and two[END_REF] and subsequently studied in [START_REF] Boasson | Context-free sets of infinite words[END_REF][START_REF] Nivat | Sur les ensembles de mots infinis engendrés par une grammaire algébrique[END_REF]. Context-free grammars generating arbitrary countable words were defined in [START_REF] Ésik | Büchi context-free languages[END_REF][START_REF] Ésik | On Müller context-free grammars[END_REF]. Actually, two types of grammars were defined, context-free grammars with Büchi acceptance condition (BCFG), and contextfree grammars with Muller acceptance condition (MCFG). These grammars generate the Büchi and the Muller context-free languages of countable words, abbreviated as BCFLs and MCFLs. Every BCFL is clearly an MCFL, but there exists an MCFL of well-ordered words that is not a BCFL, for example the set of all countable well-ordered words over some alphabet. In contrast, the set of all countable words over an alphabet is a BCFL.

In [START_REF] Ésik | On Müller context-free grammars[END_REF], it was shown that it is decidable (in polynomial time) whether a given MCFG generates well-ordered (or scattered) words only. This result was obtained by analysing the structure of a finite graph canonically associated with the grammar. In this note we establish a generic decidability result to the effect that whenever P is some property of countable words definable in monadic second-order logic (MSO), e.g., being well-ordered or scattered, then it is decidable whether an MCFG generates only words satisfying P . Of course for such a general setting one cannot hope for efficient algorithms since model checking MSO is nonelementary.

The main idea of the proof is that one can associate with each MCFG a regular tree in which every derivation tree of the grammar can be represented and moreover, the set of all derivation trees is MSO-definable.

Notation

Countable words and Muller context-free grammars. An alphabet is a finite nonempty set Σ of symbols, usually called letters. A word over Σ is a strict linear ordering (I, <) equipped with a labeling function λ : I → Σ. The empty word, denoted ε, is the unique word over the empty ordering. It is assumed that no alphabet contains ε. When Σ is an alphabet, Σ ε stands for Σ ∪ {ε}. An embedding of words is a mapping between the respective underlying linear orderings that preserves the order and the labeling; a surjective embedding is an isomorphism. We usually identify isomorphic words and denote by Σ ♯ the set of all countable words over the alphabet Σ. As usual, we denote the collections of finite and ω-words over Σ by Σ * and Σ ω , respectively. Sometimes we will also use the same notation for infinite sets.

Let N denote the set of positive integers. When u ∈ N * and i ∈ N, we usually write ui as u • i. A tree domain D is a prefix-and left-sibling closed nonempty (but possibly infinite) subset of N * . Thus, whenever u • (i + 1) is in D, where i ∈ N, then u • i is also in D, and u • i ∈ D implies u ∈ D as well. Elements of a tree domain D are also called the nodes of D. When u and u • i are nodes of D, where u ∈ N * and i ∈ N, then u • i is called a child of u. A descendant of a node u is a node of the form uv, or u • v, where v ∈ N * . Nodes of D having no child are the leaves of D. The leaves, equipped with the order inherited from the lexicographic ordering ≺ ℓ of N * (that is, u ≺ ℓ v iff u = wiw ′ and v = wjw ′′ for some i < j ∈ N, w, w ′ , w ′′ ∈ N * ) form the frontier of D, denoted fr(D). An inner node of D is a non-leaf node. A path of a tree domain D is a (finite or infinite) prefix-closed subset π of D such that each node of π has at most one child in π. Given a tree domain D and some node u ∈ D, the sub-tree domain of D rooted at u is the tree domain D| u = {v : uv ∈ D}.

A tree over some alphabet ∆, or a ∆-tree for short, is a mapping t : dom(t) → ∆ ε , where dom(t) is a tree domain, such that inner vertices are mapped to letters in ∆. Notions such as nodes, paths etc. of tree domains are lifted to trees. When π is a path of the tree t, then labels(π) = {t(u) : u ∈ π} is the set of labels occurring on π and infLabels(π) = u∈π {t(v) : uv ∈ π} ⊆ labels(π) is the set of labels occurring infinitely often. Given a tree t and some node u ∈ dom(t), the subtree of t rooted at u is the tree t| u with domain dom(t| u ) = dom(t)| u and labeling t| u (v) = t(uv). A tree is regular if it has finitely many subtrees.

The frontier word lfr(t) of a tree t is determined by the leaves not labeled by ε, which is equipped with the lexicographic ordering of N * and the labeling function inherited from t. The root symbol of t is t(ε).

A Muller context-free grammar [START_REF] Ésik | On Müller context-free grammars[END_REF], or MCFG for short, is a system G = (V, Σ, R, S, F ), where V and Σ are the pairwise disjoint alphabets of nonterminals and terminals respectively, R is the finite set of productions of the form A → α with A ∈ V and α ∈ (Σ ∪ V ) * , S ∈ V is the start symbol and F ⊆ P (V ) is the set of accepting sets.

A (V ∪ Σ)-tree t is locally consistent with the above grammar G if it satisfies the following conditions:

1. The root symbol of t is S. 2. For each inner node u of t there exists a production A → X

1 . . . X n in R with t(u) = A, X i ∈ V ∪ Σ such that: (a) either n > 0, the children of u are exactly u • 1, . . . , u • n and for each 1 ≤ i ≤ n, t(u • i) = X i ; (b) or n = 0 and u has a single child u • 1 labeled ε. 3. The leaves of t are labeled in Σ ε .
A derivation tree of the above grammar G is a locally consistent tree t satisfying the additional condition that for each infinite path π of t, infLabels(π) is an accepting set of G.

The language L(G) ⊆ Σ ♯ generated by G is the set of frontier words of derivation trees. A Muller context-free language, or MCFL for short, is a language generated by some MCFG.

Example 1. If G = ({S, I}, {a, b}, R, S, {{I}}), with R = {S → a, S → b, S → ε, S → I, I → SI},
then L(G) consists of all the well-ordered words over {a, b}.

Indeed, assume t 1 , t 2 , . . . are derivation trees. Then so is the tree t depicted in Figure 1 with frontier word lfr(t 1 )lfr(t 2 ) . . .. Thus, L(G) contains the empty word (by S → ε), the words of length 1 (by S → a and S → b), and is closed under taking "ω-products". Since the least class of order types which contains 0, 1 and which is closed under ω-sums is the class of all countable ordinals (see e.g. [START_REF] Rosenstein | Linear orderings[END_REF]), L(G) contains all the well-ordered words over {a, b}. For the other direction, assume t is a derivation tree having a frontier word containing an infinite descending chain u 1 ≻ ℓ u 2 ≻ ℓ . . .. Then let us define the path v 0 , v 1 , . . . in t: v 0 = ε and v i+1 is v i •1 if this node is an ancestor of infinitely many u j and v i • 2 otherwise (which happens if v i corresponds to the production I → SI and the node v i • 1 (which is labeled S) has no descendant of the form u j at all). Note that for each u j there exists a unique v ij such that v ij is an ancestor of u j and v ij +1 is not, since the length of the words v i grows without a bound. Now these nodes v ij correspond to the production I → SI and v ij +1 = v ij • 1, so that the successor of v ij along the path is labeled by S. Hence v 0 , v 1 , . . . , is a path π in t such that infLabels(π) contains S, which is a contradiction since the only accepting set is {I}.

MSO on trees and words. Let X 1 and X 2 be fixed, countably infinite, disjoint sets of first-order and second-order variables, respectively. It is assumed that X 1 and X 2 are disjoint from alphabets, they do not contain ε, etc.

Given an alphabet ∆, the set of monadic second-order, or MSO-formulas (for trees over ∆) is the least set satisfying the following conditions:

1. When x is a first-order variable and δ ∈ ∆ ε is a symbol, then δ(x) is an MSO-formula. 2. When x and y are first-order variables, then y = x • 1 and sibling(x, y) are MSO-formulas. 3. When x is a first-order and X is a second-order variable, then X(x), also written x ∈ X is an MSO-formula. 4. When ϕ and ψ are MSO-formulas, then so are (ϕ ∨ ψ) and (¬ϕ). 5. When x (X, resp.) is a first-order (second-order, resp.) variable and ϕ is an MSO-formula, then so is (∃xϕ) ((∃Xϕ), resp).

We also use the standard abbreviations of ϕ∧ψ = ¬(¬ϕ∨¬ψ), ϕ → ψ = (¬ϕ)∨ψ, ∀xϕ = ¬∃x¬ϕ etc., and omit some parentheses for the sake of readability.

Formulas over ∆ are interpreted on ∆-trees in the expected way. A structure is a triple (t, Π 1 , Π 2 ) where t is a ∆-tree, Π 1 : X 1 → dom(t) assigns a node of t to each first-order variable, and Π 2 : X 2 → P (dom(t)) assigns a set of nodes of t to each second-order variable. Then, the above structure satisfies the formula ϕ, denoted (t, Π 1 , Π 2 ) |= ϕ, if and only if one of the following conditions holds:

1. ϕ = δ(x) for δ ∈ ∆ ε and x ∈ X 1 , and t(Π 1 (x)) = δ. 2. ϕ = (y = x • 1) for x, y ∈ X 1 and Π 1 (y) = Π 1 (x) • 1. 3. ϕ = sibling(x, y) for x, y ∈ X 1 and there exist u ∈ N * , i ∈ N with Π 1 (x) = u • i, Π 1 (y) = u • (i + 1). 4. ϕ = X(x) for x ∈ X 1 , X ∈ X 2 and Π 1 (x) ∈ Π 2 (X). 5. ϕ = (ϕ 1 ∨ ϕ 2
) and (t, Π 1 , Π 2 ) satisfies ϕ 1 or ϕ 2 (or both). 6. ϕ = (¬ϕ 1 ) and it is not the case that the structure satisfies ϕ 1 . 7. ϕ = (∃xϕ 1 ) and there is a structure (t, Π ′ 1 , Π 2 ) satisfying ϕ 1 such that Π 1 (y) = Π ′ 1 (y) for each first-order variable y = x. 8. ϕ = (∃Xϕ 1 ) and there is a structure (t,

Π 1 , Π ′ 2 ) satisfying ϕ 1 such that Π 2 (Y ) = Π ′ 2 (Y ) for each second-order variable Y = X.
It is clear that satisfaction depends on Π 1 (x) or Π 2 (X) only if the appropriate variable occurs freely in the formula (i.e. not within the scope of some ∃ quantifier). Hence when ϕ is a sentence, a formula without free variable occurrences, it makes sense to write t |= ϕ instead of (t, Π 1 , Π 2 ) |= ϕ.

In order to ease notation, when Π 1 and Π 2 are clear from the context, we write x and X for Π 1 (x) and Π 2 (X).

Example 2. One can define the i-th child relation y = x • i for i ∈ N inductively as ∃z(z = x • (i -1) ∧ sibling(z, y)) (which is satisfied by a structure if and only if y = x • i).

Consider the formula

child(x, y) = ∃z(z = x • 1) ∧ ∀X ∀z (z = x • 1) → z ∈ X ∧ ∀z∀w(z ∈ X ∧ sibling(z, w) → w ∈ X) → y ∈ X .
Then, child(x, y) holds in the structure iff x has a first child and if whenever a set X contains the first child of x and is closed under taking right siblings, then X contains y as well, that is, if and only if y = x • i for some i.

As another example, the formula

∃x(x ∈ X) ∧ ∀x∀y(x ∈ X ∧ child(y, x) → y ∈ X)
holds in a structure if X is a nonempty, prefix-closed subset of the nodes.

It is well-known [START_REF] Michael | Decidability of second order theories and automata on infinite trees[END_REF] that given any regular tree t and MSO sentence ϕ, it is decidable whether t |= ϕ holds.

For countable Σ-words, the syntax and semantics of MSO are slightly changed due to the differing relational structure: the atomic formulas are of the form a(x) for a ∈ Σ and x ∈ X 1 and x < y for x, y ∈ X 1 , interpreted in the expected way. A property P of countable Σ-words is called MSO-definable if there exists an MSO sentence ϕ P which is satisfied exactly by those Σ-words having property P .

Result

Let us fix a Muller context-free grammar G = (V, Σ, R, S, F ) for this section, with R being disjoint from V ∪ Σ. Without loss of generality we assume that each A ∈ V is the left-hand side of at least one production. We define the grammar tree associated with G as the unique derivation tree T of the following grammar G ′ = (V ∪ R, Σ, R ′ , S, P (V ∪ R)) with R ′ consisting of productions of the following form:

1. When A → α 1 ,. . . ,A → α k are all the productions of G having A on their left side in some fixed ordering of the productions, then A → (A → α 1 )(A → α 2 ) . . . (A → α k ) is a production of G ′ (the right-hand side of this single production is in R * while the left-hand side is in V ).

For each production

A → X 1 . . . X k , the production (A → X 1 . . . X k ) → X 1 . . . X k .
(which is a production of the form r → α for some r ∈ R and

α ∈ (V ∪ Σ) * ) is a production of G ′ .
Note that each element of V ∪ R is the left-hand side of exactly one production in R ′ , hence there exists exactly one locally consistent tree of G ′ . Also, since the acceptance condition is P (V ∪ R), this tree is a valid derivation tree of the grammar, thus T is well-defined and has at most

|V | + |R| + |Σ ε | subtrees up to isomorphism.
Hence it is a regular tree.

Example 3. For the MCFG of Example 1, this tree T is depicted in Figure 2. Moreover, each locally consistent tree t of G can be embedded into T in the following sense: there exists a mapping h t : dom(t) → dom(T ) with h t (ε) = ε and t(u) = T (h t (u)) for each u ∈ dom(t), moreover h t (u • i) is a descendant (in particular, a grandchild) of h t (u) in T for each u • i ∈ dom(t), moreover, when u and v are siblings in t, then so are h t (u) and h t (v) in T . Indeed, assume u•i ∈ dom(t) and that u ′ = h t (u) is already defined. Then since u is an inner node of t, we have t(u) = A ∈ V . By T (u ′ ) = t(u) = A, each production r = A → α occurs as T (u ′ • k r ) for some k r ∈ N. In particular, let r = A → X 1 . . . X n be the production corresponding to u, so that u has n children and t(u • j) = X j for each j = 1, . . . , n (subsuming the case when n = 0 as t(u

• 1) = ε). Then, we define h t (u • j) as u ′ • k r • j.
We call a prefix-closed nonempty set T ⊆ dom(T ) derivation-like iff it satisfies the following conditions:

1. For each u ∈ T with T (u) ∈ R, each child of u is in T . 2. For each u ∈ T with T (u) ∈ V , exactly one child of u is in T .
It is clear that derivation-like subsets of dom(T ) are in one-to-one correspondence with the locally consistent trees of G: with any locally consistent tree t of G we associate the derivation-like set T ⊆ dom(T ) which is the closure of im(h t ) with respect to the prefix relation. Given a derivation-like set T , the corresponding locally consistent tree is denoted t. There is an MSO formula d(X) with the free variable X ∈ X 2 such that (T , Π 1 , Π 2 ) |= d(X) if and only if X is a derivation-like set.

(In short, it is MSO-definable whether some set X is derivation-like.)

Proof. We can define d(X) as the conjunction of the formulas stating that X is nonempty and prefix-closed (see Example 2), the formula

∀x (x ∈ X ∧ r∈R r(x)) → ∀y(child(x, y) → y ∈ X)
stating that all the children of the nodes labeled by productions are members of X, and the formula

∀x (x ∈ X ∧ A∈V A(x)) → ∃y child(x, y) ∧ ∀z(child(x, z) ∧ z ∈ X ↔ z = y)
stating that exactly one child of the nodes labeled by nonterminals is in X. ⊓ ⊔ Also, from a derivation-like set T determining a locally consistent tree t of G, one can select a subset of nodes corresponding to a path of t:

Proposition 2. There exists an MSO-formula p(X, Y ) with the free secondorder variables X, Y such that (T , Π 1 , Π 2 ) |= p(X, Y ) if and only if X = T is a derivation-like subset of T with corresponding locally consistent tree t and Y = h t (π)1 for some infinite path π of t.

Proof. p(X, Y ) expresses the following:

i) X is a derivation-like subset of T , i.e. d(X) holds, ii) Y ⊆ X,
iii) each of the nodes of Y is labeled by some member of V , iv) whenever v is a grandparent of some node u ∈ Y , then v ∈ Y as well, and v) each u ∈ Y has exactly one grandchild in Y .

These properties can clearly be defined in MSO.

⊓ ⊔

Proposition 3. There is an MSO formula d ′ (X) expressing that X is a derivation-like set corresponding to an actual derivation tree of G.

Proof. The descendant relation x y can be defined in MSO by a formula expressing that whenever Y is a prefix-closed set containing y, then Y contains x as well.

Then, for each F ∈ F we can construct a formula m F (Y ) stating that if Y = h t (π) for some path π of some locally consistent tree t of G, then infLabels(π) = F :

m F (Y ) = A∈F i A (Y ) ∧ A / ∈F ¬i A (Y )
where i A (Y ) is the formula

∀x(x ∈ Y → ∃y(x y ∧ y ∈ Y ∧ A(y)))
stating that A occurs infinitely many times on the path given by Y . Now, we can define d ′ (X) as

d(X) ∧ ∀Y (p(X, Y ) → F ∈F m F (Y ))
expressing that X is a derivation-like set corresponding to some locally consistent tree t of G such that any infinite path π of t satisfies the Muller acceptance condition.

⊓ ⊔

Now a set Y ⊆ dom(T ) corresponds to a frontier word of some derivation tree of G (i.e. belongs to L(G)) if and only if there exists some X ⊆ dom(T ) satisfying d ′ (X) such that a node v ∈ dom(T ) is in Y if and only if v ∈ X and is a Σ-labeled node of T , which is an MSO-definable property:

∃X d ′ (X) ∧ ∀y(y ∈ Y ↔ (y ∈ X ∧ a∈Σ a(y))) .
Moreover, the lexicographic ordering on these leaves can also be defined in MSO as u ≺ ℓ v iff there exists some common ancestor w of u and v such that w • i and w • j are respectively ancestors of u and v for some i < j:

x ≺ ℓ y = ∃z 1 ∃z 2 z 1 x ∧ z 2 y ∧ sibling + (z 1 , z 2 )
where sibling + (x, y) is the transitive closure of sibling:

x = y ∧ ∀X x ∈ X ∧ ∀z 1 ∀z 2 (z 1 ∈ X ∧ sibling(z 1 , z 2 ) → z 2 ∈ X) → y ∈ X
Hence we have shown: Proposition 4. For any MCFG G, there exists an effectively constructible MSO formula w(Y ) such that (T , Π 1 , Π 2 ) |= w(Y ) if and only Y is the set of Σ-labeled leaves of some derivation-like subset of T corresponding to a derivation tree of G.

As a corollary, we obtain the main result of this note.

Theorem 1. It is decidable for a given MCFL L and an MSO-definable property ϕ of words whether every member of L satisfies ϕ.

Proof. The question can be reduced to checking whether T satisfies the formula ∀Y (w(Y ) → ϕ(Y )) where ϕ(Y ) is obtained from ϕ by replacing all the subformulas of the form ∃xϕ ′ and ∃Xϕ ′ respectively to ∃x(x ∈ Y ∧ ϕ ′ ) and ∃X(∀x(x ∈ X → x ∈ Y )) ∧ ϕ ′ ) and substituting the formula defining the lexicographic ordering x ≺ ℓ y in place of the atomic formulas x < y. Since T is regular, model checking the resulting formula on T is decidable.

⊓ ⊔ (We remark that thus it is also decidable whether there exists a word in L satisfying an MSO formula ϕ since such a word exists if and only if not all members of L satisfy ¬ϕ.)

In particular, our former decidability results (without complexity bounds) regarding whether an MCFG generates scattered (or well-ordered) words are corollaries of this general theorem. However, since model-checking MSO formulas on regular trees has a high complexity in general (tower(n) when n is the alternation depth of the second-order quantifiers), no polytime decision procedures follow from the present theorem. Nevertheless several interesting properties are decidable in polynomial time, including whether every word generated by an MFCG is scattered or well-ordered, cf. [START_REF] Ésik | On Müller context-free grammars[END_REF].

As another example, let Σ = {a, b} be an alphabet. The following formula segment(X) expresses that X is a nonempty interval, or segment of a given word:

(∃x x ∈ X) ∧ ∀x∀y∀z(x < y ∧ y < z ∧ x ∈ X ∧ z ∈ X) → y ∈ X .
The following formula dense(X) expresses that X is a dense subset (containing at least two elements) of the word:

∃x∃y(x < y ∧ x ∈ X ∧ y ∈ X) ∧ ∀x∀y x < y ∧ x ∈ X ∧ y ∈ X → ∃z(x < z ∧ z < y ∧ z ∈ X) .
Thus, the property "there exists a dense segment X of the word such that for all x < y in X there exists z, z ′ with x < z, z ′ < y and z is labeled by a, z ′ is labeled by b" is also expressible in MSO as

∃X dense(X) ∧ segment(X) ∧ ∀x∀y x < y ∧ x ∈ X ∧ y ∈ X → ∃z∃z ′ (x < z ∧ z < y ∧ x < z ′ ∧ z ′ < y ∧ a(z) ∧ b(z ′ ))
In other words, w ∈ {a, b} ♯ satisfies the above formula iff w = u{a, b} η v for some words u, v ∈ {a, b} ♯ where {a, b} η is the so-called shuffle of a and b. Thus, it is also decidable for a MCFL L whether every word in L is of the form u{a, b} η v.

Another expressible property is that whether a word is the shuffle product of, say, a dense word and a scattered word consisting only of a's, that is, whether the underlying linear order can be partitioned into two subsets such that the two subwords determined by the partitions satisfy the appropriate property:

∃X dense(X)∧∀x(x / ∈ X → a(x))∧¬∃Y ∀x(x ∈ Y → x / ∈ X) ∧ dense(Y ) .
Thus, it is also decidable for a given MCFL L whether every member of L is a shuffle product of a dense word and a scattered one consisting only of a's.

Conclusion

We have proved that there is an algorithm to decide for a Muller context-free language L generated by an MCFG and an MSO-definable property P of words whether every word in L has property P . We obtained this result by assigning a regular tree t to an MCFG such that the derivation trees of the grammar have an MSO-interpretation in t. We then used the fact that the MSO-theory of a regular tree is decidable.

There is an alternative method. First, we can prove that the MCFLs are exactly the frontier languages of the tree languages recognizable by Muller tree automata. This is similar to the well-known fact that ordinary context-free languages are the frontier languages of the languages of finite trees recognizable by finite tree automata. Also, there is an algorithm to decide, for a Muller tree automaton and an MSO-definable property of trees whether every tree in the language L recognized by the automaton has property P . This follows using the fact that every Muller tree automaton can be converted to an MSO-formula ϕ, and if P is definable by the formula ψ, then it holds that every tree in L satisfies P iff there is no tree satisfying ϕ ∧ ¬ψ, which is decidable.

Fig. 1 .

 1 Fig. 1. Derivation tree corresponding to Example 1

Fig. 2 .

 2 Fig. 2. Grammar tree of the MCFG of Example 1

Example 4 .

 4

Figure 3 Fig. 3 .

 33 Fig. 3. A part of a derivation tree t of Example 1 and the corresponding derivation-like subset T of T

⋆ This research was supported by NKFI grant number K108448.

Here, ht(π) denotes the set of images of the nodes of π with respect to the embedding ht.


Lukas Fleischer
email: fleischer@fmi.uni-stuttgart.de

Manfred Kufleitner
email: kufleitner@fmi.uni-stuttgart.de

Operations on Weakly Recognizing Morphisms

Weakly recognizing morphisms from free semigroups onto finite semigroups are a classical way for defining the class of ω-regular languages, i.e., a set of infinite words is weakly recognizable by such a morphism if and only if it is accepted by some Büchi automaton. We consider the descriptional complexity of various constructions for weakly recognizing morphisms. This includes the conversion from and to Büchi automata, the conversion into strongly recognizing morphisms, and complementation. For some problems, we are able to give more precise bounds in the case of binary alphabets or simple semigroups.

Introduction

Büchi automata define the class of ω-regular languages. They were introduced by Büchi for deciding the monadic second-order theory of (N, <) [START_REF] Büchi | Weak second-order arithmetic and finite automata[END_REF]. Since then, ω-regular languages have become an important tool in formal verification, and many other automata models for this language class have been considered; see e.g. [START_REF] Perrin | Infinite words[END_REF][START_REF] Thomas | Automata on infinite objects[END_REF]. Each automaton model has its merits and its disadvantages. Recently, the authors have shown that recognizing morphisms have many nice algorithmic properties [START_REF] Fleischer | Efficient Algorithms for Morphisms over Omega-Regular Languages[END_REF]. Such morphisms come in two different flavors. Strongly recognizing morphisms admit efficient minimization and complementation, whereas weakly recognizing morphisms can be exponentially more succinct (but there is no minimal weak recognizer and there is no efficient complementation). The situation is similar to the behavior of deterministic and nondeterministic finite automata. The major difference to both nondeterministic finite automata and Büchi automata is that there is an efficient inclusion test for weakly recognizing morphisms [START_REF] Fleischer | Efficient Algorithms for Morphisms over Omega-Regular Languages[END_REF]. Every strongly recognizing morphism is also weakly recognizing, but the converse is false.

In this paper, we consider the descriptional complexity of various operations on weakly recognizing morphisms and conversions involving nondeterministic Büchi automata (BA) and strongly recognizing morphisms. In each case, we give asymptotically tight bounds. For the conversion of a BA into a weakly recognizing morphism, we give a lower bound which matches the naive upper bound. Our results are summarized in Table 1.

There are some similarities between recognizing morphisms over finite and over infinite words. Strong recognition is the natural counterpart to recognition This work was supported by the DFG grants DI 435/5-2 and KU 2716/1-1. for finite words. Nevertheless, in order to prove lower bounds for the conversion of Büchi automata to weakly recognizing morphisms, we first show that bounds for converting nondeterministic finite automata to recognizing morphisms over finite words (with some limitations) also hold for the conversion of Büchi automata to weakly recognizing morphisms. We then use techniques of Sakoda and Sipser [START_REF] Sakoda | Nondeterminism and the size of two way finite automata[END_REF] and of Yan [START_REF] Yan | Lower bounds for complementation of omega-automata via the full automata technique[END_REF] to obtain tight bounds for the conversion of nondeterministic finite automata to recognizing morphisms. This step is similar to the work of Holzer and König [START_REF] Holzer | On deterministic finite automata and syntactic monoid size[END_REF]. To the best of our knowledge, our lower bound over finite words for the conversion of an NFA into a recognizing morphism is also a new result.

Operation

Preliminaries

This section gives a brief overview of some basic definitions from the fields of formal languages, finite automata and semigroup theory. We refer to [START_REF] Perrin | Infinite words[END_REF][START_REF] Pin | Varieties of Formal Languages[END_REF] for more detailed introductions.

Words.

Let A be a finite alphabet. The elements of A are called letters. A finite word is a sequence a 1 a 2 • • • a n of letters of A and an infinite word is an infinite sequence a 1 a 2 • • • . The empty word is denoted by ε. Given an infinite word α = a 1 a 2 • • • , we let inf(α) ⊆ A denote the set of letters in α which occur infinitely often. Let K be a set of finite words and let L be a set of infinite words. We set

KL = {uα | u ∈ K, α ∈ L}, K n = {u 1 u 2 • • • u n | u i ∈ K}, K + = n 1 K n and K * = K + ∪ {ε}. Moreover, if ε ∈ K we define the infinite iteration K ω = {u 1 u 2 • • • | u i ∈ K}. A natural extension to K ⊆ A * is K ω = (K \ {ε}) ω ∪ {ε}. Automata. A finite automaton is a 5-tuple A = (Q, A, δ, I, F )
where Q is a finite set of states and A is a finite alphabet. The transition relation δ is a subset of Q×A×Q and its elements are called transitions. The sets I and F are subsets of Q and are called initial states and final states, respectively.

A finite run of a word a 1 a 2 • • • a n on A is a sequence q 0 a 1 q 1 a 1 • • • q n-1 a n q n such that q 0 ∈ I and (q i , a i+1 , q i+1 ) ∈ δ for all i ∈ {0, . . . , n -1}. The run is said to start in q 0 and end in q n . The word a 1 a 2 • • • a n is the label of the run. A finite run is called accepting if it ends in a final state. A finite word u is said to be accepted by A if there exists an accepting finite run of u on A and the language accepted by A is the set of all finite words over A * accepted by A. It is denoted by L NFA (A).

Analogously, an infinite run of a word a 1 a 2 • • • on A is an infinite sequence q 0 a 1 q 1 a 1 • • • such that q 0 ∈ I and (q i , a i+1 , q i+1 ) ∈ δ for all i 0. It is called

accepting if inf(q 0 q 1 q 2 • • • ) ∩ F = ∅.
An infinite word α is said to be Büchiaccepted by A if there exists an accepting infinite run of α on A. The language Büchi-accepted by A is the set of all infinite words Büchi-accepted by A and it is denoted by L BA (A).

We use the term run for both finite and infinite runs if the reference is clear from the context. A language L ⊆ A * (resp. L ⊆ A ω ) is regular (resp. ω-regular) if it is accepted (resp. Büchi-accepted) by some finite automaton.

Finite semigroups.

A semigroup morphism is a mapping h : S → T between two (not necessarily finite) semigroups S and T such that h(s)h(t) = h(st) for all s, t ∈ S. Since we do not consider morphisms of other objects, we use the term morphism synonymously. A subsemigroup of a semigroup S is a subset that is closed under multiplication. We say that a semigroup T divides a semigroup S if there exists a surjective morphism from a subsemigroup of S onto T .

Green's relations are an important tool in the study of semigroups. For the remainder of this subsection, let S be a finite semigroup. We let S 1 denote the monoid that is obtained by adding a new neutral element 1 to S. For s, t ∈ S let s R t if there exist q, q ∈ S 1 such that sq = t and tq = s, s L t if there exist p, p ∈ S 1 such that ps = t and p t = s, s J t if there exist p, q, p , q ∈ S 1 such that psq = t and p tq = s, s H t if s R t and s L t.

These relations are equivalence relations. The equivalence classes of R (resp. L, J , H) are called R-classes (resp. L-classes, J -classes, H-classes). For s ∈ S, we denote the R-class (resp. L-class) of s by R s (resp. L s ) and we let S/R = {R s | s ∈ S} as well as S/L = {L s | s ∈ S}.

A semigroup is called J -trivial if each of its J -classes contains exactly one element. A semigroup is called simple if it consists of a single J -class. In a finite simple semigroup, the relations s R st L t hold for all s, t ∈ S. Moreover, each H-class forms a group and all such groups are isomorphic [START_REF] Pin | Varieties of Formal Languages[END_REF]. We will also utilize the following lemma: Lemma 1. Let S be a finite simple semigroup and let x, y, z ∈ S such that y R z. Then xy = xz implies y = z.

Proof. Suppose that xy = xz. Since S is simple, we have y L xy and thus, there exists an element p ∈ S 1 such that pxy = y. Since y R z, there exists an element q ∈ S 1 with yq = z. It follows that y = pxy = pxz = pxyq = yq = z.

Recognition by morphisms.

Let h : A + → S be a morphism to a finite semigroup S. A pair (s, e) of elements of S is a linked pair if se = s and e 2 = e. For s ∈ S, we set [s] h = h -1 (s) and if h is understood from the context, we may skip the reference to the morphism in the subscript. A language L ⊆ A + is recognized by a morphism h :

A + → S if L is a union of sets [s i ] with s i ∈ S. A language L ⊆ A ω is weakly recognized by a morphism h : A + → S if it is a union of sets [s i ][e i ]
ω where (s i , e i ) are linked pairs of S. A language L ⊆ A ω is strongly recognized by a morphism h :

A + → S if [s][t] ω ∩ L = ∅ implies [s][t] ω ⊆ L for all s, t ∈ S.
It is easy to see that strong recognition implies weak recognition, see e.g. [START_REF] Perrin | Infinite words[END_REF]Theorem 2.2]. Moreover, if a morphism strongly recognizes L, it also strongly recognizes its complement A ω \ L. By extension, we also say that a semigroup S recognizes (resp. weakly recognizes, strongly recognizes) a language L if there exists a morphism h : A + → L that recognizes (resp. weakly recognizes, strongly recognizes) L.

For a language L ⊆ A + ∪ A ω , we have u ≡ L v if and only if

(xuy)z ω ∈ L ⇔ (xvy)z ω ∈ L and z(xuy) ω ∈ L ⇔ z(xvy) ω ∈ L
for all finite words x, y, z ∈ A * . Keep in mind that ε ω = ε. The relation ≡ L was introduced by Arnold [START_REF] Arnold | A syntactic congruence for rational ω-languages[END_REF]; it is called the syntactic congruence of L. The congruence classes of ≡ L form the so-called syntactic semigroup A + /≡ L and the syntactic morphism h L :

A + → A + /≡ L is the natural quotient map. If L ⊆ A * (resp. L ⊆ A ω
) is regular (resp. ω-regular), the syntactic semigroup of L is finite and h L recognizes (resp. strongly recognizes) the language L; see [START_REF] Arnold | A syntactic congruence for rational ω-languages[END_REF][START_REF] Perrin | Infinite words[END_REF].

Lower Bound Techniques

Proving Lower Bounds for Weakly Recognizing Morphisms

We first consider the general problem of proving lower bounds for the size of weakly recognizing semigroups for a given language L. In the case of recognizing morphisms over finite words and in the case of strongly recognizing morphisms, this is easy since one only needs to compute the syntactic semigroup, which immediately yields a tight lower bound. On the contrary, weakly recognizing morphisms do not admit minimal objects. However, it turns out that one can still use a relaxed version of Arnold's syntactic congruence. We first prove a combinatorial lemma and then give the main result of this section.

Lemma 2. Let u, v ∈ A + and let (s, e) be a linked pair. Then uv ω is contained in [s][e]

ω if and only if there exists a factorization v = v 1 v 2 and powers k,

0 such that is odd, h(uv k v 1 ) = s and h(v 2 v v 1 ) = e. Proof. Let v = a 1 a 2 • • • a n with n 1 and a i ∈ A. If uv ω is contained in [s][e]
ω , there exists a factorization

uv ω = u v 1 v 2 • • • such that h(u ) = s and h(v i ) = e
for all i 1. Since u and v are finite words, there exist indices j > i 1, powers k, 1 and a position m ∈ {1, . . . , n} such that

u v 1 v 2 • • • v i-1 = uv k a 1 a 2 • • • a m and v i v i+1 • • • v j = a m+1 a m+2 • • • a n v a 1 a 2 • • • a m . We set v 1 = a 1 a 2 • • • a m and v 2 = a m+1 a m+2 • • • a n . Then v 1 v 2 = v, h(uv k v 1 ) = h(uv k a 1 a 2 • • • a m ) = h(u v 1 v 2 • • • v i-1 ) = se i-1 = s, h(v 2 v v 1 ) = h(a m+1 a m+2 • • • a n v a 1 a 2 • • • a m ) = h(v i v i+1 • • • v j ) = e j-i+1 = e.
If is even, we can replace by 2

+ 1 since h(v 2 v 2 +1 v 1 ) = h(v 2 v v 1 v 2 v v 1 ) = e 2 = e.
The converse implication is trivial.

Theorem 3. Let L ⊆ A ω be a language weakly recognized by some morphism h : A + → S and let u, v, z ∈ A + and x, y ∈ A * be words such that one of the following two properties holds:

1. xuyz ω ∈ L and xvyz ω ∈ L 2. x(uy) ω ∈ L and x(uyvy) ω ∈ L and x(vyuy) ω ∈ L. Then h(u) = h(v).
Proof. We consider finite words u, v ∈ A + such that h(u) = h(v) and show that in this case, neither of the properties can hold.

If the first property holds, there exists a linked pair (s, e) such that

xuyz ω ∈ [s][e]
ω ⊆ L. Thus, by Lemma 2, we have h(xuyz k z 1 ) = s and h(z 2 z z 1 ) = e for some factorization z = z 1 z 2 and powers k,

0. Now, since h(xvyz k z 1 ) = h(xuyz k z 1 ) = s, we obtain xvyz ω ∈ [s][e]
ω ⊆ L, a contradiction. If the second property holds, there exists a linked pair (s, e) of S such that

xw ω ∈ [s][e]
ω ⊆ L where w = uy. Thus, by Lemma 2, we have h(xw k w 1 ) = s and h(w 2 w w 1 ) = e for some factorization w = w 1 w 2 , some power k 0 and some odd power 0. Since is odd ( -1)/2 is an integer and we have h(w 2 (vyuy) ( -1)/2 vyw 1 ) = h(w 2 (uy) w 1 ) = e. Now, if k is odd as well, we obtain h(x(vyuy) (k-1)/2 vyw 1 ) = h(x(uy) k w 1 ) = s and therefore, x(vyuy) ω ∈ L.

Equivalently, if k is even, we have h(x(uyvy) k/2 w 1 ) = h(x(uy) k w 1 ) = s and hence, x(uyvy) ω ∈ L. Both cases contradict Property 2 above.

The next proposition is another simple, yet useful, tool for proving lower bounds. It allows to transfer bounds from the setting of finite words to infinite words. Proposition 4. Let A = (Q, A, δ, I, F ) and let a ∈ A be a letter such that for all q ∈ Q and q f ∈ F , we have (q, a, q f ) ∈ δ if and only if q = q f . Let K = L BA (A) and let L = L NFA (A). Then each semigroup weakly recognizing K has at least

|A + /≡ L | elements.
Proof. Let h : A + → S be a morphism weakly recognizing K and consider two words u, v ∈ A + such that u ≡ L v. Then, without loss of generality, there exist x, y ∈ A * such that xuy ∈ L and xvy ∈ L. This implies xuya ω ∈ K since (q f , a, q f ) ∈ δ for all q f ∈ F . Equivalently, because of (q, a, q f ) ∈ δ for all q ∈ Q \ F and q f ∈ F , we have xvya ω ∈ K. By Theorem 3, this yields h(u) = h(v).

The Full Automata Technique

The full automata technique is a useful tool for proving lower bounds for the conversion of automata to other objects. It was introduced by Yan [START_REF] Yan | Lower bounds for complementation of omega-automata via the full automata technique[END_REF] who attributes it to Sakoda and Sipser [START_REF] Sakoda | Nondeterminism and the size of two way finite automata[END_REF]. The technique works for both accepted and Büchi-accepted languages. However, we will prove the main result of this section only for the setting of finite words and use Proposition 4 to obtain analogous results for infinite words.

Let Q be a finite set and let I, F be subsets of Q. The full automaton F(Q, I, F ) is the finite automaton (Q, B, ∆, I, F ) defined by B = 2 Q 2 and by the transition relation Proof. We first define a morphism π :

∆ = {(p, T, q) ∈ Q × B × Q | (p, q) ∈ T }.
A + → B + by π(a) = {(p, q) | (p, a, q) ∈ δ}. Let K = L NFA (F(Q, I, F )) and let L = L NFA (A). It suffices to show that π(u) ≡ K π(v) implies u ≡ L v. Thus, consider u, v ∈ A + such that π(u) ≡ K π(v).
In particular, for all x, y ∈ A * , we have π(xuy) ∈ K if and only if π(xvy) ∈ K. By the definition of π, we have π(w) ∈ K if and only if w ∈ L for all w ∈ A + . Using the equivalence from above, this yields xuy ∈ L if and only if xvy ∈ L for all x, y ∈ A * , thereby proving that u ≡ L v.

From Automata to Weakly Recognizing Morphisms

The standard construction for converting a finite automaton A to a recognizing morphism is the so-called transition semigroup of A. For a given word u ∈ A + , it encodes for each pair (p, q) of states whether there is a run of u on A starting in p and ending in q. Thus, for a finite automaton with n states the transition semigroup has 2 n 2 elements. For details on the construction, we refer to [START_REF] Perrin | Infinite words[END_REF][START_REF] Pin | Varieties of Formal Languages[END_REF]. We show that this construction is optimal. Theorem 6. Let A be a finite automaton with n states. Then there exists a semigroup recognizing L NFA (A) (resp. weakly recognizing L BA (A)) which has at most 2 n 2 elements and this bound is tight.

Proof. Each language that is accepted (resp. Büchi-accepted) by A is recognized (resp. weakly recognized) by the transition semigroup of A which has size 2 n 2 .

To show that this is optimal, we consider the full automaton F(N, N, N ) = (N, B, ∆, N, N ) where N = {1, . . . , n} and let L = L NFA (F(N, N, N )). For two different letters X, Y ∈ B we may assume, without loss of generality, that there exist p, q ∈ N such that (p, q) ∈ X \ Y . With P = {(p, p)} and Q = {(q, q)}, we then have P XQ ∈ L and P Y Q ∈ L. Thus, X ≡ L Y . This shows that B + /≡ L has at least |B| = 2 n 2 elements.

Noting that the transitions labeled by the letter {(q, q) | q ∈ N } form selfloops at each state, the Büchi case immediately follows by Proposition 4.

The proof of the optimality result requires a large alphabet that grows superexponentially in the number of states of the automaton. A natural restriction is considering automata over fixed-size alphabets.

By a result of Chrobak [START_REF] Chrobak | Finite automata and unary languages[END_REF], the size of the syntactic semigroup of an unary language accepted by a finite automaton of size n is in 2 O( √ n log n) (note that since unary languages are commutative, the syntactic monoid is isomorphic to the minimal deterministic automaton). Over infinite words, the unary case is uninteresting since the only language over the alphabet A = {a} is {a ω }.

For binary alphabets, a lower bound can be obtained by combining the full automata technique with a result from the study of semigroups of binary relations [7, Proposition 6]. In order to keep the paper self-contained, we present a proof that is adapted to finite automata and does not require any knowledge of binary relations. Theorem 7. Let A = {a, b} and let n be an odd natural number. There exists a language L ⊆ A + (resp. L ⊆ A ω ) and a finite automaton with n states accepting (resp. Büchi-accepting) L, such that each semigroup recognizing (resp. weakly recognizing) L has at least 2 (n-1) 2 /4 elements.

Proof. We first analyze the case of finite words. Let m = (n -1)/2 and let M = {1, . . . , m}. We consider the automaton A depicted below and let L = L NFA (A). For 1 i, j m we first define p i,j = (m+j-i)m-i and q i,j = (m+i-j+2)m+i. Furthermore, we set u i,j = a pi,j ba qi,j . We claim that for each i, j there exists a path from state k to labeled by u i,j if and only if (k, ) = (i, j + m) or k = .

1 2 • • • m m+1 m+2 • • • n a a a
The two a-cycles have length m and m + 1, respectively. Since for each pair (i, j) we have p i,j + q i,j = 2m(m + 1) and since one can always stay in the same state when reading the letter b, there clearly exists a path from each state to itself labeled by u i,j . Now, fix some (i, j) and let (k, ) = (i, j + m). We have i + p i,j = (m+j -i)m which means that, when starting in state i, one can reach state m by reading a pi,j . Being in state m, one of the b-transitions leads to state m+1. From there on, we make a single step backwards whenever reading the factor a m . Thus, by reading the word a qi,j , we perform (m+i-j +2)-i = m-j +2 backward steps in total, finally reaching state n+1-(m-j+2) = 2m+2-(m-j+2) = m+j = . The converse direction of our claim follows immediately since the automaton is deterministic when restricted to a-transitions and since one can only reach states > m by using the transition (m, b, m + 1).

For X ⊆ M × M , we now define u X as the concatenation of all u i,j with (i, j) ∈ X, where the factors are ordered according to their indices (i, j). By the above argument, it is easy to see that there is a path from state i to j + m labeled by u X if and only if (i, j) ∈ X. Since there are 2 m 2 = 2 (n-1) 2 /4 subsets of the Cartesian product M × M , it remains to show that for different subsets X, Y ⊆ M ×M , we have u X ≡ L v Y . To this end, assume without loss of generality that (i, j) ∈ X \ Y . Then a i-1 u X a n-j ∈ L but a i-1 u Y a n-j ∈ L, as desired.

For the Büchi case note that for all i ∈ Q, we have (i, b, n) ∈ δ if and only if i = n. Therefore, by Proposition 4 and the arguments above, the smallest semigroup weakly recognizing L BA (A) has at least 2 (n-1) 2 /4 elements.

The construction above does not reach the 2 n 2 bound obtained when using a larger alphabet. However, this is not surprising, given the following result. Proposition 8. Let m ∈ N be a fixed integer and let A be an alphabet of size m. Then there exists an integer n m 1 such that for each finite automaton A over A with n n m states, the language L NFA (A) ⊆ A * (resp. L BA (A) ⊆ A ω ) is recognized (resp. weakly recognized) by a morphism onto a semigroup with less than 2 n 2 elements.

We do not give a full proof of the proposition here, but the claim essentially follows from a careful analysis of the subsemigroup of the transition semigroup generated by the transitions corresponding to the letters in A. Applying Devadze's Theorem [START_REF] Devadze | Generating sets of the semigroup of all binary relations in a finite set[END_REF][START_REF] Konieczny | A proof of Devadze's theorem on generators of the semigroup of boolean matrices[END_REF] to the matrix representation of this subsemigroup shows that it is proper, i.e., smaller than the full transition semigroup itself.

From Weakly Recognizing Morphisms to Automata

The well-known construction to convert weakly recognizing morphisms to finite automata with a Büchi-acceptance condition has quadratic blow-up [START_REF] Perrin | Infinite words[END_REF]. We show that this is optimal up to a constant factor. Proof. We first define a semigroup S = a i , a i b, ba i , ba i b | 1 i n ∪ {b, bb, 0} by the multiplication 0

• s = s • 0 = 0 for all s ∈ S and b a i b r • b m a j b s =          bb if i = j = 0 b a i+j b s if r = m = 0 and 1 i + j n 0 if r = m = 0 and i + j > n b a i b otherwise
where , m, r, s ∈ {0, 1} and i, j ∈ {0, . . . , n}. The morphism h :

A + → S defined by h(a) = a and h(b) = b now weakly recognizes L since L is the union of all sets [ba i b][ba i b] ω with 1 i n.
Now assume that we are given a finite automaton A = (Q, A, δ, I, F ) such that L BA (A) = L. For each i ∈ {1, . . . , n}, we consider the word α i = (ba i b) ω and let r i be an accepting run of α i . We first show that for i = j, we have inf(r i ) ∩ Q ∩ inf(r j ) = ∅, and then prove that |inf(r i ) ∩ Q| i for 1 i n. Together, this yields

|Q| n i=1 |inf(r i ) ∩ Q| n i=1 i = n(n + 1)/2.
Let i, j ∈ {1, . . . , n} such that i = j. We assume for the sake of contradiction that there exists a state q ∈ Q with q ∈ inf(r i ) and q ∈ inf(r j ). Let u ∈ ba i bA * be a prefix of α i such that r i visits q after reading u. Let v ∈ A * be a factor of α j such that there exists a finite run labeled by v, which starts and ends in q, visits at least one final state and such that v ω = (ba j b)

ω or v ω = a k b(ba j b) ω
for some k ∈ {0, . . . , j}. Obviously, we then have

uv ω ∈ L BA (A) but uv ω ∈ L, a contradiction.
For the second part of the proof, assume again for the sake of contradiction that |inf(r i ) ∩ Q| < i for some accepting run r i of α i . Then inside each ba i bfactor, a state is visited twice and we can apply the standard pumping argument to show that a word in A ω \ L BA (A) has an accepting run as well.

Complementation

To date, the best construction for complementing weakly recognizing morphisms is the so-called strong expansion [START_REF] Perrin | Infinite words[END_REF]. Given a morphism h : A + → S, the strong expansion of h is a morphism g : A + → T which strongly recognizes all languages weakly recognized by h. If S has n elements, the size of T is 2 n 2 . The purpose of this section is to give a lower bound for complementation. At the same time, the established bound also serves as a lower bound for the conversion of weak recognition to strong recognition since each morphism strongly recognizing a language also strongly recognizes its complement.

Complementing weakly recognizing morphisms is easy in the case of J -trivial semigroups since each language weakly recognized by a J -trivial semigroup S is already strongly recognized by S, i.e., there is no need the compute the strong expansion if the J -classes of the input are trivial already. In order to establish a lower bound, we thus consider the class of simple semigroups, which is dual to J -trivial semigroups in the sense that simple semigroups consist of a single J -class only.

Proposition 10. Let n 1 be an arbitrary integer and let

A = {a 1 , a 2 , . . . , a n }. The language L = n i=1 (a i A * )
ω is weakly recognized by a simple semigroup with n elements and every semigroup weakly recognizing A ω \ L has at least n2 n-1 elements. Rather surprisingly, the established lower bound turns out to be asymptotically tight in the case of simple semigroups. More generally, for simple semigroups, the construction of the strong expansion can be improved such that only n2 n elements are needed. This will be proved in the remainder of this section.

Proof. The alphabet

We start with a morphism h : A + → S onto a simple semigroup with n = |S| elements. Since S is simple, there exists a surjective mapping γ : S → G onto a finite group G that becomes a bijection when restricted to a single H-class. Therefore, the mapping π : (S/R) × G × (S/L) → S with π -1 (s) = (R s , γ(s), L s ) for all s ∈ S is well-defined and bijective. Moreover, for s, t ∈ S, we write R t • s to denote the element π(R t , γ(s), L s ).

Let T = {(s, X) | s ∈ S, X ⊆ S} and let g : A + → T be defined by

g(u) = (h(u), R h(q) • h(p) | p, q ∈ A + , pq = u )
for all u ∈ A + . The set T can be extended to a semigroup by defining an associative multiplication (s, X)

• (t, Y ) = (st, X ∪ {R t • s} ∪ Ŷ )
where Ŷ denotes the set {π(R y , γ(s(R t • y)), L y ) | y ∈ Y }. Under this extension, the mapping g becomes a morphism.

The following three technical lemmas capture important properties of the construction and are needed for the main proof. Lemma 11. Let s, t ∈ S. Then R t • s is the unique element x such that x R t, x L s and γ(x) = γ(s) or, equivalently, the unique element x such that x H ts and γ(x) = γ(s).

Proof. Let x = R t • s. We have (R x , γ(x), L x ) = π -1 (x) = π -1 (R t • s) = (R t , γ(s), L s ).
Together with the fact that π is bijective, this establishes the first claim. For the second claim, note that since S is simple, x R t is equivalent to x R ts and x L s is equivalent to x L ts. Lemma 12. Let u ∈ A + with g(u) = (s, X) and let x ∈ S. Then x ∈ X ∪ {s} if and only if there exists a factorization u = pq with p ∈ A + and q ∈ A * such that x H h(qp) and γ(x) = γ(h(p)).

Proof. Obviously, we have x = s if and only if there exists a factorization u = pq with p = u and q = ε satisfying the properties described above. Thus, it suffices to consider factorizations where p, q ∈ A + . By Lemma 11, such a factorization exists if and only if x = R h(q) • h(p) which is, in turn, equivalent to x ∈ X by the definition of g. Lemma 13. Let (t, f ) be a linked pair of S, let (s, X), (e, Y ) be a linked pair of T and let α ∈

[(s, X)] g [(e, Y )] ω g . Then α ∈ [t] h [f ] ω h if and only if tq = s, pq = e, qp = f , R q • t ∈ X and R q • p ∈ Y for some p, q ∈ S.
Proof. For the direction from left to right, let α

= uv 1 v 1 v 2 v 2 • • • such that g(u) = (s, X), g(v i v i ) = (e, Y ), h(uv 1 ) = t and h(v i v i+1 ) = f for all i
1. Furthermore, we assume without loss of generality that v i , v i = ε for all i 1 and that h(v 1 ) = h(v 2 ). We set p = h(v 1 ) = h(v 2 ) and q = h(v 1 ). Now, tq = h(uv

1 v 1 ) = se = s, pq = h(v 1 v 1 ) = e and qp = h(v 1 v 2 ) = f . Moreover, by the definition of g, we have R q •t = R h(v 1 ) •h(uv 1 ) ∈ X and R q •p = R h(v 1 ) •h(v 1 ) ∈ Y .
For the converse implication, note that by Lemma 12, there exists a factorization

α = uv 1 v 1 v 2 v 2 • • • such that h(u) = s, h(v i v i ) = e, R h(v 1 ) • h(uv 1 ) = R q • t and R h(v i ) • h(v i ) = R q • p for all i 1. Since S is simple, h(v i ) R h(v i v i ) = e R p and h(v i ) L (R h(v i ) • h(v i )) = (R q • p) L p for all i 1. Furthermore, γ(h(v i )) = γ(R h(v i ) • h(v i )) = γ(R q • p) = γ(p).
Together, this yields h(v i ) = p by Lemma 11. Similarly, we have h(v i ) R (R h(v i ) • h(v i )) = (R q • p) R q and thus, ph(v i ) = h(v i v i ) = pq implies h(v i ) = q for all i 1 by Lemma 1. This shows that h(uv 1 ) = sp = tqp = tf = t and h(v i v i+1 ) = qp = f . We conclude that α ∈ [t][f ] ω .

Theorem 14. Let h : A + → S be a morphism onto a simple semigroup of size n = |S| that weakly recognizes a language L ⊆ A ω . Then there exists a morphism g : A + → T to a semigroup of size |T | = n2 n that strongly recognizes L.

Proof. The construction we use is the one described in the introduction of this section. Consider a linked pair ((s, X), (e, Y )) of T as well as two infinite words α, β ∈ [(s, X)][(e, Y )] ω . If α ∈ L, there exists a linked pair (t, f ) of S such that α ∈ [t][f ] ω ⊆ L. Lemma 13 immediately yields β ∈ [t][f ] ω ⊆ L, thereby showing that g strongly recognizes L.

Discussion and Open Problems

We presented lower bound techniques and gave tight bounds for the conversion between finite automata and weakly recognizing morphisms. One can use techniques similar to those described in Section 4 to obtain a 3 n 2 lower bound for the conversion of finite automata with transition-based Büchi acceptance to strongly recognizing morphisms. However, with the usual state-based Büchi acceptance criterion, the analysis becomes much more involved and it is not clear whether the 3 n 2 upper bound can be reached. Analogously, there is no straightforward adaptation of the conversion of weakly recognizing morphisms into Büchi automata in Section 5 to strongly recognizing morphisms. It would be interesting to see whether the quadratic lower bound also holds in this setting.

Another open problem is to close the remaining gaps between the upper and the lower bounds. This is particularly true for the complexity of complementation and the conversion of weakly recognizing morphisms to strong recognition. We showed that there is an exponential lower bound and gave an asymptotically optimal construction for simple semigroups which was a first candidate for semigroups that are hard to complement. It is easy to adapt this construction to families of semigroups where the size of each J -class is bounded by a constant. However, for the general case, the gap between n2 n-1 and 2 n 2 remains.

Beyond that, another direction for future research is to investigate whether any of the bounds can be improved by considering the size of the accepting set, i.e., the number of linked pairs used to describe a language.

Theorem 5 .

 5 Let A = (Q, A, δ, I, F ) be a finite automaton and let F(Q, I, F ) = (Q, B, ∆, I, F ) be the corresponding full automaton. Then the syntactic semigroup of L NFA (A) divides the syntactic semigroup of L NFA (F(Q, I, F )).

Theorem 9 .

 9 Let A = {a, b}, let n 3, and let L = n i=1 (ba i bA * ) ω . Then there exists a semigroup with 4n + 3 elements that weakly recognizes L and every finite automaton Büchi-accepting L has at least n(n + 1)/2 states.

  A can be extended to a semigroup by defining an associative operation a • b = a for all a, b ∈ A. Now, the morphism h : A + → (A, •) given by h(a) = a for all a ∈ A weakly recognizes L. The semigroup (A, •) contains |A| = n elements and it is simple because we have a L b for all a, b ∈ A. Now, let h : A + → S be a morphism weakly recognizing A ω \L. For a letter b ∈ A and a subset B ⊆ A \ {b}, let u b,B be the uniquely defined word ba i1 a i2 • • • a i such that i 1 < i 2 < • • • < i and {a i1 , a i2 , . . . , a i } = B. Consider two letters b, c ∈ A and subsets B ⊆ A \ {b}, C ⊆ A \ {c}. If b = c, we have u b,B c ω ∈ L and u c,C c ω ∈ L. If B = C we may assume, without loss of generality, that there exists a letter a ∈ B \ C. In this case, we have au c,C ω ∈ L but a(u b,B u c,C ) ω ∈ L and a(u c,C u b,B ) ω ∈ L. By Theorem 3, this suffices to conclude that h(u b,B ) = h(u c,C ) whenever b = c or B = C and therefore, S contains at least |A| 2 |A|-1 = n2 n-1 elements.

Lower bound Upper bound

	BA to weak recognition	2 n 2	[new]	2 n 2	[9]
	BA to weak recognition, binary alphabet	2 (n-1) 2 /4 [new]	2 n 2	[9]
	Weak recognition to BA	(n -3)(n + 1)/32 [new]	n(n + 1) [9]
	Weak recognition to strong recognition	n2 n-1 [new]	2 n 2	[10]
	Complementation of weak recognition	n2 n-1 [new]	2 n 2	[10]
	Complementation for simple semigroups	n2 n-1 [new]	n2 n [new]

Table 1 .

 1 Bounds for the descriptional complexity of various operations.

Acknowledgments. We thank the anonymous referees for several useful suggestions which helped to improve the presentation of this paper.