BRICS RS-02-47 Z. Ésik: Extended Temporal Logic on Finite Words BRICS

Basic Research in Computer Science

Extended Temporal Logic on Finite Words and Wreath Product of Monoids with Distinguished Generators

Zoltán Ésik

BRICS Report Series RS-02-47 ISSN 0909-0878 December 2002 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2002, Zoltán Ésik.

BRICS, Department of Computer Science University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/02/47/

Extended Temporal Logic on Finite Words and Wreath Product of Monoids with Distinguished

Generators

Z. Ésik^{⋆}

Dept. of Computer Science, University of Szeged, P.O.B. 652, 6701 Szeged, Hungary

Abstract. We associate a modal operator with each language belonging to a given class of regular languages and use the (reverse) wreath product of monoids with distinguished generators to characterize the expressive power of the resulting logic.

1 Introduction

The wreath product and its variants have been very useful and powerful tools in the characterization of the expressive power of several logical systems over finite and infinite words, including first-order logic and its extension with modular counting, cf. Straubing [11] and Straubing, Therien, Thomas [12], temporal logic and the until hierarchy, Cohen, Pin, Perrin [3] and Therien, Thomas [13], and modular temporal logic, Bazirambawo, McKenzie, Therien [2]. In this paper, we associate a modal operator with each language in a given subclass of regular languages, and use the reverse wreath product (of monoids with distinguished generators) to provide an algebraic characterization of the expressive power of (future) temporal logic on finite words endowed with these modal operators. Our logic is closely related to that proposed in Wolper [14], and our methods are related to those of Cohen, Pin, Perrin [3] and Bazirambawo, McKenzie, Therien [2] and Ésik, Larsen [7]. Moreover, our methods and results extend to ω-words, (countable) ordinal words and, more generally, to all discrete words. These extensions will be treated in subsequent papers.

Some notation An alphabet is a finite nonempty set. We assume that each alphabet is equipped with a fixed linear order <. For an alphabet Σ, we denote by Σ^{∗} the free monoid of all finite words over Σ including the empty word ϵ. The length of a word u is denoted |u|. The notation u = u_{1} ⋯ u_{n} for a word u ∈ Σ^{∗} means that u is a word of length n whose letters are u_{1}, …, u_{n}. A subset of Σ^{∗} is called a language over Σ. The boolean and regular operations on languages, and regular languages are defined as usual. When L ⊆ Σ^{∗} and u ∈ Σ^{∗}, the left quotient u^{−1}L and right quotient Σu^{−1} of L with respect to u are respectively given by

u^{−1}L = {v : uv ∈ L}
Lu^{−1} = {v : vu ∈ L}.

⋆ Supported in part by BRICS, a grant from the National Foundation of Hungary for Scientific Research, and by the Japan Society for the Promotion of Science.

A class of (regular) languages L consists of a set of (regular) languages for each alphabet Σ. If n is a nonnegative integer, we let [n] denote the set {1, …, n}. Thus, [0] is another name for the empty set.

2 Extended Temporal Logic

Syntax. For an alphabet Σ, the set of formulas over Σ is the least set containing the letters p_{σ}, for all σ ∈ Σ, closed with respect to the boolean connectives ∨ (disjunction) and ¬ (negation), as well as the following construct. Suppose that L ⊆ Δ^{∗} and that for each δ ∈ Δ, φ_{δ} is a formula over Σ. Then

L(δ ↦ φ_{δ})_{δ∈Δ}  (1)

is a formula over Σ. The notion of subformula of a formula is defined as usual.

Semantics. Suppose that φ is a formula over Σ and u ∈ Σ^{∗}. We say that u satisfies φ, in notation u ⊧ φ, if

– φ = p_{σ}, for some σ ∈ Σ, and u is a nonempty word whose first letter is σ, i.e., u = σu′ for some u′ ∈ Σ^{∗}, or

– φ = φ′ ∨ φ′′ and u ⊧ φ′ or u ⊧ φ′′, or

– φ = ¬φ′ and it is not the case that u ⊧ φ′, or

– φ = L(δ ↦ φ_{δ})_{δ∈Δ}, u = u_{1} ⋯ u_{n}, where each u_{i} is a letter, and the characteristic word δ_{1} ⋯ δ_{n} belongs to L, where for each i ∈ [n], δ_{i} is the first letter of Δ with respect to the linear order on Δ with u_{i} ⋯ u_{n} ⊧ φ_{δ_{i}}, if such a letter exists, and δ_{i} is the last letter of Δ, otherwise.

For any formula φ of over Σ, we let L_{φ} denote the language defined by φ:

L_{φ} = {u ∈ Σ^{∗} : u ⊧ φ}.

We say that formulas φ and ψ over Σ are equivalent if L_{φ} = L_{ψ}. Throughout the paper we will use the boolean connective ∧ (conjunction) as an abbreviation. Moreover, for any alphabet Σ, we define tt = p_{σ} ∨ ¬p_{σ} and ff = ¬tt, where σ is a letter in Σ.

We will consider subsets of formulas associated with a class L of (regular) languages. We let FTL(L) denote the collection of formulas all of whose subformulas of the form (1) above satisfy that L belongs to L. We define FTL(L) to be the class of all languages definable by formulas in FTL(L). It is clear that for each formula L(δ ↦ φ_{δ})_{δ∈Δ} in FTL(L) over an alphabet Σ there is an equivalent formula L(δ ↦ φ′_{δ})_{δ∈Δ} in FTL(L) such that the subformulas φ′_{δ} are pairwise inconsistent: There exists no u ∈ Σ^{∗} and distinct letters δ, δ′ ∈ Δ such that u ⊧ φ′_{δ} ∧ φ′_{δ′}. Indeed, when the given linear order on Δ is δ_{1} < ⋯ < δ_{k}, then we define

φ′_{δ_{i}} = φ_{δ_{i}} ∧ ⋀_{j<i} ¬φ_{δ_{j}},

for all i ∈ [k]. Alternatively, we may define φ′_{δ_{i}} for all i < k as above, and

φ′_{δ_{k}} = ⋀_{j<k} ¬φ_{δ_{j}}.

Thus, the modal formulas in FTL(L) over Σ associated with a language L ⊆ Δ^{∗} in L may equivalently be written as L(δ ↦ φ_{δ})_{δ∈Δ}, where the φ_{δ} are pairwise inconsistent and ⋁_{δ∈Δ} φ_{δ} is equivalent to tt, so that each word in Σ^{∗} satisfies exactly one φ_{δ}. Below we will call such families φ_{δ}, δ ∈ Δ deterministic. Moreover, we will sometimes write modal formulas over Σ as L(δ ↦ φ_{δ})_{δ∈Δ}, where φ_{δ}, δ ∈ Δ is a deterministic family of formulas over Σ. When φ_{δ}, δ ∈ Δ is a deterministic family, we have

u ⊧ L(δ ↦ φ_{δ})_{δ∈Δ} ⇔ ∃δ_{1} ⋯ δ_{n} ∈ L ∀i ∈ [n] u_{i} ⋯ u_{n} ⊧ φ_{δ_{i}},

for all u = u_{1} ⋯ u_{n} ∈ Σ^{∗}. We call a formula φ deterministic if for every subformula of φ of the form L(δ ↦ φ_{δ})_{δ∈Δ}, the family φ_{δ}, δ ∈ Δ is deterministic. As shown above, for each φ ∈ FTL(L) there is a deterministic formula in FTL(L) which is equivalent to φ.

We end this section with the definition of formula substitution. Suppose that φ is a formula over an alphabet Σ, and suppose that for each σ ∈ Σ we are given a formula ψ_{σ} over Σ′. Then the formula over Σ′,

τ = φ[p_{σ} ↦ ψ_{σ}],

is obtained from φ by replacing, for each letter σ ∈ Σ, each occurrence of the symbol p_{σ} by the formula ψ_{σ}. Formally, we define

– τ = ψ_{σ} if φ = p_{σ},

– τ = φ_{1}[p_{σ} ↦ ψ_{σ}] ∨ φ_{2}[p_{σ} ↦ ψ_{σ}] if φ = φ_{1} ∨ φ_{2},

– τ = ¬(φ_{1}[p_{σ} ↦ ψ_{σ}]) if φ = ¬φ_{1},

– τ = L(δ ↦ φ_{δ}[p_{σ} ↦ ψ_{σ}])_{δ∈Δ} if φ = L(δ ↦ φ_{δ})_{δ∈Δ}. Note that when φ and ψ_{σ} are in FTL(L), for all σ ∈ Σ, then φ[p_{σ} ↦ ψ_{σ}] belongs to FTL(L).

3 Some Elementary Properties

In this section, we establish some elementary properties of the classes FTL(L), where L denotes a class of languages. We also study conditions on L and L′ under which FTL(L) = FTL(L′).

Suppose that Δ and Δ′ are alphabets. A literal homomorphism Δ^{∗} → Δ^{′∗} is a homomorphism h : Δ^{∗} → Δ^{′∗} such that h(Δ) ⊆ Δ′. Note that a homomorphism h : Δ^{∗} → Δ^{′∗} is a literal homomorphism iff it is length preserving, i.e., when |h(u)| = |u|, for all u ∈ Σ^{∗}.

Proposition 1. For each L, the class of languages FTL(L) contains L and is closed with respect to the boolean operations and inverse literal homomorphisms.

Proof. It is obvious that FTL(L) is closed under the boolean operations. Moreover, each language L ⊆ Σ^{∗} in L is definable by the formula L(σ ↦ p_{σ})_{σ∈Σ} in FTL(L). Assume now that h : Σ^{′∗} → Σ^{∗} is a literal homomorphism. We argue by induction on the structure of the formula φ over Σ in FTL(L) to show that h^{−1}(L_{φ}) is definable by some formula ψ in FTL(L). When φ = p_{σ}, for some letter σ, then we define ψ = ⋁_{h(σ′)=σ} p_{σ′}. It is clear that L_{ψ} = h^{−1}(L_{φ}). Suppose now that φ = φ_{1} ∨ φ_{2} and that L_{ψ_{i}} = h^{−1}(L_{φ_{i}}), i = 1, 2. Then we define ψ = ψ_{1} ∨ ψ_{2}. When φ = ¬φ_{1} and L_{ψ_{1}} = h^{−1}(L_{φ_{1}}), then let ψ = ¬ψ_{1}. In either case, we have L_{ψ} = h^{−1}(L_{φ}). Finally, assume that ψ = L(δ ↦ φ_{δ})_{δ∈Δ}, and that for each δ there is a formula ψ_{δ} in FTL(L) with L_{ψ_{δ}} = h^{−1}(L_{φ_{δ}}). Then define ψ = L(δ ↦ ψ_{δ})_{δ∈Δ}. Let u = u_{1} ⋯ u_{n} ∈ Σ^{′∗}. Since for all δ ∈ Δ and i ∈ [n],

u_{i} ⋯ u_{n} ⊧ ψ_{δ} ⇔ h(u_{i} ⋯ u_{n}) ⊧ φ_{δ},

the characteristic word determined by u and the formulas ψ_{δ} is the same as that determined by h(u) and the formulas φ_{δ}. It follows that u ⊧ ψ iff h(u) ⊧ φ.

□

Next we show that FTL is a closure operator.

Proposition 2. For any class L of languages, FTL(FTL(L)) = FTL(L).

Proof. The inclusion from right to left follows from Proposition 1. To prove that FTL(FTL(L)) ⊆ FTL(L), we argue by induction on the structure of a formula φ over Δ in FTL(L) to show that for every deterministic family φ_{δ}, δ ∈ Δ of formulas in FTL(L) over an alphabet A, the formula L_{φ}(δ ↦ φ_{δ})_{δ∈Δ} is expressible in FTL(L), i.e., there exists a formula in FTL(L) which is equivalent to it. Assume first that φ = p_{δ_{0}}, for some δ_{0} ∈ Δ. Then L_{φ} = δ_{0}Δ^{∗}. It is clear that a word u ∈ A^{∗} satisfies L_{φ}(δ ↦ φ_{δ})_{δ∈Δ} iff |u| > 0 and u satisfies φ_{δ_{0}}, so that L_{φ}(δ ↦ φ_{δ})_{δ∈Δ} is equivalent to φ_{δ_{0}} ∧ ⋁_{a∈A} p_{a}. In the induction step, assume first that φ = φ_{1} ∨ φ_{2}. Then L_{φ} = L_{φ_{1}} ∪ L_{φ_{2}} and thus L_{φ}(δ ↦ φ_{δ})_{δ∈Δ} is equivalent to L_{φ_{1}}(δ ↦ φ_{δ})_{δ∈Δ} ∨ L_{φ_{2}}(δ ↦ φ_{δ})_{δ∈Δ}. By induction, there exist ψ_{1} and ψ_{2} in FTL(L) such that L_{φ_{i}}(δ ↦ φ_{δ})_{δ∈Δ} is equivalent to ψ_{i}, i = 1, 2. It follows that L_{φ}(δ ↦ φ_{δ})_{δ∈Δ} is equivalent to ψ_{1} ∨ ψ_{2} which is in FTL(L). Suppose next that φ = ¬φ_{1}, so that L_{φ} = \overline{L_{φ_{1}}}. Then we have L_{φ}(δ ↦ φ_{δ})_{δ∈Δ} is equivalent to ¬(L_{φ_{1}}(δ ↦ φ_{δ})_{δ∈Δ}). It follows from the induction hypothesis that L_{φ}(δ ↦ φ_{δ})_{δ∈Δ} is equivalent to a formula in FTL(L). Assume finally that φ = K(σ ↦ τ_{σ})_{σ∈Σ}, where the family τ_{σ}, σ ∈ Σ is deterministic. Then for any word u_{1} ⋯ u_{n} ∈ A^{∗} and for any i ∈ [n], let φ_{δ_{i}} denote the unique formula φ_{δ} with u_{i} ⋯ u_{n} ⊧ φ_{δ}. Moreover, for each i ∈ [n], let τ_{σ_{i}} denote the unique formula τ_{σ} with δ_{i} ⋯ δ_{n} ⊧ τ_{σ}. Then we have:

u_{1} ⋯ u_{n} ⊧ L_{φ}(δ ↦ φ_{δ})_{δ∈Δ} ⇔ δ_{1} ⋯ δ_{n} ∈ L_{φ}
⇔ δ_{1} ⋯ δ_{n} ⊧ φ
⇔ σ_{1} ⋯ σ_{n} ∈ K.

But for every i ∈ [n],

u_{i} ⋯ u_{n} ⊧ L_{τ_{σ_{i}}} (δ ↦ φ_{δ})_{δ∈Δ},

since for every j ≥ i, u_{j} ⋯ u_{n} ⊧ φ_{δ_{j}} and since δ_{i} ⋯ δ_{n} ∈ L_{τ_{σ_{i}}}. Moreover, the formulas L_{τ_{σ}}(δ ↦ φ_{δ})_{δ∈Δ}, σ ∈ Σ form a deterministic family. Thus,

u_{1} ⋯ u_{n} ⊧ K(σ ↦ L_{τ_{σ}}(δ ↦ φ_{δ})_{δ∈Δ})_{σ∈Σ} ⇔ σ_{1} ⋯ σ_{n} ∈ K.

We have thus shown that φ is equivalent to K(σ ↦ L_{τ_{σ}}(δ ↦ φ_{δ})_{δ∈Δ})_{σ∈Σ}. By the induction hypothesis, for each σ there is a formula ψ_{σ} in FTL(L) which is equivalent to L_{τ_{σ}}(δ ↦ φ_{δ})_{δ∈Δ}. Thus, φ is equivalent to K(σ ↦ ψ_{σ})_{σ∈Σ}. □

Since FTL(L_{1}) ⊆ FTL(L_{2}) whenever L_{1} ⊆ L_{2} and since L ⊆ FTL(L), for all L, we have:

Corollary 1. FTL is a closure operator.

Proposition 3. Suppose that for each formula L(δ ↦ φ_{δ})_{δ∈Δ} in FTL(L), over any alphabet Σ, and for each w ∈ Δ^{∗} there is a formula in FTL(L) which is equivalent to (w^{−1}L)(δ ↦ φ_{δ})_{δ∈Δ}. Then FTL(L) is closed with respect to left quotients.

Proof. Suppose that φ is a formula over Σ in FTL(L) and σ is a letter in Σ. We show that σ^{−1}L_{φ} belongs to FTL(L). The generalization to quotients w^{−1}L_{φ}, where w is a word, is left to the reader. When φ is p_{σ}, then σ^{−1}L_{φ} is Σ^{∗}, which is definable by the formula tt. When φ is p_{σ′}, where σ′ ≠ σ, then σ^{−1}L_{φ} is ∅, which is definable by the formula ff. We continue by induction on the structure of φ. Suppose that φ = φ_{1} ∨ φ_{2} or φ = ¬φ_{1}, and assume that σ^{−1}L_{φ_{i}} is defined by φ̃_{i} in FTL(L), i = 1, 2. Then σ^{−1}L_{φ} is defined by φ̃_{1} ∨ φ̃_{2} or ¬φ̃_{1}, respectively. Assume finally that φ is L(δ ↦ φ_{δ})_{δ∈Δ}, where φ_{δ}, δ ∈ Δ is a deterministic family, and that for each δ, σ^{−1}L_{φ_{δ}} is defined by φ̃_{δ} in FTL(L). Note that φ̃_{δ}, δ ∈ Δ is also a deterministic family. By assumption, for each δ_{0} in Δ there is a formula τ_{δ_{0}} in FTL(L) such that for all words u ∈ Σ^{∗},

u ⊧ τ_{δ_{0}} ⇔ u ⊧ (δ_{0}^{−1}L)(δ ↦ φ_{δ})_{δ∈Δ}.

Then let

φ̃ = ⋁_{δ_{0}∈Δ}(φ̃_{δ_{0}} ∧ τ_{δ_{0}}).

We have, for all u = u_{1} ⋯ u_{n} ∈ Σ^{∗},

u ⊧ φ̃ ⇔ ∃δ_{0} u ⊧ φ̃_{δ_{0}} ∧ u ⊧ τ_{δ_{0}}
⇔ ∃δ_{0} σu ⊧ φ_{δ_{0}} ∧ u ⊧ (δ_{0}^{−1}L)(δ ↦ φ_{δ})_{δ∈Δ}
⇔ ∃δ_{0} σu ⊧ φ_{δ_{0}} ∧ ∃δ_{1} ⋯ δ_{n} ∈ δ_{0}^{−1}L ∀i ∈ [n] u_{i} ⋯ u_{n} ⊧ φ_{δ_{i}}
⇔ ∃δ_{0} ⋯ δ_{n} ∈ L σu ⊧ φ_{δ_{0}} ∧ ∀i ∈ [n] u_{i} ⋯ u_{n} ⊧ φ_{δ_{i}}
⇔ σu ⊧ L(δ ↦ φ_{δ})_{δ∈Δ}
⇔ σu ⊧ φ.

This concludes the proof of Proposition 3. □

Proposition 4. Suppose that for each formula L(δ ↦ φ_{δ})_{δ∈Δ} in FTL(L), over any alphabet Σ, and for each w ∈ Δ^{∗} there is a formula in FTL(L) which is equivalent to (Lw^{−1})(δ ↦ φ_{δ})_{δ∈Δ}. Then FTL(L) is closed with respect to right quotients.

Proof. Suppose that φ is a formula over Σ in FTL(L), and let σ be a letter in Σ. We only show that L_{φ}σ^{−1} belongs to FTL(L). When φ is p_{σ}, then L_{φ}σ^{−1} is σΣ^{∗} ∪ {ϵ}, which is defined by the formula p_{σ} ∨ ⋀_{σ′∈Σ} ¬p_{σ′}. When φ is p_{σ′}, where σ′ ≠ σ, then σ^{−1}L_{φ} is σ′Σ^{∗}, which is defined by the formula p_{σ′}. We proceed by induction on the structure of φ. The cases when φ = φ_{1} ∨ φ_{2} or φ = ¬φ_{1} can be handled as above. Assume finally that φ is L(δ ↦ φ_{δ})_{δ∈Δ}, and that for each δ, L_{φ_{δ}}σ^{−1} is defined by φ̃_{δ} in FTL(L). By assumption, for each δ_{0} in Δ there is a formula τ_{δ_{0}} such that for all words u ∈ Σ^{∗},

u ⊧ τ_{δ_{0}} ⇔ u ⊧ (Lδ_{0}^{−1})(δ ↦ φ̃_{δ})_{δ∈Δ}.

We define

φ̃ = ⋁_{σ⊧φ_{δ_{0}}} τ_{δ_{0}}.

Then, u ∈ L_{φ}σ^{−1} iff uσ ∈ L_{φ} iff the characteristic word determined by uσ and the formulas φ_{δ} belongs to L iff there exists some δ_{0} such that σ ⊧ φ_{δ_{0}} and the characteristic word determined by u and the formulas φ̃_{δ} belongs to Lδ_{0}^{−1} iff u ⊧ φ̃. □

Corollary 2. 1. For any class L of languages, FTL(L) = FTL(L′), where L′ is the least class containing L closed with respect to the boolean operations and inverse literal morphisms.

2. For any class L of languages closed with respect to quotients, or such that the modal operators associated with the quotients of the languages in L are expressible in FTL(L) as in Propositions 3 and 4, FTL(L) = FTL(L′), where L′ is the least class containing L closed with respect to the boolean operations, quotients, and inverse literal morphisms.

4 Monoids with Distinguished Generators

Suppose that M is a monoid and A is a nonempty set of distinguished generators for M. Then we call the pair (M, A) a monoid with distinguished generators, or mg-pair, for short. When M is finite, the mg-pair (M, A) is also called finite.

Suppose that (M, A) and (N, B) are mg-pairs. A homomorphism (M, A) → (N, B) is a monoid homomorphism h : M → N such that h(A) ⊆ B. It is clear that mg-pairs equipped with these homomorphisms form a category. We call (M, A) a sub mg-pair of (N, B) if M is a submonoid of N and A is a subset of B. Moreover, we call (M, A) a quotient of (N, B) if there is a surjective homomorphism (N, B) → (M, A), i.e., a homomorphism of mg-pairs which maps B onto A. We say that (M, A) divides, or is a divisor of (N, B), denoted (M, A) < (N, B), if (M, A) is a quotient of a sub mg-pair of (N, B). We identify any monoid M with the mg-pair (M, M).

Example 1. For every alphabet Σ, (Σ^{∗}, Σ) is an mg-pair with the following property: For every mg-pair (M, A) and function h : Σ → A there is a unique homomorphism h^{♯} : (Σ^{∗}, Σ) → (M, A) extending h. We call such mg-pairs free.

Let L ⊆ Σ^{∗}. Recall that the syntactic monoid of L is the quotient Σ^{∗}/ ∼_{L} of Σ^{∗} with respect to the syntactic congruence ∼_{L} defined on Σ^{∗} by

u ∼_{L} v ⇔ ∀x, y ∈ Σ^{∗} xuy ∈ L ⇔ xvy ∈ L.

The syntactic mg-pair of L is Synt(L) = (Σ^{∗}/ ∼_{L}, Σ/ ∼_{L}).

We call a language L ⊆ Σ^{∗} recognizable by an mg-pair (M, A) if there is a homomorphism h : (Σ^{∗}, Σ) → (M, A) with L = h^{−1}(h(L)). It follows by standard arguments that a language L is recognizable by an mg-pair (M, A) iff Synt(L) < (M, A). Moreover, a language is recognizable by a finite mg-pair iff it is regular.

For the definition of the (reverse) semidirect product of monoids we refer to Eilenberg [5], and for the extension of these notions to mg-pairs to Ésik and Larsen [7]. When (S, A) and (T, B) are mg-pairs equipped with a (monoidal) right action of T on S,

S × T → S
(s, t) ↦ st

such that st ∈ A whenever s ∈ A, we let (S, A) ⋆_{r} (T, B) denote the reverse semidirect product of (S, A) and (T, B) determined by the right action. This is the mg-pair (R, A × B), where R is the submonoid of the ordinary reverse semidirect product S ⋆_{r} T of the monoids S and T determined by the action. When the right action is trivial, i.e., st = s for all s ∈ S and t ∈ T, the reverse semidirect product (S, A) ⋆_{r} (T, B) becomes the direct product (S, A) × (T, B), i.e., the mg-pair (R, A × B), where R is the submonoid generated by A × B in the usual direct product S × T of the monoids S and T.

In addition to the reverse semidirect product, we will also make use of the reverse wreath product. Suppose that (S, A) and (T, B) are mg-pairs. Then consider the direct power (S, A)^{T} of (S, A), i.e., the mg-pair (R, A^{T}), where R is the submonoid of S^{T} generated by A^{T}. Define the right action of T on R by

(ft)(t′) = f(tt′),

for all f ∈ R and t, t′ ∈ T. Then the reverse wreath product (S, A) ∘_{r} (T, B) is the reverse semidirect product (R, A^{T})⋆_{r} (T, B) determined by the above action.

In the sequel, except for free mg-pairs, we will only consider finite mg-pairs. We call a nonempty class of finite mg-pairs a variety if it is closed with respect to division and direct product. A closed variety is also closed with respect the reverse semidirect product (or reverse wreath product). For any class K of finite mg-pairs, we let K̂ denote the least closed variety containing K. An example of a closed variety is the class D^{r} of all reverse definite mg-pairs. We call a finite mg-pair (M, A) reverse definite if there exists an integer n ≥ 0 such that a_{1} ⋯ a_{n} = a_{1} ⋯ a_{n+1} for all a_{1}, …, a_{n+1} in A. For example, when M_{n} denotes the monoid of all words over the two-letter alphabet {a, b} whose length is at most n equipped with the product operation u·v = w iff w is the maximal prefix of uv of length ≤ n, then E_{n} = (M_{n}, {a, b}) is a reverse definite mg-pair. Below we will write E for E_{2}. Note that E_{n} is a quotient of E_{n+1}, for all n. Each E_{n} generates D^{r}:

Proposition 5. For each n ≥ 1, D^{r} is the least closed variety containing E_{n}.

This follows by adapting the proof of a well-known fact for definite semigroups, proved in Eilenberg [5]. Further examples of closed varieties will be introduced when needed. When V and W are closed varieties, we let V ∨ W denote the least closed variety containing V ∪ W.

Suppose that K is a class of finite mg-pairs. We let L_{K} denote the class of all regular languages recognizable by the mg-pairs in K. By standard arguments, it follows that a language is in L_{K} iff its syntactic mg-pair is in the variety generated by K. Conversely, when L is a class of regular languages, let K_{L} denote the class of all syntactic mg-pairs of the languages in L.

For each class K of finite mg-pairs, we define FTL(K) = FTL(L_{K}) and FTL(K) = FTL(L_{K}).

Corollary 3. Let L denote a class of regular languages. We have FTL(L) = FTL(K_{L}) iff there exists some class K of finite mg-pairs with FTL(L) = FTL(K) iff for each L ⊆ Δ^{∗} in L and for each w ∈ Δ^{∗}, the modal operators associated with w^{−1}L and Lw^{−1} are expressible in FTL(L) as in Propositions 3 and 4.

Remark 1. Given a class K of finite mg-pairs, let L denote the class of all regular languages L ⊆ A^{∗} such that there exists some mg-pair (S, A) ∈ K with L = h^{−1}(h(L)), where h denotes the homomorphism (A^{∗}, A) → (S, A) which is the identity function on A. Then it follows from Corollary 2 and Corollary 1 that FTL(K) = FTL(L).

5 Main Results

We say that the next modality is expressible in FTL(L) if for each formula φ in FTL(L) over any alphabet Σ there is a formula Xφ over Σ such that for all u ∈ Σ^{∗},

u ⊧ Xφ ⇔ ∃σ ∈ Σ, v ∈ Σ^{∗} u = σv ∧ v ⊧ φ.

Proposition 6. The next modality is expressible in FTL(L) iff the two-letter regular language (a+b)b(a+b)^{∗} and the one-letter language a belong to FTL(L).

Proof. Suppose first that L_{1} = (a + b)b(a + b)^{∗} and L_{2} = a are in FTL(L). Let φ be any formula in FTL(L) over the alphabet Σ. If ϵ |̸= φ, then Xφ is expressible as L_{1}(a ↦ ¬φ, b ↦ φ). If ϵ ⊧ φ, then Xφ is expressible by L_{1}(a ↦ ¬φ, b ↦ φ) ∨ L_{2}(a ↦ tt). It follows from Corollary 1 that the next modality is expressible in FTL(L).

Suppose now that the next modality is expressible in FTL(L), so that Xφ exists for each formula φ in FTL. Then (a + b)b(a + b)^{∗} is definable by Xp_{b}, and a is definable by p_{a} ∧ X¬p_{a}. □

Note that the mg-pair E defined above is isomorphic to the syntactic mg-pair of the language (a + b)b(a + b)^{∗}. Using this fact, we have:

Corollary 4. For any class K of finite mg-pairs, the next modality is expressible in FTL(K) iff (a+b)b(a+b)^{∗} belongs to FTL(K) iff every language recognizable by E belongs to FTL(K).

Proof. If L = (a + b)b(a + b)^{∗} belongs to FTL(K), then, by Corollary 2, so does a, regarded as a one-letter language, since it can be constructed from L by the boolean operations, left quotients, and inverse literal homomorphisms. The first equivalence in Corollary 4 now follows from Proposition 6. As for the second, it is clear that if every language recognizable by E belongs to FTL(K), then so does the language (a + b)b(a + b)^{∗}, since it is recognizable by E. On the other hand, it can be shown by standard arguments that any language recognizable by the syntactic mg-pair of a regular language L is the inverse image under a literal homomorphism of a boolean combination of quotients of L. Thus, since E is the syntactic monoid of (a + b)b(a + b)^{∗}, if (a + b)b(a + b)^{∗} is in FTL(K), then since FTL(K) is closed with respect to the above operations, it follows that every language recognizable by E is in FTL(K). □

Corollary 5. For any class K of finite mg-pairs, the next modality is expressible in FTL(K) iff FTL(K) = FTL(K_{1}), where K_{1} = K ∪ {E}.

Proof. By Corollary 4 and Corollary 1. □

Proposition 7. Suppose that (S, A) and (T, B) are finite mg-pairs and (R, A × B) is a reverse semidirect product of (S, A) and (T, B) determined by a right action of T on S. If every language recognizable by (S, A) and (T, B) belongs to FTL(L), and if the next modality is expressible in FTL(L), then every language recognizable by (R, A × B) also belongs to FTL(L).

Proof. Let h denote a homomorphism

(Σ^{∗}, Σ) → (R, A × B)
u ↦ h(u) = (h_{ℓ}(u), h_{r}(u)).

It suffices to show that for each (s, t) ∈ R, the language h^{−1}((s, t)) belongs to FTL(L).

For each u ∈ A^{∗}, let \overline{u} denote the image of u under the homomorphism (A^{∗}, A) → (S, A) which is the identity map on A. Moreover, let ĥ denote the function Σ^{∗} → A^{∗} defined by

ĥ(ϵ) = ϵ
ĥ(σu) = [h_{ℓ}(σ)h_{r}(u)]ĥ(u),

for all u ∈ Σ^{∗} and σ ∈ Σ. Here, h_{ℓ}(σ)h_{r}(u) is the result of the right action of h_{r}(u) on h_{ℓ}(σ). Note that |ĥ(u)| = |u| and that ĥ(u) is a suffix of ĥ(v) whenever u is a suffix of v. Also, \overline{ĥ(u)} = h_{ℓ}(u), for all u ∈ Σ^{∗}.

By assumption, for each s ∈ S and t ∈ T there exist a formula φ_{s} over A and a formula φ_{t} over Σ in FTL(L) such that

L_{φ_{s}} = \{w ∈ A^{∗} : \overline{w} = s\}
L_{φ_{t}} = {u ∈ Σ^{∗} : h_{r}(u) = t}.

Given a formula ψ over A in FTL(L), let

ψ′ = ψ[p_{a} ↦ ⋁_{h_{ℓ}(σ)t=a}(p_{σ} ∧ Xφ_{t})].

Claim For all u ∈ Σ^{∗},

u ⊧ ψ′ ⇔ ĥ(u) ⊧ ψ.

We prove this claim by induction on the structure of ψ. When ψ is p_{a}, for some a ∈ A, we have

u ⊧ ψ′ ⇔ ∃σ, t[u ⊧ p_{σ} ∧ u ⊧ Xφ_{t} ∧ h_{ℓ}(σ)t = a]
⇔ ∃σ, t, v[u = σv ∧ v ⊧ φ_{t} ∧ h_{ℓ}(σ)t = a]
⇔ ∃σ, t, v[u = σv ∧ h_{r}(v) = t ∧ h_{ℓ}(σ)t = a]
⇔ ∃σ, v[u = σv ∧ h_{ℓ}(σ)h_{r}(v) = a]
⇔ ĥ(u) ⊧ p_{a}
⇔ ĥ(u) ⊧ ψ.

The induction step is obvious when ψ is the disjunction ψ_{1} ∨ ψ_{2} or a negation ¬ψ_{1}. Suppose now that ψ is L(δ ↦ ψ_{δ})_{δ∈Δ}, where L ⊆ Δ^{∗} is in L and each φ_{δ} is a formula in FTL(L) over Σ satisfying the induction assumption. Suppose that u = u_{1} ⋯ u_{n}, say. By the induction hypothesis we have that for all i ∈ [n] and δ ∈ Δ,

u_{i} ⋯ u_{n} ⊧ ψ′_{δ} ⇔ ĥ(u_{i} ⋯ u_{n}) ⊧ ψ_{δ}.

Thus, since ĥ preserves suffixes, the characteristic word determined by u and ψ′ is the same as that determined by ĥ(u) and ψ, proving that u ⊧ ψ′ iff ĥ(u) ⊧ ψ.

We now complete the proof of the proposition. For any (s, t) ∈ R and u ∈ Σ^{∗},

h(u) = (s, t) ⇔ h_{ℓ}(u) = s ∧ h_{r}(u) = t
⇔ \overline{ĥ(u)} = s ∧ h_{r}(u) = t
⇔ ĥ(u) ⊧ φ_{s} ∧ u ⊧ φ_{t}
⇔ u ⊧ φ′_{s} ∧ φ_{t}.

Thus, φ′_{s} ∧ φ_{t} defines h^{−1}((s, t)). □

Proposition 8. Suppose that φ = K(δ ↦ φ_{δ})_{δ∈Δ} is a formula over Σ in FTL(L), where φ_{δ}, δ ∈ Δ is a deterministic family. Suppose that K is recognized by h_{K} : (Δ^{∗}, Δ) → (S, A) and that each L_{φ_{δ}} is recognized by the morphism h : (Σ^{∗}, Σ) → (T, B). Then L_{φ} ⊆ Σ^{∗} is recognizable by the reverse wreath product (S, A) ∘_{r} (T, B).

Proof. Without loss of generality we may assume that h is surjective. For each δ ∈ Δ, let F_{δ} denote the set h(L_{φ_{δ}}). Note that the sets F_{δ} are pairwise disjoint by assumption, and that ⋃_{δ∈Δ} F_{δ} = T, since h is surjective. Define k : (Σ^{∗}, Σ) → (S, A) ∘_{r} (T, B) by

k(σ) = (f_{σ}, h(σ)),

for all σ ∈ Σ, where for each t ∈ T, f_{σ}(t) = h_{K}(δ) for the unique δ with h(σ)t ∈ F_{δ}. Let u = u_{1} ⋯ u_{n} in Σ^{∗}. We have

k(u) = (f, h(u)),

where

f(t) = h_{K}(δ_{1} ⋯ δ_{n})

for the unique word δ_{1} ⋯ δ_{n} with h(u_{i} ⋯ u_{n})t ∈ F_{δ_{i}} for each i ∈ [n]. In particular,

f(1) = h_{K}(δ_{1} ⋯ δ_{n})

for the unique word δ_{1} ⋯ δ_{n} with h(u_{i} ⋯ u_{n}) ∈ F_{δ_{i}}, i.e.,

u_{i} ⋯ u_{n} ⊧ φ_{δ_{i}}

for each i ∈ [n]. Thus,

f(1) ∈ h_{K}(K) ⇔ δ_{1} ⋯ δ_{n} ∈ K
⇔ u ⊧ φ.

It follows that

L_{φ} = {u ∈ Σ^{∗} : f(1) ∈ h_{K}(K)}.

This proves that L_{φ} is recognizable by (S, A) ∘_{r} (T, B). □

Recall that E_{1} denotes the mg-pair ({1, a, b}, {a, b}), where 1 is the identity element and a, b are both left-zeroes. Note that E_{1} is just the syntactic mg-pair of the language a(a + b)^{∗}.

Theorem 1. For any class K of finite mg-pairs, every language in FTL(K) is recognizable by some mg-pair in K̂ ∨ D^{r}.

Proof. Let φ denote a deterministic formula over Σ in FTL(K). When φ is p_{σ}, for some σ ∈ Σ, then L_{φ} = σΣ^{∗}, which is recognizable by E_{1} ∈ D^{r}. We continue by induction on the structure of φ. Assume that φ = φ_{1} ∨ φ_{2} such that L_{φ_{i}} is recognizable by (S_{i}, A_{i}) in K̂∨D^{r}, i = 1, 2. Then L_{φ} is recognizable by the direct product (S_{1}, A_{1}) × (S_{2}, A_{2}) which is also in K̂ ∨ D^{r}. When φ = ¬φ_{1}, where L_{φ_{1}} is recognizable by (S_{1}, A_{1}) above, then L_{φ} is recognizable by the same mg-pair (S_{1}, A_{1}). Finally, when φ = L(δ ↦ φ_{δ})_{δ∈Δ} and each L_{φ_{δ}} is recognizable by some mg-pair in K̂ ∨ D^{r}, then it follows by Proposition 8 that L_{φ} is recognizable by some mg-pair in K̂ ∨ D^{r}. (Note that since K̂ ∨ D^{r} is closed with respect to the direct product, we may assume without loss of generality that each L_{φ_{δ}} is recognizable by the same mg-pair (M, A) in K̂ ∨ D^{r}, and in fact by the same morphism (Σ^{∗}, Σ) → (M, A).) □

Theorem 2. Suppose that the next modality is expressible in FTL(K), where K is a class of finite mg-pairs. Then a language L belongs to FTL(K) iff Synt(L) belongs to K̂ ∨ D^{r}.

Proof. First, by Corollary 5, we have FTL(K) = FTL(K_{1}), where K_{1} = K ∪ {E}, so that K̂_{1} = K̂ ∨ D^{r}. Let us define the rank of (S, A) ∈ K̂ ∨ D^{r} to be the smallest number of reverse semidirect product and division operations needed to generate (S, A) from K_{1}. We prove by induction on the rank of (S, A) that every language recognizable by (S, A) is in FTL(K_{1}). When the rank is 0 we have (S, A) ∈ K_{1}. Thus the result follows from Proposition 1. When the rank of (S, A) is positive, then (S, A) either divides an mg-pair (T, B) in K̂ ∨ D^{r} of smaller rank, or (S, A) is the reverse semidirect product of some mg-pairs in K̂∨D^{r} of smaller rank. In the first case, every language recognizable by (S, A) is recognizable by (T, B). In the second case, the result follows from Proposition 7.

To necessity part of Theorem 2 follows from Theorem 1. □

Corollary 6. For each class L of regular languages, FTL(L) consists of regular languages.

Call a nonempty class of regular languages L closed if FTL(L) ⊆ L and if L is closed with respect to quotients. By Propositions 1, 3 and 4, every closed class is a literal variety, i.e., it is closed with respect to the boolean operations, quotients, and inverse literal homomorphisms. Moreover, by Corollaries 1, 2 and 3, L is closed iff L = FTL(L′) for a class L′ of regular languages closed with respect to quotients iff L = FTL(K) for a class K of finite mg-pairs.

The assignment V ↦ L_{V} defines an order isomorphism between varieties V of finite mg-pairs and literal varieties of regular languages, cf. Ésik, Larsen [7]. The inverse assignment maps a literal variety L to the class of those finite mg-pairs (M, A) such that every language recognizable by (M, A) belongs to L.

Theorem 3. The assignment V ↦ L_{V} = FTL(V) defines an order isomorphism between closed varieties V of finite mg-pairs containing D^{r} and closed classes L of regular languages containing (a + b)b(a + b)^{∗}.

Proof. If V is a closed variety containing D^{r}, then by Theorem 1, L_{V} is a closed class of regular languages containing (a + b)b(a + b)^{∗}. Since FTL(V) is the least closed class containing L_{V}, it follows that L_{V} = FTL(V). As mentioned above, we have V_{1} ⊆ V_{2} iff L_{V_{1}} ⊆ L_{V_{2}}. Finally, the map is surjective, for if L is a closed class of regular languages containing (a + b)b(a + b)^{∗}, then L = L_{V} for some variety V of finite mg-pairs containing E. By Proposition 7, V is closed with respect to the reverse semidirect product. Since V contains E, by Proposition 5 it also contains all the reverse definite mg-pairs. □

We refer to Almeida [1] for a detailed study of varieties of finite semigroups closed with respect to the semidirect product. Any such variety gives rise to a closed variety of finite mg-pairs.

Example 2. The closed class of regular languages corresponding to D^{r} is the class of reverse definite languages, where a language L ⊆ Σ^{∗} is termed reverse definite iff there is some n ≥ 0 such that the membership of a word u in L depends only on the maximal prefix of u of length ≤ n. (This condition is equivalent to requiring that the language is recognizable by some E_{n}.)

6 Some Applications

Propositional (future) temporal logic (FTL) was introduced in Pnueli [10]. The formulas of FTL over an alphabet Σ are constructed from the letters p_{σ}, σ ∈ Σ by the boolean connectives ∨ and ¬ and the next and until modalities, denoted Xφ and φUψ. The semantics of FTL are defined similarly to that of FTL(L). In particular, when u = u_{1} ⋯ u_{n} ∈ Σ^{∗} and φ and ψ are formulas over Σ,

1. u ⊧ Xφ iff n ≥ 1 and u_{2} ⋯ u_{n} ⊧ φ,

2. u ⊧ φUψ iff there exists some i ∈ [n] such that u_{i} ⋯ u_{n} ⊧ ψ and u_{j} ⋯ u_{n} ⊧ φ for all j < i.

We let FTL denote the class of languages definable by the formulas in FTL.

Let U^{r} denote the monoid component of E_{1}, i.e., the monoid {1, a, b}, where a, b are left-zero elements.

Proposition 9. FTL = FTL({U^{r}, E}).

Proof. The inclusion FTL ⊆ FTL({U^{r}, E}) follows from Corollary 4 and the fact that φUψ is expressible as L_{U}(a ↦ φ ∧ ¬ψ, b ↦ ψ, c ↦ ¬φ ∨ ¬ψ), where L_{U} denotes the language a^{∗}b(a + b + c)^{∗} over the three-letter alphabet {a, b, c} which can be recognized by U^{r}. For the reverse inclusion, one can show easily that every language recognizable by U^{r} or E is definable in FTL. For example, L_{U} is defined by p_{a}Up_{b}. It then follows that the modal operator corresponding to any language recognized by U^{r} or E is expressible in FTL. □

We call a finite mg-pair aperiodic if its monoid component is aperiodic, cf. Eilenberg [5]. For example, U^{r} and E are aperiodic. It follows from (the dual of) the Krohn-Rhodes Decomposition Theorem [5] that the aperiodic mg-pairs form a closed variety, namely the closed variety generated by U^{r}. Let A denote the closed variety of aperiodic mg-pairs. For first-order definable languages, we refer to [9].

Theorem 4. Mc Naughton-Papert [9] A language is first-order definable iff Synt(L) ∈ A.

Theorem 5. Let K denote a class of finite mg-pairs such that the next modality is expressible in FTL(K). Then FTL(K) contains the first-order definable languages iff A ⊆ K̂ ∨ D^{r}. Moreover, FTL(K) is the class of all first-order definable languages iff A = K̂ ∨ D^{r}.

Proof. Immediate from Theorem 2, Theorem 3, the Krohn-Rhodes Decomposition Theorem and the fact that E is aperiodic. □

From Theorem 5 and Proposition 9 we immediately have:

Corollary 7. Kamp [8] A language is first-order definable iff it is in FTL.

We now consider cyclic counting. For any formula φ over Σ and integers k ≥ 1 and 0 ≤ r < k, let C_{k}^{r}φ be a formula with the following semantics. For any u = u_{1} ⋯ u_{n} is Σ^{∗}, u ⊧ C_{k}^{r}φ iff the number of indices i with u_{i} ⋯ u_{n} ⊧ φ is congruent to r modulo k. Similarly, let u ⊧ L_{k}^{r} iff |u| is congruent to r modulo k. Let K and M be two subsets of the naturals. We denote by FTL(K, M) the extension of FTL by the modalities C_{k}^{r}, 0 ≤ r < k and L_{m}^{r}, 0 ≤ r < m with k ∈ K and m ∈ M. Moreover, we denote by FTL(K, M) the class of all languages definable by the formulas in FTL(K, M).

For each n ≥ 1, let Z_{n} denote a cyclic group of order n. Below we will denote by a a cyclic generator of Z_{n} and by 1 the identity element. The division ideal generated by a set M of naturals consists of all divisors of least common multiples of finite sets of naturals in M. When M is empty, the division ideal generated by M is {1}.

Theorem 6. A language L belongs to FTL(K, M) iff Synt(L) = (S, A) satisfies the following condition: There is some m in the division ideal generated by M such that every group contained in the submonoid of S generated by A^{m} is solvable whose order is a multiple of the prime divisors of the integers in K.

Proof. We have FTL(K, M) = FTL(K), where K consists of U^{r}, E and the mgpairs (Z_{k}, {1, a}) and (Z_{m}, {a}), for all k ∈ K and m ∈ M. Thus, by Theorem 3, FTL(K) consists of all languages whose syntactic mg-pair is in K̂. It is shown in Ésik, Ito [6] that the syntactic mg-pair of a language belongs to this variety iff the condition described in the Theorem holds. □

See also Straubing, Therien, Thomas [12], Straubing [11].

For a class K of finite mg-pairs, let FTL + K denote the extension of FTL by the modal operators corresponding to the languages recognizable by the mgpairs in K. Moreover, let FTL + K denote the class of languages definable by the formulas in FTL + K.

Theorem 7. FTL + K is the class of all regular languages iff the following two conditions hold:

1. For each m, (Z_{m}, {a}) ∈ K̂.

2. For each finite (nonabelian simple) group G there is an mg-pair (M, A) in K such that G divides M.

Proof. First, by Theorem 5 and Theorem 2, it follows that a language belongs to FTL + K iff its syntactic mg-pair is contained in the closed variety V generated by K and the aperiodics. Now, by (the dual of) a result proved in Dömösi, Ésik [4], V is the class of all finite mg-pairs iff the above two conditions hold. The result now follows by using Theorem 3, since a language is regular iff it is recognizable by a finite mg-pair. □

Corollary 8. If FTL+K is the class of all regular languages, then K is infinite.

Example 3. Let K consist of the mg-pairs (S_{n}, {π, ρ}), n ≥ 3, where S_{n} denotes the symmetric group of all permutations of the set [n], and where π is a transposition and ρ is a cyclic permutation of [n]. Then FTL + K is the class of all regular languages.

When K is a class of finite mg-pairs, let FTL + MOD + K denote the language class FTL + K′, where K′ = K ∪ {(Z_{n}, {1, a}) : n ≥ 2}. The proof of the following result is similar to that of Theorem 7.

Theorem 8. A language L belongs to FTL + MOD + K iff L is regular and for every finite nonabelian simple group G, if G divides the syntactic monoid of L, then G divides the monoid component of an mg-pair in K.

Given a formula φ of FTL over the alphabet Σ, let ⟨⟩φ denote the formula ttUφ. Thus, for each word u = u_{1} ⋯ u_{n} in Σ^{∗}, u ⊧ ⟨⟩φ iff u_{1} ⋯ u_{n} ⊧ φ, for some i ∈ [n]. In [3], Cohen, Perrin and Pin studied the expressive power of the restricted temporal logic RTL whose formulas over an alphabet Σ are constructed from the atomic formulas p_{σ}, σ ∈ Σ by the X and ⟨⟩ modalities. Let RTL denote the class of languages definable by the formulas in RTL. Let U_{1} denote a two-element semilattice (which may be identified with the mg-pair (U_{1}, U_{1})).

Proposition 10. RTL = FTL({U_{1}, E}).

The proof is based on the observation that U_{1} is isomorphic to the syntactic monoid of the two-letter language L = (a + b)^{∗}b(a + b)^{∗}, and for any formula φ, ⟨⟩φ is expressible as L(a ↦ ¬φ, b ↦ φ).

Recall that a semigroup S is called L-trivial, cf. Almeida [1], Eilenberg [5], if Green’s L-relation on S is the equality relation. Moreover, a semigroup S is locally L-trivial iff for each idempotent e, the monoid eSe is L-trivial. Accordingly, we call an mg-pair (M, A) locally L-trivial if the subsemigroup of M generated by A is locally L-trivial.

It follows from well-known facts (cf. [5, 1]) that a finite mg-pair is locally L-trivial iff it belongs to the least closed variety containing U_{1} and E_{1}, or U_{1} and E. Thus, from Proposition 10 and Theorem 2 we may derive:

Theorem 9. Cohen, Perrin, Pin [3] A language L ⊆ Σ^{∗} belongs to RTL iff L is regular and Synt(L) is locally L-trivial.

Following the definitions of the language classes FTL(K, M), we may define the classes RTL(K, M). For lack of space we omit the proof of the following result.

Theorem 10. A language L belongs to RTL(K, M) iff Synt(L) = (S, A) satisfies the following condition: There is an integer m in the division ideal generated by M such that for each idempotent e of the subsemigroup T of S generated by A^{m}, it holds that eT e is a solvable group whose order is a multiple of the primes that divide the integers in K.

References

1. J. Almeida, Finite Semigroups and Universal Algebra, World Scientific, 1994.

2. A. Baziramwabo, P. McKenzie and D. Therien, Modular temporal logic, in: Proc. 1999 IEEE Conference LICS, Trento, Italy.

3. J. Cohen, J.-E. Pin and D. Perrin, On the expressive power of temporal logic, J. Computer and System Sciences, 46(1993), 271–294.

4. P. Dömösi and Z. Ésik, Critical classes for the α_{0}-product, Theoretical Computer Science, 61(1988), 17–24.

5. S. Eilenberg, Automata, Languages, and Machines, vol. A and B, Academic Press, 1974 and 1976.

6. Z. Ésik and M. Ito, Temporal logic with cyclic counting and the degree of aperiodicity of finite automata, Acta Cybernetica, to appear.

7. Z. Ésik and K. G. Larsen, Regular languages definable by Lindström quantifiers, BRICS Reports, RS-02-20, April, 2002.

8. J. A. Kamp, Tense logic and the theory of linear order, Ph. D. Thesis, UCLA, 1968.

9. R. McNaughton and S. Papert, Counter-Free Automata, MIT Press, 1971.

10. A. Pnueli, The temporal logic of programs, in: Proc. 18th FOCS, Providence, RI, IEEE Press, 1977, 46–57.

11. H. Straubing, Finite Automata, Formal Logic, and Circuit Complexity, Birkhauser, 1994.

12. H. Straubing, D. Therien and W. Thomas, Regular languages defined with generalized quantifiers, Information and Computation, 118(1995), 289–301.

13. D. Therien and Th. Wilke, Temporal logic and semidirect products: An effective characterization of the until hierarchy, DIMACS TR-96-28, 1996.

14. P. Wolper, Temporal logic can be more expressive, Information and Control, 56(1983), 72–99.

Recent BRICS Report Series Publications

RS-02-47 Zoltán Ésik. Extended Temporal Logic on Finite Words and Wreath Product of Monoids with Distinguished Generators. December 2002. 16 pp. To appear in 6th International Conference, Developments in Language Theory, DLT ’02 Revised Papers, LNCS, 2002.

RS-02-46 Zoltán Ésik and Hans Leiß. Greibach Normal Form in Algebraically Complete Semirings. December 2002. 43 pp. An extended abstract appears in Bradfield, editor, European Association for Computer Science Logic: 16th International Workshop, CSL ’02 Proceedings, LNCS 2471, 2002, pages 135–150.

RS-02-45 Jesper Makholm Byskov. Chromatic Number in Time O(2.4023^{n}) Using Maximal Independent Sets. December 2002. 6 pp.

RS-02-44 Zoltán Ésik and Zoltán L. Németh. Higher Dimensional Automata. November 2002. 32 pp. A preliminary version appears under the title Automata on Series-Parallel Biposets in Kuich, Rozenberg and Salomaa, editors, 5th International Conference, Developments in Language Theory, DLT ’01 Revised Papers, LNCS 2295, 2001, pages 217–227. This report supersedes the earlier BRICS report RS-01-24.

RS-02-43 Mikkel Christiansen and Emmanuel Fleury. Using IDDs for Packet Filtering. October 2002. 25 pp.

RS-02-42 Luca Aceto, Jens A. Hansen, Anna Ingólfsdóttir, Jacob Johnsen, and John Knudsen. Checking Consistency of Pedigree Information is NP-complete (Preliminary Report). October 2002. 16 pp.

RS-02-41 Stephen L. Bloom and Zoltán Ésik. Axiomatizing Omega and Omega-op Powers of Words. October 2002. 16 pp.

RS-02-40 Luca Aceto, Willem Jan Fokkink, and Anna Ingólfsdóttir. A Note on an Expressiveness Hierarchy for Multi-exit Iteration. September 2002. 8 pp.

RS-02-39 Stephen L. Bloom and Zoltán Ésik. Some Remarks on Regular Words. September 2002. 27 pp.