BRICS RS-01-53 Ésik & Ito: Temporal Logic with Cyclic Counting BRICS

Basic Research in Computer Science

Temporal Logic with Cyclic Counting and the Degree of Aperiodicity of Finite Automata

Zoltán Ésik Masami Ito BRICS Report Series RS-01-53 ISSN 0909-0878 December 2001 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2001, Zoltán Ésik & Masami Ito.

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/01/53/

Temporal Logic with Cyclic Counting and the Degree of Aperiodicity of Finite Automata

Z. Ésik^{∗}

Dept. of Computer Science University of Szeged Szeged, Hungary

esik@inf.u-szeged.hu

M. Ito^{†}

Dept. of Mathematics Kyoto Sangyo University Kyoto, Japan

ito@ksuvx0.kyoto-su.ac.jp

December, 2001

Abstract

We define the degree of aperiodicity of finite automata and show that for every set M of positive integers, the class QA_{M} of finite automata whose degree of aperiodicity belongs to the division ideal generated by M is closed with respect to direct products, disjoint unions, subautomata, homomorphic images and renamings. These closure conditions define qvarieties of finite automata. We show that q-varieties are in a one-to-one correspondence with literal varieties of regular languages. We also characterize QA_{M} as the cascade product of a variety of counters with the variety of aperiodic (or counter-free) automata. We then use the notion of degree of aperiodicity to characterize the expressive power of first-order logic and temporal logic with cyclic counting with respect to any given set M of moduli. It follows that when M is finite, then it is decidable whether a regular language is definable in first-order or temporal logic with cyclic counting with respect to moduli in M.

∗The results of this paper were obtained during the first author’s visit at the Faculty of Science at the Kyoto Sangyo University and at the Department of Computer Science at the University of Aalborg. The first author was partially supported by Grant-in-Aid 10044098, Japan Society for the Promotion of Science, by BRICS (Basic Research in Computer Science), and by grant no. T30511 from the National Foundation of Hungary for Scientific Research.

†Partially supported by Grant-in-Aid 10044098, Japan Society for the Promotion of Science.

1 Introduction

The richness of the theory of regular languages is due to the many different characterizations of (subclasses of) regular languages. By the theorem of Büchi and Elgot, a language is regular iff it is definable in monadic second-order logic over words [2, 5] involving the predicate < and a predicate corresponding to each letter of the alphabet. Moreover, by classic results of Schützenberger [13] and Mc Naughton and Papert [10], a language is star-free iff it is definable in firstorder logic iff it is accepted by an aperiodic (or counter-free) finite automaton. Thus, it is decidable for a regular language whether or not it is definable in firstorder logic, or has a star-free expression. Moreover, by a classic result of Kamp [9] and Gabbay et al. [7], the logic LTL of Linear (Propositional) Temporal Logic over words has the same expressive power as first-order logic.

The above results have been extended in several directions involving, in addition to words, also ω-words, trees and other structures, see [17, 18] for overviews. In order to increase the expressive power of first-order logic on words, two kinds of cyclic counting have been studied: the extension of first-order logic with numerical predicates C_{m}^{r}(x) that holds for a position x in a word iff x is congruent to r modulo m, see [1, 15], and the extension with modular quantifiers, cf. [16, 15]. In this paper our concern is the first type of counting. In [1], Barrington, Compton, Straubing and Therien gave a decidable characterization of the languages definable in first-order logic with counting with respect to the predicates C_{m}^{r}(x), where the modulus m ranges over all positive integers and r is any nonnegative integer < m. However, this characterization does not answer the question that, given a finite set M of moduli, what languages are definable by using only predicates involving moduli in M. Our aim in this paper is to provide an analysis of the above mentioned result of Barrington, Compton, Straubing and Therien that will allow to answer the previous question. Moreover, we also study an extension of temporal logic yielding the same expressive power.

We define the degree of aperiodicity of finite automata and show that for every set M of positive integers, the class QA_{M} of automata whose degree of aperiodicity belongs to the division ideal generated by M is closed with respect to direct products, disjoint unions, subautomata, homomorphic images and renamings. These closure conditions define q-varieties. We show that q-varieties are in a one-to-one correspondence with literal varieties of regular languages. We also characterize QA_{M} as the cascade product of a variety of counters with the variety of aperiodic (or counter-free) automata. We then use the notion of degree of aperiodicity to characterize the expressive power of first-order logic and temporal logic with cyclic counting with respect to any given set M of moduli. When M is finite, this characterization is effective.

The paper is organized as follows. In Section 2 we define literal varieties of regular languages, q-varieties of finite automata, and establish an Eilenberg-type correspondence between them. In Section 3, we recall the notion of cascade product of finite automata together with a few basic facts regarding regular languages accepted by cascade products. We also define cascade products V ⋆ W of q-varieties. Then, in Section 4, we study q-varieties of finite automata of the form C_{M} ⋆ V, where M is a given subset of the positive integers and C_{M} is the q-variety generated by all counters whose length belongs to M. Then, in Section 5, we define the degree of aperiodicity of finite automata and show that for every set M as above, the finite automata whose degree of aperiodicity belongs to the division ideal generated by M form a q-variety QA_{M} which is the cascade product of C_{M} with the q-variety of aperiodic (counter-free) automata. Moreover, we show that the degree of aperiodicity of a finite automaton is computable. We also show that a language can be recognized by an automaton in QA_{M} iff it can be constructed from the finite languages and the languages consisting of all words over the underlying alphabet whose length is a multiple of some integer in M by the boolean operations and concatenation. Then, in Section 6 we prove that the very same condition characterizes the languages definable in first-order logic with cyclic counting with respect to moduli in M. When M is empty or M is the set of all positive integers, these results correspond to those of Schützenberger [13], Mc Naughton and Papert [10], and Barrington et al. [1] mentioned above. In Section 7, we provide several extensions of propositional temporal logic with cyclic counting and show that all these are equivalent. Moreover, we show that temporal logic with cyclic counting with respect to any given set M of moduli has the same expressive power as first-order logic with counting with respect to moduli in M. When M is empty, this fact corresponds to the result of Kamp [9] and Gabbay et al. [7]. Section 8 contains a summary of the results obtained and outlines some future results.

2 An Eilenberg correspondence

A finite alphabet, or just alphabet, for short, is any finite nonempty set whose elements are called letters. When Σ is an alphabet, we let Σ^{∗} denote the free monoid of words over Σ including the empty word ϵ equipped with the operation of concatenation as product. For any word u = a_{0} … a_{n−1}, where the a_{i} are letters, we call the integer n the length of u and denote it by |u|. We let Σ^{n} denote the set of all words in Σ^{∗} of length n. The prefix order ≤ on words is defined by u ≤ v iff there is a word z with uz = v, i.e., when u is a prefix of v. Suppose that h is a (monoid) homomorphism Σ^{∗} → Δ^{∗}, where Σ, Δ are finite alphabets. We call h nonerasing if ah ≠ ϵ holds for all a ∈ Σ. Moreover, we call h a literal homomorphism if ah ∈ Δ holds for all a ∈ Σ.

A language (over Σ) is any subset of Σ^{∗}. Languages over Σ are equipped with several operations including the boolean operations ∪, ∩ and ^{c} (complement), product (or concatenation), Kleene star (^{∗}), left and right quotients, homomorphisms, inverse homomorphisms, etc. These are defined in the standard way. When L ⊆ Σ^{∗} and u ∈ Σ^{∗}, we let u^{−1}L and Lu^{−1} denote the left and right quotients of L with respect to u, respectively:

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

We will sometimes identify a word w with the singleton set {w} and write w^{∗} for the Kleene star {w}^{∗} of the language {w}.

Recall that a language L ⊆ Σ^{∗} is called regular if it can be constructed from the finite subsets of Σ^{∗} by the regular operations of union, product and Kleene star. It is well-known that the class of regular languages is closed with respect to all of the operations mentioned above. Moreover, by Kleene’s classic theorem, the regular languages are exactly those languages that can be recognized by finite automata.

In this paper, by a finite automaton, or just automaton, we mean a system Q = (Q, Σ, ·) consisting of a finite nonempty set Q of states, a finite input alphabet Σ and a right action of Σ on Q, i.e., a function · : Q × Σ → Q, which is extended to an action of Σ^{∗} on Q in the usual way. Below we will usually write just qu for q · u, for all q ∈ Q and u ∈ Σ^{∗}. The function q ↦ qu is called the function induced by u, denoted u^{Q}. When we want to emphasize that the input alphabet of an automaton is some alphabet Σ, we call it a Σ-automaton. Suppose that L ⊆ Σ^{∗} and that Q = (Q, Σ, ·) is a Σ-automaton. We say that L is recognizable in Q, or that L can be recognized by Q, if there is a state q_{0} ∈ Q, the initial state, and a set F ⊆ Q of final states such that L = {u ∈ Σ^{∗} : q_{0}u ∈ F }. Moreover, a language is called recognizable if it can be recognized by some finite automaton. The aforementioned theorem of Kleene equates the recognizable languages with the regular languages.

Recall [4, 11] that a stream (or class) V of regular languages is a nonempty collection Σ^{∗}V of regular languages over Σ, for each finite alphabet Σ. Streams of regular languages are ordered by set inclusion: we write V ⊆ V′ if Σ^{∗}V ⊆ Σ^{∗}V′, for all finite alphabets Σ.

Definition 2.1 A literal variety (of languages), or l-variety, for short, is a stream V of regular languages closed with respect to the boolean operations, left and right quotients and inverse literal homomorphisms. Thus, if L_{1}, L_{2} ∈ Σ^{∗}V and a ∈ Σ, then L_{1} ∪ L_{2}, L_{1} ∩ L_{2}, L_{1}^{c}, a^{−1}L_{1} and L_{1}a^{−1} are all in Σ^{∗}V. Moreover, if h is a literal homomorphism Δ^{∗} → Σ^{∗}, so that Δh ⊆ Σ, then L_{1}h^{−1} ∈ Δ^{∗}V.

A ∗-variety (+-variety) of languages is a literal variety which is closed with respect to all (nonerasing) inverse homomorphisms.

Example 2.2 It is clear that l-varieties form a complete lattice, in fact, an algebraic lattice. The largest l-variety contains, for each Σ, all the regular languages in Σ^{∗}, and the smallest only the empty language and the language Σ^{∗}. When {V_{i} : i ∈ I} is a directed set of l-varieties, the least upper bound V = ⋁_{i∈I} V_{i} is just the union ⋃_{i∈I} V_{i}, so that Σ^{∗}V = ⋃_{i∈I} Σ^{∗}V_{i}, for each Σ.

Example 2.3 Of course, every ∗-variety or +-variety is a literal variety. For each Σ, let Σ^{∗}L consist of all regular languages L in Σ^{∗} such that for all words u, v ∈ Σ^{∗}, if u ∈ L and |u| = |v|, then v ∈ L. Then L is a literal variety which is not a +-variety or a ∗-variety.

The l-varieties contained in L correspond to those boolean algebras of regular languages over the one-letter alphabet closed with respect to quotients. We give some examples of such varieties.

Suppose that d ≥ 1 is an integer. The l-variety C_{d} is that generated by the one-letter regular language (a^{d})^{∗}, considered as a subset of a^{∗}. It is not hard to see that each language in Σ^{∗}C_{d} is a finite union of languages of the form (Σ^{d})^{∗}Σ^{i}, where i is an integer in [d] = {0, 1, …, d − 1}.

Suppose that M is a subset of the set Nat of positive integers. Then let C_{M} denote the smallest l-variety containing all of the C_{m} with m ∈ M. It is clear that C_{M} is the union of those C_{d} where d is contained in the division ideal (M] generated by M. (Of course, (M] consists of all divisors of least common multiples of finite families of elements of M.) Thus, C_{M} ⊆ C_{M′} iff (M] ⊆ (M′]. We write C for C_{Nat}.

Further examples of literal varieties that are not ∗-varieties or +-varieties will be given later.

Remark 2.4 The ∗-varieties defined above are the same as the ∗-varieties of Eilenberg [4], see also [11]. However, Eilenberg’s +-varieties [4] are streams of regular languages containing only nonempty words closed with respect to the boolean operations, left and right quotients, and nonerasing inverse homomorphisms. If V is a +-variety as defined in Definition 2.1, and if Σ^{+}W = Σ^{∗}V ∩ Σ^{+}, for each Σ, where Σ^{+} denotes the free semigroup of all nonempty words over Σ, then W is an Eilenberg +-variety. This mapping V ↦ W is surjective but not injective.

Suppose that W is an Eilenberg +-variety. For each alphabet Σ, define

Σ^{∗}V = {L, L ∪ ϵ : L ∈ Σ^{+}W}.

Then V is a +-variety, as defined in Definition 2.1, which is mapped to W. If for some Σ, there is a finite nonempty set in Σ^{+}W, then this is in fact the unique +-variety mapped to W. However, if Σ^{∗}V = {∅, Σ^{∗}} and Σ^{∗}V′ = {∅, ϵ, Σ^{+}, Σ^{∗}}, for each alphabet Σ, then the same Eilenberg +-variety W corresponds to both V and V′:

Σ^{+}W = {∅, Σ^{+}},

for each Σ.

A stream (or class) V of finite automata is a nonempty collection ΣV of finite Σ-automata, for each finite alphabet Σ. Streams of finite automata are ordered by set inclusion in the same way as streams of regular languages.

The notions of subautomaton and quotient (or homomorphic image) of an automaton are defined as usual. When Q = (Q, Σ, ·) and Q′ = (Q′, Σ, ·) are automata with the same set of input letters, the direct product Q × Q′ = (Q×Q′, Σ, ·) is equipped with the pointwise action, so that (q, q′)·a = (qa, q′a), for all q ∈ Q, q′ ∈ Q′ and a ∈ Σ. The disjoint sum (or disjoint union) of Q and Q′ is also defined in the standard way. It is the automaton Q ⊕ Q′ = (Q × {0} ∪ Q × {1}, Σ, ·), where (q, 0)a = (qa, 0) and (q′, 1)a = (q′a, 1), for all q ∈ Q and q′ ∈ Q′. Suppose now that Q = (Q, Σ, ·) and Q′ = (Q′, Δ, ·), where Σ and Δ are any alphabets. We say that Q can be constructed from Q′ by renaming, or that Q is a renaming of Q′, if Q = Q′ and there is a function h : Σ → Δ such that qa = q(ah), for all q ∈ Q and a ∈ Σ.

Definition 2.5 A q-variety of finite automata is any stream of finite automata closed with respect to the operations of taking subautomata, quotients, direct products, disjoint sums and renamings.

We use the prefix to distinguish q-varieties from varieties (or pseudo-varieties) that are nonempty classes of automata with the same input alphabet closed with respect to the operations of taking subautomata, quotients, and direct products, and to express that q-varieties are also closed with respect to the quasi-direct product [8].

Since a q-variety V is nonempty and closed with respect to subautomata, quotients, direct product and renaming, closure under disjoint sum is clearly equivalent to the requirement that the two-element discrete automaton with a single input letter belongs to V. (A Σ-automaton is called discrete if it is a disjoint sum of trivial, i.e., one-state Σ-automata.)

A ∗-variety (+-variety) of finite automata is a q-variety that is also closed with respect to the operation Q ↦ Q^{∗} (Q ↦ Q^{+}). Here, the operation Q ↦ Q^{∗} is defined as follows. Let Q = (Q, Σ, ·), say, and let M(Q) denote the monoid of Q. Thus, the elements of M(Q) are the functions u^{Q} : Q → Q induced by the words u ∈ Σ^{∗}, and the product operation in M(Q) is function composition written left-to-right. Now Q^{∗} is (Q, M(Q), ·), where for each q ∈ Q and u ∈ Σ^{∗}, q·u^{Q} is just qu = q·u, the image of q under u^{Q}. The automaton Q^{+} is defined in the same way except that its alphabet is S(Q) = {u^{Q} : u ∈ Σ^{+}}, the semigroup of Q.

Remark 2.6 It is clear that ∗-varieties of finite automata correspond in a bijective manner to varieties of finite monoids as defined in [4, 11]. Given a ∗-variety V of finite automata, the corresponding variety of finite monoids consists of all monoids that are isomorphic to the monoid of some automaton in V.

However, a similar function mapping +-varieties of finite automata to varieties of finite monoids is only surjective, but not injective. See also Remark 2.4.

Example 2.7 The set of all q-varieties equipped with set inclusion is an algebraic lattice. The largest q-variety contains, for each Σ, all Σ-automata, and the smallest one only the discrete Σ-automata. When {V_{i} : i ∈ I} is a directed set of q-varieties, the least upper bound ⋁_{i∈I} V_{i} is just the union ⋃_{i∈I} V_{i}.

Example 2.8 For each Σ, the q-variety L consists of all autonomous Σ-automata, i.e., all the automata Q = (Q, Σ, ·) such that qa = qb, for all q ∈ Q and a, b ∈ Σ.

Given an integer d ≥ 1, the q-variety C_{d} has, as its members in ΣC_{d}, all the Σ-automata that are disjoint sums of Σ-counters of length a divisor of d. A Σ-counter is an automaton (Q, Σ, ·) such that each letter in Σ induces the same cyclic permutation Q → Q. The length of the counter is |Q|, the number of states in Q. Note that C_{d} is contained in L.

When M is a set of positive integers, then we define C_{M} = ⋁_{m∈M} C_{m}, so that C_{M} is the least q-variety containing all of the C_{m} with m ∈ M. Note that C_{M} is just the union of the C_{d} with d any integer in (M]. Thus, C_{M} ⊆ C_{M′} iff (M] ⊆ (M′]. We denote C_{Nat} by C.

Suppose that V is a q-variety. The corresponding stream V of regular languages contains those languages in Σ^{∗}V that can be recognized by an automaton in ΣV (by a suitable initial state and a set of final states). Thus, a language L ⊆ Σ^{∗} belongs to Σ^{∗}V if and only if there is an automaton Q = (Q, Σ, ·) in V, a state q_{0} ∈ Q and a set F ⊆ Q such that the language recognized by Q with initial state q_{0} and final states F is L. Alternatively, a (regular) language L ⊆ Σ^{∗} belongs to Σ^{∗}V if and only if the minimal automaton recognizing L is in ΣV.

The following variant of Eilenberg’s variety theorem [4, 11] follows by standard arguments.

Theorem 2.9 The correspondence V ↦ V is an order isomorphism from the lattice of q-varieties of finite automata onto the lattice of l-varieties of regular languages. The same correspondence establishes an order isomorphism between ∗-varieties (+-varieties) of finite automata and ∗-varieties (+-varieties) of regular languages.

Proof. We briefly sketch the proof of the first statement. If L is in Σ^{∗}V, then L is accepted by an automaton in V by a suitable initial state and a set of final states. By taking the same initial state and the complement of the set of final states, the same automaton accepts L^{c}. It is also known that any quotient of L can be accepted by the same automaton with suitable initial and final states. Closure with respect to set union follows from the fact that the union of languages accepted by Q_{1} and Q_{2} can be accepted by the direct product of Q_{1} and Q_{2}. It is clear that V_{1} ⊆ V_{2} implies V_{1} ⊆ V_{2}. Suppose now that V_{1} ⊆ V_{2}. Assume that Q = (Q, Σ, ·) ∈ V_{1} is generated by a single state q_{0}, so that each state q ∈ Q is of the form q_{0}u, for some u ∈ Σ^{∗}. For each state q ∈ Q, let L_{q} denote the language accepted by Q with initial state q_{0} and single final state q. Since L_{q} ∈ V_{1} and V_{1} ⊆ V_{2}, there exists an automaton Q_{q} ∈ V_{2} accepting L_{q} with some initial state i_{q} and some set of final states F_{q}. Now the direct product of the Q_{q} contains a subautomaton that can be mapped homomorphically onto Q: take those tuples of the direct product accessible by a word from that tuple whose components are the respective initial states i_{q}. It follows that each state s = (s_{q})_{q∈Q} has a unique component s_{q} with s_{q} ∈ F_{q}, and that the map taking s to this component s_{q} is a homomorphism onto Q. Since V_{2} is closed with respect to direct product, subautomata and homomorphic images, it follows that Q is in V_{2}. If Q ∈ V_{1} is not generated by a single state, then Q is a quotient of the disjoint sum of its (maximal) one-generated subautomata. Since q-varieties are closed with respect to disjoint sum, it follows by the above argument that Q ∈ V_{2}. Finally, the fact that the assignment V ↦ V is surjective can be seen as follows. Given an l-variety V, consider the stream V of automata that only accept languages in V, so that Q = (Q, Σ, ·) ∈ V iff for each q_{0} ∈ Q and F ⊆ Q it holds that the language accepted by Q with initial state q_{0} and set of final states F is in V. Then V is a q-variety mapped to V. Indeed, the closure properties of V guarantee that V is a q-variety. Moreover, every language L ∈ Σ^{∗}V can be accepted by an automaton in V, namely the minimal automaton Q_{L} corresponding to L, since any language accepted by this automaton is a boolean combination of quotients of L. ■

Example 2.10 The l-variety corresponding to L is the variety L defined in Example 2.3. For each M, the l-variety corresponding to C_{M} is C_{M}.

Example 2.11 We call a finite automaton Q = (Q, Σ, ·) nilpotent if there is an integer n such that qu = qv holds for all words u, v ∈ Σ^{∗} of length ≥ n. (Note that the usual definition of nilpotent automata [8] requires that qu = q′v hold for all states q, q′ and words u, v ∈ Σ^{∗} of length at least n.) Nilpotent automata form a +-variety denoted N. The corresponding +-variety N of languages contains in Σ^{∗}N, for each alphabet Σ, all finite and cofinite languages in Σ^{∗}.

Example 2.12 A finite automaton Q = (Q, Σ, ·) is called definite if there exits some n ≥ 0 such that for all q ∈ Q and u, v ∈ Σ^{∗}, if the suffixes of u and v of length at most n agree, then qu = qv. (Again, the usual definition of definite automata [8] requires more.) For example, any shift register (Σ^{n}, Σ, ·) with u · a being the length n suffix of ua, for each u ∈ Σ^{n} and a ∈ A, is definite.

Definite automata form a +-variety D with corresponding +-variety of languages denoted D. We call D the +-variety of definite languages. For each Σ and L ⊆ Σ^{∗}, we have L ∈ Σ^{∗} iff there is an integer n ≥ 0 such that for all words u, v ∈ Σ^{∗} such that u and v have the same suffixes of length at most n, it holds that u ∈ L iff v ∈ L. (See [4].)

Example 2.13 A finite automaton Q is called aperiodic, or counter-free [4], if M(Q) (or S(Q)) contains only trivial subgroups. Aperiodic automata form a ∗-variety A with corresponding language variety A. We have that N ⊂ D ⊂ A and N ⊂ D ⊂ A.

3 Cascade product

We call a function τ : Σ^{∗} → Δ^{∗} sequential if τ preserves prefixes, i.e., for all words u and v in Σ^{∗}, if u ≤ v in the prefix order then τ(u) ≤ τ(v). It then follows that for each word u ∈ Σ^{∗} there is a (unique) function, in fact a sequential function τ_{u} : Σ^{∗} → Δ^{∗} with τ(uv) = τ(u)τ_{u}(v). If in addition τ preserves the length of the words, then we call τ a literal sequential function.

Sequential functions are known to be the functions inducible by sequential transducers, and literal sequential functions by Mealy automata [8], which are a restricted type of transducers. The (literal) sequential functions τ : Σ^{∗} → Δ^{∗} that can be induced by finite transducers obey the condition that the functions τ_{u}, u ∈ Σ^{∗} form a finite set. Such (literal) sequential functions are said to be of finite state. Note that any (literal) homomorphism is a finite state (literal) sequential function.

Suppose that Q = (Q, Σ, ·) is a finite automaton. A Mealy automaton [8] over Q is the extension of Q by an output alphabet Δ and an output function μ : Q × Σ → Δ. We let Q(Δ, μ) denote this extension. Clearly, each state q ∈ Q may be used to induce a finite state literal sequential function μ_{q} : Σ^{∗} → Δ^{∗} defined by μ_{q}(ϵ) = ϵ and μ_{q}(ua) = μ_{q}(u)μ(qu, a). We use Mealy automata extensions to define cascade products.

Suppose that Q = (Q, Σ, ·) and R = (R, Δ, ·) are finite automata and suppose that we are given a Mealy automaton extension Q(Δ, μ). Then the cascade product of Q with R determined by μ is defined to be the automaton Q ×_{μ} R = (Q × R, Σ, ·), where (q, r) · a = (qa, rμ(q, a)) = (qa, rμ_{q}(a)), for all q ∈ Q and r ∈ R. Note that it follows by induction that (q, r) · u = (qu, rμ_{q}(u)), for all u ∈ Σ^{∗}.

The semigroup theoretic concepts corresponding to the cascade product are the semi-direct product and the wreath product, cf. [4, 11]. The following fundamental fact is an adaptation of Straubing’s “wreath product principle” [3] to the cascade product.

Proposition 3.1 A language is recognized by a cascade product Q ×_{μ} R with initial state (q_{0}, r_{0}) iff it is a finite union of languages of the form K ∩ μ_{q_{0}}^{−1}(L), where K is a language recognized by Q with initial state q_{0} and L is a language recognized by R with initial state r_{0}.

The cascade product may be extended to q-varieties.

Definition 3.2 Suppose that V and W are q-varieties. The q-variety V ⋆ W is that generated by all cascade products Q ×_{μ} R with Q an automaton in ΣV, R an automaton in ΔW, and Q(Δ, μ) a Mealy automaton extension of Q.

It is immediate to prove that when both V and W are +-varieties (∗-varieties, respectively), then so is V ⋆ W.

The l-variety corresponding to V ⋆ W has the following description. The result is an adaptation of a similar characterization of languages recognizable by semigroups in the wreath product of two semigroup varieties, see [11].

Theorem 3.3 Suppose that V and W are q-varieties with corresponding lvarieties V and W. Then for each Σ, the l-variety V ⋆W corresponding to V⋆W contains exactly those languages in Σ^{∗} that are finite unions of languages of the form K ∩ μ^{−1}(L), where K ∈ Σ^{∗}V, L ∈ Δ^{∗}W and where μ : Σ^{∗} → Δ^{∗} is a sequential function induced by some state of a Mealy automaton extension of an automaton in V.

We may as well require that the same finite state literal sequential function μ appears in all terms of the finite union. Theorem 3.3 relies on on Proposition 3.1 and the following fact.

Theorem 3.4 For any q-varieties V and W and any Σ, an automaton Q is in Σ(V ⋆ W) iff Q is a quotient of a subautomaton of a cascade product R ×_{μ} S, where R ∈ ΣV and S ∈ ΔW such that and R(Δ, μ) is a Mealy automaton extension of R.

Proof. Let K denote the stream determined by those automata Q that can be constructed as quotients of subautomata of cascade products of automata R ∈ V and S ∈ W. It is clear that K ⊆ V ⋆ W. Also, K is easily shown to be closed with respect to subautomata, quotients, direct products and renaming. Moreover, K clearly contains all discrete automata. Hence, K is closed with respect to disjoint sum. It follows that V ⋆ W ⊆ K. ■

We say that a q-variety V is closed with respect to the cascade product if for any cascade product Q ×_{μ} R with Q, R ∈ V, it holds that Q ×_{μ} R ∈ V. For example, N, D, A are all closed with respect to the cascade product, cf. [4]. Moreover, for any set M of positive integers, C_{M} is closed with respect to the cascade product, as is any q-variety of autonomous automata.

We omit the straightforward proofs of the following facts.

Proposition 3.5 Any q-variety contained in L is closed with respect to the cascade product. If V and W are q-varieties such that V is contained in L and W is closed with respect to the cascade product, then V ⋆ W is also closed with respect to the cascade product.

Proposition 3.6 Suppose that {V_{i} : i ∈ I} is a directed set of q-varieties and V = ⋃_{i∈I} V_{i}. Then for any q-variety W, we have V ⋆ W = ⋃_{i∈I} V_{i} ⋆ W. Suppose that V_{i} denotes the l-variety corresponding to V_{i}, for each i ∈ I, and suppose that V denotes the l-variety corresponding to V. Then for any l-variety W, it holds that V ⋆ W = ⋃_{i∈I}(V_{i} ⋆ W).

Thus, the ⋆ operation is continuous in its first argument. In a similar way, it is continuous in its second argument.

As an immediate application of Proposition 3.6 we have that

C_{M} ⋆ V = ⋃_{d∈(M]} C_{d} ⋆ V

and

C_{M} ⋆ V = ⋃_{d∈(M]} C_{d} ⋆ V,

for all q-varieties V and l-varieties V, and for all M ⊆ Nat.

4 Varieties C_{M} ⋆ V

In this section, we study q-varieties of the form C_{d} ⋆ V and C_{M} ⋆ V, and the corresponding l-varieties C_{d} ⋆ V and C_{M} ⋆ V.

Definition 4.1 For any automaton Q = (Q, Σ, ·) and integer d > 0, let Q^{(d)} denote the automaton (Q, Σ^{(d)}, ·), where Σ^{(d)} consists of all letters ⟨u⟩, where u is any word of length d in Σ^{∗}, i.e., any element of Σ^{d}, and where

q · ⟨u⟩ = qu,

for all q ∈ Q and u ∈ Σ^{d}.

Thus, Q^{(d)} arises from Q by letting the words in Σ^{∗} of length d be the input letters. For each u ∈ Σ^{d}, the function induced by ⟨u⟩ in Q^{(d)} is the same as the function induced by u in the automaton Q. Besides Q^{(d)}, we will also use the automaton Q_{1}^{(d)}, which is the extension of Q^{(d)} by a letter a_{0} inducing the identity function Q → Q. Thus, Q_{1}^{(d)} = (Q, Σ^{(d)} ∪ {a_{0}}, ·), where q · a_{0} = q, for all q ∈ Q, and where for all q ∈ Q and u ∈ Σ^{d}, q · ⟨u⟩ is defined as above. Note that the monoids M(Q^{(d)}) and M(Q_{1}^{(d)}) are both isomorphic to the submonoid M_{d}(Q) of the monoid M(Q) of automaton Q consisting of all functions Q → Q induced by those words in Σ^{∗} whose length is a multiple of d.

Proposition 4.2 Each automaton Q is a homomorphic image of a cascade product of an automaton which is a direct product of a counter of length d with a shift register, and the automaton Q_{1}^{(d)}.

Proof. Suppose that Q = (Q, Σ, ·), so that Q_{1}^{(d)} is (Q, Σ^{(d)} ∪ {a_{0}}, ·) defined above.

Let C_{d} denote the counter of length d whose input alphabet is Σ and whose states are the integers in [d], so that i · a = i + 1 mod d, for all i ∈ [d] and a ∈ Σ. Let D_{d−1} denote the shift register of length d − 1 over Σ. Thus the states of D_{d−1} are the words in Σ^{d−1}, and the transition is defined so that for each u ∈ Σ^{d−1} and a ∈ Σ, state u · a is the suffix of ua of length d − 1. Define

μ : ([d] × Σ^{d−1}) × Σ → Σ^{(d)} ∪ {a_{0}}

by

μ((i, u), a) = \{ \begin{matrix}a_{0} & if i ≠ d − 1 \\ ⟨ua⟩ & otherwise. \end{matrix}

We thus obtain the cascade product Q′ = (C_{d} × D_{d−1}) ×_{μ} Q_{1}^{(d)}. We claim that there is a surjective homomorphism h : Q′ → Q. Indeed, for each state ((i, u), q) of Q′, define

((i, u), q)h = qv,

where v denotes the suffix of u of length i. In particular, ((0, u), q)h = q, for all u ∈ Σ^{d−1} and q ∈ Q, so that h is surjective. We show that h is a homomorphism. Assume that ((i, u), q) is a state of Q′ and a ∈ Σ. If i ≠ d − 1 then

((i, u), q)ah = ((i + 1, u′a), q)h
= qva
= (((i, u), q)h)a,

where v denotes the suffix of u of length i and u′ the suffix of u of length d − 1. When i = d − 1, we have

((d − 1, u), q)ah = ((0, u′a), qua)h
= qua
= (((d − 1, u), q)h)a,

where u′ is the same as above. ■

Remark 4.3 The same argument proves the following stronger version of Proposition 4.2. Suppose that R is a subautomaton of Q_{1}^{(d)} such that for each q ∈ Q there exists a state r ∈ R and a word u ∈ Σ^{∗} with |u| < d such that ru = q holds in Q. Then automaton Q is a homomorphic image of a cascade product of an automaton which is the direct product of a counter of length d with a shiftregister, and the automaton R. Indeed, if we replace Q_{1}^{(d)} with R in the above proof, the same argument works. The assumption that each q be of the form ru with r ∈ R and |u| < d is needed to show that h is surjective.

Recall that D denotes the +-variety of definite automata and that D denotes the corresponding +-variety of definite languages. Note that for any ∗-variety V of automata and for any automaton Q and d ≥ 1, we have Q^{(d)} ∈ V iff Q_{1}^{(d)} ∈ V.

Corollary 4.4 Suppose that V is a q-variety such that D ⋆ V ⊆ V. Then for any integer d ≥ 1 and automaton Q, if Q_{1}^{(d)} ∈ V then Q ∈ C_{d} ⋆ V.

We now want to prove a certain converse of the above result.

Proposition 4.5 Suppose that V is a ∗-variety of automata and d ≥ 1. If Q ∈ C_{d} ⋆ V, then Q^{(d)}, and thus Q_{1}^{(d)}, is in V.

Proof. First assume that Q is 1-generated, i.e., there exists a state q_{0} in Q such that each state is accessible from q_{0} by an input word. If Q ∈ C_{d} ⋆ V then, by Theorem 3.4, Q is a quotient of a subautomaton R′ of a cascade product of an automaton C in C_{d} and an automaton R in V. Since Q is 1-generated, without loss of generality we may assume that so is R′. But in that case C may be chosen to be 1-generated as well, so that C is a counter in C_{d} and is thus a quotient of a counter of length d. We conclude that Q is a homomorphic image, with respect to a homomorphism h, of a subautomaton R′ = (R′, Σ, ·) of a cascade product C_{d} ×_{μ} R, where C_{d} = ([d], Σ, ·) is the counter of length d with ia = i + 1 mod d, for all i ∈ [d] and a ∈ Σ, and R = (R, Δ, ·) is an automaton in V. For each i ∈ [d], let R_{i} denote the set of all states r ∈ R such that (i, r) ∈ R′. It is clear that R_{i} ≠ ∅. Moreover, let h_{i} : R_{i} → Q be defined by r ↦ h((i, r)), for all r ∈ R_{i}. We turn each R_{i} into an automaton R_{i} = (R_{i}, Σ^{(d)}, ·) with input letters in the set Σ^{(d)}. For each r ∈ R_{i} and u ∈ Σ^{d}, let r · ⟨u⟩ = rμ_{i}(u), the image of r with respect to the word which is the image of u with respect to the sequential function induced by state i of the Mealy extension C_{d}(Δ, μ). Since V is a ∗-variety and R ∈ V, it follows that each R_{i} is in V. Indeed, R_{i} can be constructed from R^{∗} by renaming and taking subautomata. Also, each h_{i} is a homomorphism R_{i} → Q^{(d)}, and since h is surjective, each state in Q appears as the image of some state in ⋃_{i∈[d]} R_{i}. Thus, the disjoint sum of the R_{i} can be mapped homomorphically onto Q^{(d)}, proving that Q^{(d)} is in V (since V is closed with respect to disjoint sum).

In the general case, Q is a quotient of the disjoint sum of its 1-generated subautomata Q_{1}, …, Q_{n}. If Q ∈ C_{d} ⋆ V then each Q_{i} belongs to C_{d} ⋆ V. Thus, by the above argument, we have Q_{i}^{(d)} ∈ V, for each i. Since V is closed with respect to disjoint sum, it follows that the disjoint sum of the Q_{i}^{(d)} is also in V. But Q^{(d)} is a quotient of this disjoint sum, so that Q^{(d)} ∈ V. ■

Call a q-variety V decidable if there is an algorithm to decide for any given automaton Q whether or not Q belongs to V. Similarly, call an l-variety V decidable if there is an algorithm to decide whether or not a regular language (given by an automaton or a regular expression) belongs to V. From Corollary 4.4 and Proposition 4.5 we have:

Theorem 4.6 For any ∗-variety V of automata with D ⋆ V ⊆ V, and for any d ≥ 1 and automaton Q, we have that Q ∈ C_{d} ⋆ V iff Q^{(d)} ∈ V. Thus, if V is decidable, then so is C_{d} ⋆ V.

A first characterization of the languages in the variety C_{d} ⋆ V, where V is any l-variety of languages, may be obtained from the wreath product principle. Let Σ denote an alphabet and consider the Σ-counter C_{d} = ([d], Σ, ·) with i · a = i + 1 mod d, for all i ∈ [d] and a ∈ Σ. Consider the alphabet [d] × Σ and the identity function π_{d} : [d] × Σ → [d] × Σ. Let σ_{d} denote the literal sequential function induced by the Mealy extension C_{d}([d] × Σ, π_{d}) in state 0. Then any literal sequential function σ : Σ^{∗} → Δ^{∗} induced by a state of a Mealy extension of an automaton in C_{d} can be factorized as the composite of σ_{d} with a literal homomorphism τ : ([d] × Σ)^{∗} → Δ^{∗}. Thus, by the wreath product principle we get:

Proposition 4.7 A language L ⊆ Σ^{∗} belongs to C_{d} ⋆ V iff L can be written as

L = ⋃_{i∈[d]}(Σ^{d})Σ^{i} ∩ σ_{d}^{−1}(K_{i}),

for some languages K_{i} ∈ ([d] × Σ)^{∗}V, i ∈ [d].

When V corresponds to a ∗-variety V with D ⋆ V ⊆ V, we can use Theorem 4.6 to derive an alternative characterization of the languages in C_{d} ⋆ V.

Suppose that L ⊆ Σ^{∗} and d ≥ 1. We define

L^{(d)} = {⟨u_{0}⟩ … ⟨u_{k−1}⟩ : u_{0} … u_{k−1} ∈ L, u_{i} ∈ Σ^{d}, i ∈ [k]},

so that L^{(d)} ⊆ (Σ^{(d)})^{∗}. Moreover, for each u ∈ Σ^{∗} with |u| < d, we define L^{(d,u)} = (Lu^{−1})^{(d)}. Thus, L^{(d)} and each L^{(d,u)} is a language in (Σ^{(d)})^{∗}, moreover, L^{(d)} = L^{(d,ϵ)}.

Theorem 4.8 Suppose that V is a ∗-variety of automata with D ⋆ V ⊆ V, and suppose that V denotes the language variety corresponding to V. Then for any integer d ≥ 1 and language L ⊆ Σ^{∗}, if L ∈ C_{d} ⋆ V then L^{(d,u)} ∈ V, for all u ∈ Σ^{∗} with |u| < d. Moreover, if L^{(d,u)} ∈ V, for all u ∈ Σ^{∗} with |u| < d, and if V is closed with respect to right (or left) concatenation with letters, then L ∈ C_{d} ⋆ V.

Proof. Suppose first that L ⊆ Σ^{∗} is in Σ^{∗}(C_{d} ⋆ V). Then L can be recognized by an automaton Q in C_{d} ⋆ V. By Theorem 4.6 we have that Q^{(d)} ∈ V. But each of the languages L^{(d,u)}, where u ∈ Σ^{∗} with |u| < d can be recognized by Q^{(d)}. For if L is recognized by Q = (Q, Σ, ·) with initial state q_{0} and final states F, then L^{(d,u)} is recognized by Q^{(d)} with initial state q_{0} and final states F_{u} = {q ∈ Q : qu ∈ F }. Thus, each L^{(d,u)} belongs to V.

Suppose now that each L^{(d,u)} belongs to V, for any u ∈ Σ^{∗} with |u| < d, so that each L^{(d,u)} can be recognized by some automaton Q_{u} in Σ^{(d)}V. For each u, let R_{u} = Q_{u} × (∪_{k∈[d]}Σ^{k}). We turn R_{u} into a Σ-automaton (R_{u}, Σ, ·) by defining, for each (q, v) ∈ R_{u} and a ∈ Σ,

(q, v) · a = \{ \begin{matrix}(q, va) & if |v| < d − 1 \\ q⟨va⟩ & otherwise. \end{matrix}

Let Q′_{u} = (q, ϵ), q ∈ Q_{u}. Then Q′_{u} determines a subautomaton of R_{u}^{(d)} which is isomorphic to Q_{u}. Moreover, (q, v) = (q, ϵ)v, for each (q, v) ∈ R_{u}. Thus, by Remark 4.3 and the assumption D ⋆ V ⊆ V, it follows that R_{u} belongs to C_{d} ⋆ V. Now for every u, the language L_{u} = (Lu^{−1}) ∩ (Σ^{d})^{∗} can be recognized by R_{u}, so that L_{u} ∈ C_{d} ⋆ V. Since L = ⋃_{u∈Σ^{∗}, |u|<d} L_{u}u, it follows now that L is in C_{d} ⋆ V. ■

Corollary 4.9 Under the assumption of Theorem 4.8, if V is decidable, then so is C_{d} ⋆ V.

Proof. This follows either from Theorem 4.8 or from Theorem 4.6. ■

Corollary 4.10 Suppose that M ⊆ Nat and V is a q-variety with corresponding l-variety V. Suppose that D ⋆ V ⊆ V and that V is closed with respect to right concatenation by letters. An automaton Q is in C_{M} ⋆ V iff there is some d ∈ (M] with Q^{(d)} ∈ V. Moreover, a language L ⊆ Σ^{∗} is in C_{M} ⋆ V iff there is some d ∈ (M] such that L^{(d,u)} ∈ V for each u ∈ Σ^{∗} with |u| < d.

5 Degree of aperiodicity

Following [1, 15], we call an automaton Q = (Q, Σ, ·) quasi-aperiodic if for each n, M(Q) (or S(Q)) contains no nontrivial group all of whose members can be induced by length n words. Thus, for any given n, the set of functions u^{Q}, where u is any word in Σ^{n} of length n, does not contain a nontrivial group. (In the terminology of [6], Q is quasi-aperiodic if no nontrivial group divides M(Q) in “equal lengths”. )

It is clear that any aperiodic automaton is quasi-aperiodic. On the other hand, a counter of length > 1 is quasi-aperiodic, but not aperiodic. Let QA denote the stream of quasi-aperiodic automata. The following theorem is a rephrasing of a result due to Barrington, Compton, Straubing and Therien. In its original formulation, the theorem involved the wreath product instead of the cascade product.

Theorem 5.1 (Barrington et al. [1]) QA = C ⋆ A. Thus QA is a q-variety.

It is a well-known consequence of the Krohn-Rhodes theorem [4, 15] that A ⋆ A ⊆ A, in fact equality holds. Thus, by Proposition 3.5, QA is also closed with respect to the cascade product. Moreover, since D ⊆ A, we have that D ⋆ A ⊆ A. Thus, by Theorem 4.6 we have:

Corollary 5.2 For any d ≥ 1 and automaton Q, we have Q ∈ C_{d} ⋆ A iff Q^{(d)} ∈ A.

Corollary 5.3 An automaton Q is quasi-aperiodic iff there is some integer d ≥ 1 such that Q^{(d)} is aperiodic.

Proof. If Q is quasi-aperiodic, then by Theorem 5.1, Q is in C ⋆ A. But since C is the union of the C_{n} where n is any positive integer, it follows that Q is in C_{d} ⋆ A, for some d ≥ 1. Thus, by Corollary 5.2, Q^{(d)} is in A, so that Q^{(d)} is aperiodic.

Assume now that Q^{(d)} is aperiodic, for some d ≥ 1. Then, by Corollary 5.2 and Theorem 5.1, Q is in C_{d} ⋆ A ⊆ QA. ■

Remark 5.4 Of course, it is possible to prove Corollary 5.3 without using Theorem 5.1 and Corollary 5.2. Assume that Q^{(d)} is aperiodic for some d ≥ 1. Then it cannot be the case that for some n, the set of all functions in M(Q) that can be induced by the length n words contains a nontrivial group G, since otherwise each element of G would be induced by a word of length dn, so that Q^{(d)} would not be aperiodic. The other direction can be verified by following the argument given in the proof of Theorem 5.10.

Proposition 5.5 Suppose that Q is an automaton such that both Q^{(m)} and Q^{(n)} are aperiodic, where m, n ≥ 1. If m and n are relative primes, then also Q is aperiodic.

Proof. If Q is not aperiodic, then M(Q) contains a cyclic subgroup G = {g_{0}, …, g_{p−1}} of prime order p > 1, where g_{0} = e denotes the unit. Unless g_{1}^{m} = e, it follows that each element of G can be induced by a word whose length is a multiple of m. (Indeed, if g_{1}^{m} = g_{i}, where i ≠ 0, then g_{i} can be induced by a word whose length is a multiple of m. Since g_{i} is a generator element of G, the same holds for any other group element.) But since Q^{(m)} is aperiodic, this is impossible. We conclude that g_{1}^{m} = e. In the same way, g_{1}^{n} = e. But then p divides both m and n, a contradiction. ■

Corollary 5.6 Suppose that Q is an automaton such that both Q^{(m)} and Q^{(n)} are aperiodic. If d denotes the g.c.d. of m and n, then Q^{(d)} is also aperiodic.

Corollary 5.7 An automaton Q is quasi-aperiodic iff there is a least integer d ≥ 1 such that Q^{(d)} is aperiodic. Moreover, for an integer n ≥ 1 we have that Q^{(n)} is aperiodic iff this integer d is a divisor of n.

Definition 5.8 The degree of aperiodicity, or aperiodicity degree of an automaton Q is the least integer d such that Q^{(d)} is aperiodic, if such an integer exists. Otherwise the degree of aperiodicity of Q is ∞.

Thus, by Corollary 5.7, the aperiodicity degree of Q is finite iff Q is quasiaperiodic.

For any set M of positive integers, we let QA_{M} denote the stream of automata whose aperiodicity degree is finite and belongs to (M]. In particular, A = QA_{{1}} = QA_{∅} and QA = QA_{Nat}. We also denote QA_{d} = QA_{{d}}, for each d ≥ 1.

Theorem 5.9 Suppose that M is a set of positive integers. Then QA_{M} = C_{M} ⋆ A. Thus, QA_{M} is a q-variety closed with respect to the cascade product.

Proof. Suppose that the aperiodicity degree d of automaton Q is finite and is contained in (M]. Then Q^{(d)} is aperiodic so that Q ∈ C_{d} ⋆ A, by Corollary 5.2. But C_{d} ⊆ C_{M}, so that Q ∈ C_{M} ⋆ A.

Suppose now that Q ∈ C_{M} ⋆ A. Then since C_{M} is the union of all varieties C_{d}, where d belongs to (M], it follows by Proposition 3.6 that Q ∈ C_{d} ⋆ A, for some such d. Thus, by Corollary 5.2, Q^{(d)} is aperiodic. But then the aperiodicity degree of Q divides d, so that it also belongs to (M]. ■

Theorem 5.10 There exists an algorithm to compute the aperiodicity degree of an automaton.

Proof. Barrington, Compton, Straubing and Therien showed in [1] how to decide for an automaton whether or not it belongs to QA. (See also [6].) Our result follows by a slight modification of their argument. Given Q = (Q, Σ, ·), successively compute the sets M_{=1}(Q), M_{=2}(Q), … until a repetition occurs, i.e., until M_{=m}(Q) = M_{=n}(Q), for some m < n. Here, we let M_{=m}(Q) denote the set of all functions Q → Q induced by the words in Σ^{m}. Then also M_{=m+r}(Q) = M_{=n+r}(Q), for all r ≥ 1. In particular, we have M_{=d}(Q) = M_{=d+n−m}(Q) for some m ≤ d < n such that n−m divides d. Thus, M_{=d}(Q) = M_{=2d}(Q), showing that M_{=d}(Q) is a subsemigroup of M(Q). In fact, M_{=d}(Q) is the semigroup of all functions inducible by words whose length is a positive multiple of d. If Q is quasi-aperiodic, then this semigroup contains no nontrivial group by definition. It follows that Q^{(d)} is aperiodic. Thus, to compute the aperiodicity degree of Q it suffices to find the least divisor d′ of d such that Q^{(d′)} is aperiodic. On the other hand, if M_{=d} does contain a nontrivial group, then Q is not quasiaperiodic and thus its aperiodicity degree is ∞. ■

Corollary 5.11 Suppose that it is decidable for an integer n whether n belongs to the division ideal generated by M. Then QA_{M} is decidable. In particular, if M is a recursive set and a division ideal, then QA_{M} is decidable.

Remark 5.12 The opposite direction is immediate: if QA_{M} is decidable then (M] is recursive.

Since QA_{M} is a q-variety, there is a corresponding l-variety that we denote by QA_{M}. We also denote QA_{{d}} by QA_{d}. In particular, QA_{{1}} = QA_{1} = A and QA_{Nat} = QA, the l-variety corresponding to QA. Since QA_{M} is the union of the QA_{d}, where d is any element of the division ideal (M] generated by M, also QA_{M} is the union of the QA_{d}, where d is any member (M]. The languages belonging to A have been characterized by Schützenberger as the star-free languages.

Theorem 5.13 (Schützenberger [13]) A language L ⊆ Σ^{∗} belongs to A iff L can be constructed from the finite subsets of Σ^{∗} by the operations of set union, complement and concatenation.

A similar characterization of languages in QA was obtained in [1].

Theorem 5.14 (Barrington, Compton, Straubing and Therien [1]) A language L ⊆ Σ^{∗} belongs to QA iff L can be constructed from the finite languages in Σ^{∗} and the languages (Σ^{d})^{∗}, d ≥ 1, by the operations of union, complement and concatenation.

In the rest of this section we prove a refinement of these results.

Theorem 5.15 Let M denote any subset of the set of positive integers. A language L ⊆ Σ^{∗} belongs to QA_{M} iff L can be constructed from the finite languages in Σ^{∗} and the languages (Σ^{m})^{∗}, where m ∈ M, by the operations of union, complement and concatenation.

In our argument, we will make use of the following characterization of QA_{d}, which is an immediate consequence of Theorem 4.8 and the fact that A is closed with respect to concatenation and contains the finite sets.

Corollary 5.16 For any integer d ≥ 1 and language L ⊆ Σ^{∗}, if L ∈ QA_{d} then L^{(d,u)} ∈ A, for all u ∈ Σ^{∗} with |u| < d. Moreover, if L^{(d,u)} ∈ A, for all u ∈ Σ^{∗} with |u| < d, then L ∈ QA_{d}.

Proof of Theorem 5.15. First note that any language (Σ^{d})^{∗}, where d is any member of the division ideal generated by M can be constructed from the finite languages and the languages (Σ^{m})^{∗}, m ∈ M by the operations of union, complement, and concatenation. This follows from the following two facts. If m_{1} and m_{2} are positive integers and m denotes their least common multiple (l.c.m.), then (Σ^{m})^{∗} = (Σ^{m_{1}})^{∗} ∩ (Σ^{m_{2}})^{∗}. Moreover, if d is a divisor of m, then for some finite F, (Σ^{d})^{∗} = (Σ^{m})^{∗}F. Thus, since QA_{M} = ⋃_{d∈(M]} QA_{d}, in the rest of the argument we may assume that M is itself a division ideal.

Suppose first that L ∈ QA_{M}. Since QA_{M} is the union of the QA_{m} with m ∈ M, there exists an integer d ∈ M with L ∈ QA_{d}. Thus, by Corollary 5.16, all the languages L^{(d,u)}, u ∈ Σ^{∗}, |u| < d are in A. By Schützenberger’s theorem, Theorem 5.13, it follows that each L^{(d,u)} with u ∈ Σ^{∗}, |u| < d can be constructed from the finite languages in (Σ^{(d)})^{∗} by using the operations of union, complement and concatenation. Hence, each language K_{u} = Lu^{−1} ∩ (Σ^{d})^{∗}, where u ∈ Σ^{∗} with |u| < d can be constructed from the finite languages in Σ^{∗} and the language (Σ^{d})^{∗} by the operations of union, complement and concatenation. (Take complement relatively to (Σ^{d})^{∗}.) Since L = ⋃_{u∈Σ^{∗}, |u|<d} K_{u}u, the same holds for L.

Suppose now that L can be constructed from the finite subsets of Σ^{∗} and the languages (Σ^{m})^{∗}, where m ∈ M by the operations of union, complement and concatenation. Let d denote the l.c.m. of those integers m for which (Σ^{m})^{∗} is used in the construction of L. If we can show that L^{(d,v)} belongs to A, for each v ∈ Σ^{∗} with |v| < d, then it follows by Corollary 5.16 that L ∈ QA_{d}, and thus that L ∈ QA_{M}. We will show that for each u, v ∈ Σ^{∗} with |u|, |v| < d, the language in (Σ^{(d)})^{∗}

L^{(d,u,v)} = {⟨x_{0}⟩ … ⟨x_{k−1}⟩ : k ≥ 0, ux_{0} … x_{k−1}v ∈ L}

is in A. Now this follows by a straightforward induction argument using Schützenberger’s theorem, Theorem 5.13, and the following facts. Let u, v ∈ Σ^{∗} with |u|, |v| < d, and let L, L_{1}, L_{2} ⊆ Σ^{∗}.

1. If L is finite, then so is L^{(d,u,v)}.

2. (L_{1} ∪ L_{2})^{(d,u,v)} = L_{1}^{(d,u,v)} ∪ L_{2}^{(d,u,v)}.

3. (L^{c})^{(d,u,v)} = (L^{(d,u,v)})^{c}.

4. If the length of each word in L_{1} is at least |u| and the length of each word in L_{2} is at least |v|, then (L_{1}L_{2})^{(d,u,v)} = ⋃_{|wz|=d} L_{1}^{(d,u,w)}⟨wz⟩L_{2}^{(d,z,v)}.

5. If the length of each word in L_{1} is less than |u| and the length of each word in L_{2} is at least |v|, then (L_{1}L_{2})^{(d,u,v)} = ⋃_{wz=u, w∈L_{1}} L_{2}^{(d,z,v)}.

6. If the length of each word in L_{1} is at least |u| and the length of each word in L_{2} is less than |v|, then (L_{1}L_{2})^{(d,u,v)} = ⋃_{zw=v, w∈L_{2}} L_{1}^{(d,u,z)}.

7. If the length of each word in L_{1} is less than |u| and the length of each word in L_{2} is less than |v|, then (L_{1}L_{2})^{(d,u,v)} is finite. ■

Corollary 5.17 Suppose that it is decidable for an integer whether it is contained in the division ideal generated by M. Then there exists an algorithm to decide for a regular language L ⊆ Σ^{∗} whether or not L can be constructed from the finite languages and the languages (Σ^{m})^{∗} with m ∈ M by the operations of union, complement and concatenation.

Remark 5.18 The converse of the above corollary is immediate. If there exists an algorithm to decide for a regular language L ⊆ Σ^{∗} whether or not L can be constructed from the finite languages and the languages (Σ^{m})^{∗} with m ∈ M by the operations of union, complement and concatenation, then (M] is a recursive set.

6 First-order logic

The expressive power of first-order logic on words with a unary predicate corresponding to each letter of the alphabet and < as the only numerical predicate was characterized by McNaughton and Papert [10]. We let FO[<] denote this logic. Thus, for any fixed alphabet Σ, the atomic formulas of FO[<] are the propositions P_{a}(x) and x < y, where a is any letter of Σ and x and y are variables. Formulas can be constructed from the atomic formulas by the boolean connectives ∨ and ¬, denoting disjunction and negation, and existential quantification. The other boolean connectives and universal quantification can be introduced as abbreviations. Free and bound variables are defined as usual. We may assume that no variable is bound two or more times in a formula, or in a finite set of formulas, and that any free variable is different from any bound variable. Below we will denote syntactic equality by ≡.

Suppose that φ is a formula with free variables in X, and suppose that w ∈ Σ^{∗} and λ : X → [|w|], i.e., λ maps variables in X to “positions” in w. We say that (w, λ) satisfies φ, denoted (w, λ) ⊧ φ, if • φ ≡ P_{a}(x) and the letter in w at position x is a, or

• φ ≡ x < y and xλ < yλ, or

• φ ≡ φ_{1} ∨ φ_{2} and (w, λ) ⊧ φ_{1} or (w, λ) ⊧ φ_{2}, or

• φ ≡ ¬ψ and (w, λ) |̸= ψ, or

• φ ≡ (∃x)ψ and there exists a function λ′ : X ∪ {x} → [|w|] which agrees with λ on X such that (w, λ′) ⊧ ψ. (Here, by our conventions, we may assume without loss of generality that x ∉ X.)

When X is empty, so that φ is a sentence, i.e., φ has no free variables, we just write w ⊧ φ and call {w ∈ Σ^{∗} : w ⊧ φ} the language defined by φ. Moreover, we say that a language L ⊆ Σ^{∗} is definable in FO[<] if there is a sentence φ which defines L.

As before, we let A denote the ∗-variety of aperiodic automata, and let A denote the corresponding ∗-variety of languages.

Theorem 6.1 (McNaughton and Papert [10]) A language L ⊆ Σ^{∗} is definable in FO[<] iff L ∈ Σ^{∗}A.

We refer the reader to [10], and in particular to [15], for detailed proofs of Theorem 6.1.

Subsequently, Barrington, Compton, Straubing and Therien [1] considered the extension of first-order logic by atomic propositions of the form C_{d}^{r}(x), d ≥ 1, r ∈ [d] meaning that position x in the word satisfies x ≡ r mod d. Thus, using the above notations, (w, λ) ⊧ C_{d}^{r}(x) if and only if xλ is congruent to r mod d. Since this logic is equivalent to the extension of FO[<] by all regular numerical predicates, see [14], we denote it by FO[R]. As before, let QA denote the l-variety corresponding to the q-variety QA of quasi-aperiodic automata.

Theorem 6.2 (Barrington et al. [1]) A language L ⊆ Σ^{∗} is definable in FO[R] iff L ∈ Σ^{∗}QA.

For an integer d ≥ 1 let FO[d] denote the fragment of FO[R] where only atomic propositions associated to the letters of the alphabet and propositions of the form x < y and C_{d}^{r}(x) are allowed. (It would be sufficient to allow only x < y and C_{d}^{0}(x).) Moreover, for a set M of the positive integers, let FO[M] denote the union of the FO[d] with d ∈ M. Thus, FO[R] = FO[Nat] and FO[<] = FO[∅] = FO[1].

Below we will write x ≤ y as abbreviation for ¬(y < x), x = y + 1 for x < y ∧ ¬(∃z)(x < z ∧ z < y), Last(x) for (∀y)(y ≤ x), True for φ ∨ ¬φ, where φ is a fixed sentence, and False for ¬True.

Proposition 6.3 A language L ⊆ Σ^{∗} is definable in FO[M] iff L is definable in FO[(M]].

Proof. This follows by the following two observations.

1. If d is a divisor of m, say dk = m, then C_{d}^{0}(x) can be expressed as C_{m}^{0}(x)∨ C_{m}^{d}(x) ∨ … C_{m}^{d(k−1)}(x). Moreover, for every r ∈ [d], C_{m}^{r+1}(x) can be expressed by (∃y)(x = y + 1 ∧ C_{m}^{r}(y)).

2. If m_{1}, m_{2} ≥ 1 and m denotes the l.c.m. of m_{1} and m_{2}, then C_{m}^{0}(x) can be expressed as C_{m_{1}}^{0}(x) ∧ C_{m_{2}}^{0}(x). ■

By our previous results we can prove the following common extension of Theorems 6.1 and 6.2.

Theorem 6.4 Suppose that M is any set of the positive integers. Then a language L ⊆ Σ^{∗} is definable in FO[M] iff L ∈ Σ^{∗}QA_{M}.

The proof of Theorem 6.4 will be completed at the end of the section.

Proposition 6.5 Suppose that L ⊆ Σ^{∗} and d ≥ 1. If L^{(d)} is definable in FO[<], then L ∩ (Σ^{d})^{∗} is definable in FO[d].

Proof. First we prove that for all φ ∈ FO[<] with free variables in X there exists some φ′ ∈ FO[d] with free variables in X such that for all w ∈ (Σ^{(d)})^{∗} and λ : X → [|w|],

(w, λ) ⊧ φ iff (wh, κ) ⊧ φ′,

where h denotes the homomorphism (Σ^{(d)})^{∗} → Σ^{∗} defined by ⟨u⟩ ↦ u, for all u ∈ Σ^{d}, and where xκ = d(xλ), the product of the integers d and xλ, for all x ∈ X. We prove this claim by induction on the structure of φ.

• φ ≡ P_{⟨u⟩}(x), where u = a_{0} … a_{d−1}. Then, writing x_{d−1} for x, we define

φ′ ≡ (∃x_{0}) … (∃x_{d−2}) [ ⋀_{j=0}^{d−2} x_{j+1} = x_{j} + 1 ∧ ⋀_{j=0}^{d−1} P_{a_{j}}(x_{j})] .

• φ ≡ x < y. Then φ′ ≡ x < y.

• φ ≡ φ_{1} ∨ φ_{2}. Then φ′ ≡ φ′_{1} ∨ φ′_{2}.

• φ ≡ ¬φ_{1}. Then φ′ ≡ ¬φ′_{1}.

• φ ≡ ∃xφ_{1}, Then φ′ ≡ (∃x)(C_{d}^{0}(x) ∧ φ′_{1}).

We now complete the proof of Proposition 6.5. Suppose that L^{(d)} is defined by sentence φ in FO[<]. Then L ∩ (Σ^{d})^{∗} is defined by φ′ ∧ (∀x)(Last(x) → C_{d}^{0}(x)).

■

Corollary 6.6 Suppose that L ⊆ Σ^{∗} and d ≥ 1. If L^{(d,u)} is definable in FO[<] for all u ∈ Σ^{∗} with |u| < d, then L is definable in FO[d].

Proof. For each u ∈ Σ^{∗} with |u| < d we have that L^{(d,u)} = (Lu^{−1})^{(d)}. By Proposition 6.5, it follows that if L^{(d,u)} is definable in FO[<], then K_{u} = Lu^{−1}∩ (Σ^{d})^{∗} is definable in FO[d], for each u ∈ Σ^{∗}, |u| < d. But then, using the formula L = ⋃_{u∈Σ^{∗}, |u|<d} K_{u}u, it follows easily that L is definable in FO[d]. Indeed, if K_{u} is defined by φ_{u}, where u = a_{0} … a_{n−1} ∈ Σ^{∗} with |u| = n < d, then K_{u}u is defined by the formula ψ_{u}

(∃x_{0}) … (∃x_{n−1}) [ ⋀_{i=0}^{n−2} x_{i+1} = x_{i} + 1 ∧ ⋀_{i=0}^{n−1} P_{a_{i}}(x_{i}) ∧ Last(x_{n−1}) ∧ φ_{u}[< x_{0}]] ,

where φ_{u}[< x_{0}] is the relativization of φ_{u} defined in the usual manner [15]. Finally, L is defined by ⋁_{u∈Σ^{∗}, |u|<d} ψ_{u}. ■

Proposition 6.7 If L ⊆ Σ^{∗} is definable in FO[d], then L^{(d)} is definable in FO[<].

Proof. We prove the following claim. For all φ in FO[d] with free variables in X and for all functions ρ : X → [d] there exists a formula φ′_{ρ} ∈ FO[<] with free variables in X such that for all words w ∈ (Σ^{(d)})^{∗} and functions λ : X → [|w|],

(w, λ) ⊧ φ′_{ρ} iff (wh, κ_{ρ}) ⊧ φ,

where h denotes the homomorphism (Σ^{(d)})^{∗} → Σ^{∗} given by ⟨u⟩ ↦ u, for all u ∈ Σ^{d}, and where xκ_{ρ} = (xλ)d + xρ, for all x ∈ X. We prove this claim by induction on the structure of φ.

• φ ≡ P_{a}(x). Then φ′_{ρ} is the disjunction of all of the P_{⟨u⟩}(x) such that the letter of u on the (xρ)th position is a.

• φ ≡ x < y. Then

φ′_{ρ} ≡ \{ \begin{matrix}x < y & if xρ ≥ yρ \\ x ≤ y & if xρ < yρ. \end{matrix}

• φ ≡ C_{d}^{r}(x). Then

φ′_{ρ} ≡ \{ \begin{matrix}True & if xρ = r \\ False & if xρ ≠ r. \end{matrix}

• φ ≡ φ_{1} ∨ φ_{2}. Then φ′_{ρ} = (φ′_{1})_{ρ} ∨ (φ′_{2})_{ρ}.

• φ ≡ ¬ψ. Then φ′_{ρ} = ¬ψ′_{ρ}.

• φ ≡ (∃x)ψ. Here we may assume that x is not in the set X. For each i ∈ [d], let ρ[x ↦ i] denote that function X ∪ {x} → [d] which agrees with ρ on X and such that xρ = i. Then we define

φ′_{ρ} ≡ (∃x) ⋁_{i∈[d]} ψ′_{ρ[x↦i]}.

We now complete the proof of Proposition 6.7. Suppose that L ⊆ Σ^{∗} is defined by the sentence φ in FO[d]. Let φ′ be the corresponding sentence of FO[<] defined above. Then for all w ∈ (Σ^{(d)})^{∗},

w ⊧ φ′ iff wh ⊧ φ.

(Note that ρ is the empty function.) Thus, φ′ defines L^{(d)}. ■

Corollary 6.8 If L ⊆ Σ^{∗} is definable in FO[d] then for each u ∈ Σ^{∗} with |u| < d, L^{(d,u)} is definable in FO[<].

Proof. Use the fact that L^{(d,u)} = (Lu^{−1})^{(d)} and that if L is definable in FO[d], then so is Lu^{−1}. ■

We are now in the position to complete the proof of Theorem 6.4.

Proof of Theorem 6.4. By Corollaries 6.6 and 6.8, a language L ⊆ Σ^{∗} is definable in FO[d] iff L^{(d,u)} is definable in FO[<], for each u ∈ Σ^{∗} with |u| < d. Thus, by the theorem of McNaughton and Papert, Theorem 6.1, and by Corollary 5.16, L is definable in FO[d] iff L ∈ QA_{d}. Since a language is definable in FO[M] iff it is definable in FO[d], for some d in the division ideal generated by M, and since QA_{M} is the union of the QA_{d} where d is any integer in the division ideal generated by M, the result follows. ■

Corollary 6.9 Suppose that membership in the division ideal generated by M is decidable. Then it is decidable for a regular language L whether or not L can be defined in FO[M].

Again, the converse direction holds obviously.

7 Temporal logic

The language LTL of Linear (Propositional) Temporal Logic [12] over an alphabet Σ has, as atomic formulas (or atomic propositions), the propositional constants p_{a} associated with the letters a ∈ Σ. Formulas can be constructed from the atomic formulas by the boolean connectives ∨ and ¬, and the modalities X (next) and U (until). Other boolean connectives may be introduced as usual. Suppose that u ∈ Σ^{∗} and that φ is a formula. We say that u satisfies φ, denoted u ⊧ φ, if

1. φ ≡ p_{a} and u = av, for some a ∈ Σ and v ∈ Σ^{∗}, or

2. φ ≡ φ_{1} ∨ φ_{2}, for some φ_{1} and φ_{2}, and u ⊧ φ_{1} or u ⊧ φ_{2}, or

3. φ ≡ ¬ψ, for some formula ψ, and it is not the case that u ⊧ ψ, or

4. φ ≡ φ_{1}Uφ_{2}, for some φ_{1} and φ_{2}, and there exist v, w ∈ Σ^{∗} such that u = vw, w ⊧ φ_{2}, moreover, z ⊧ φ_{1} for all suffixes z of u properly including w.

In this section we study the extension of LTL by counting. Suppose that M ⊆ Nat. For an alphabet Σ, the atomic formulas of LTL[M] are those of LTL together with an additional propositional constant lg_{d,r}, for each d ∈ M and r ∈ [d]. Formulas are constructed from the atomic formulas as above, so that if φ and ψ are formulas, then so are φ ∨ ψ, ¬φ, Xφ and φUψ. For all d ∈ M and r ∈ [d], we define u ⊧ lg_{d,r} iff the length of u is congruent to r modulo d. The semantics of the other constructs of LTL[M] are defined as above. When M is the division ideal generated by d, we write just LTL[d] for LTL[M]. Note that LTL[1] is just LTL, as is LTL[∅].

We say that a language L ⊆ Σ^{∗} is definable in LTL[M] if there is a formula φ of LTL[M] (with propositional constants corresponding to the letters of Σ) such that L = L_{φ} = {u ∈ Σ^{∗} : u ⊧ φ}.

Example 7.1 For any m, n > 0 and u ∈ Σ^{∗}, we have that u ⊧ lg_{m,0} and u ⊧ lg_{n,0} iff u ⊧ lg_{k,0}, where k denotes the least common multiple of m and n. Moreover, u ⊧ lg_{m,r}, for r ∈ [m], iff u ⊧ X^{r}lg_{m,0}, where X^{r} is X … X with X appearing r times. Also, if n divides m, then u ⊧ lg_{n,0} iff u ⊧ ⋁_{i∈[m/n]} lg_{m,in}.

By the above example, we have that LTL[M] is as exactly as expressive as LTL[(M]], i.e., a language is definable in LTL[M] iff it is definable in LTL[(M]]. Moreover, when M is not empty, then a language is definable in LTL[M] iff it is definable in LTL[d], for some d ∈ (M].

The logic LTL[M] allows for several counting versions of the until modality. For any formulas φ and ψ, and for any d ∈ M and r ∈ [d], define φU^{(d,0)}ψ to be the formula

⋁_{i∈[d]}[lg_{d,i} ∧ (φU(ψ ∧ lg_{d,i}))],

and define φU^{(d,r)}ψ, r > 0 as

φ ∧ Xφ ∧ … ∧ X^{r−1}φ ∧ X^{r}(φU^{(d,0)}ψ).

We then have u ⊧ φU^{(d,r)}ψ iff u has a decomposition u = vw such that w ⊧ ψ, |v| is congruent to r modulo d, moreover, for all x, z with xz = u such that w is a proper suffix of z, it holds that z ⊧ φ.

A second counting version of the until modality can now be defined as follows. For all φ, ψ and d, r as before, let φU_{1}^{(d,0)}ψ be the formula

⋁_{i∈[d]}[lg_{d,i} ∧ (¬lg_{d,i} ∨ φ)U^{(d,0)}ψ)].

Moreover, when r > 0, let φU_{1}^{(d,r)}ψ be the formula

φ ∧ Xφ ∧ … ∧ X^{r−1}φ ∧ X^{r}(φU_{1}^{(d,0)}ψ).

We now have u ⊧ φU^{(d,r)}ψ, for u a word in Σ^{∗}, iff u has a decomposition u = vw such that w ⊧ ψ, |v| is congruent to r modulo d, moreover, for all x, z with xz = u such that w is a proper suffix of z and |x| is congruent to r modulo d, it holds that z ⊧ φ.

A last version of until involves several formulas. Suppose, as before, that d ∈ M, and suppose that φ_{0}, …, φ_{d−1}, ψ are formulas of LTL[M]. We define (φ_{0}, …, φ_{d−1})U_{2}^{(d,0)}ψ as the formula

⋁_{i∈[d]}[lg_{d,i} ∧ ((¬lg_{d,i} ∨ φ_{i})U^{(d,0)}ψ)]

Thus, for all words u ∈ Σ^{∗}, we have u ⊧ (φ_{0}, …, φ_{d−1})U_{2}^{(d,0)}ψ iff u has a decomposition u = vw such that w ⊧ ψ, |v| is congruent to r modulo 0, moreover, for all x, z and i ∈ [d] with xz = u such that w is a proper suffix of z and |x| is congruent to i modulo d, it holds that z ⊧ φ_{i}. The modalities U^{(d,r)} with r ∈ [d], r ≠ 0, which have a similar semantics, can be introduced in the obvious way. Of course, the propositional constants lg_{d,r} can in turn be defined using either version of until.

Remark 7.2 The last version of until shows that the extension of LTL by counting fits in the framework of Wolper’s extension of temporal logic by grammar (or finite automaton) operators, cf. [21, 20].

We introduce several abbreviations. First, let True = p_{a} ∨ ¬p_{a}, where a is any letter in Σ, and let False = ¬True. Moreover, let End denote the formula ⋀_{a∈Σ} ¬p_{a}, so that for all u ∈ Σ^{∗}, we have u ⊧ End iff u = ϵ. Finally, for any formula φ, let ⟨⟩^{(d,r)}φ stand for True U^{(d,r)}φ and □^{(d,r)}φ for ¬⟨⟩^{(d,r)}¬φ. The modalities ⟨⟩ and □ are defined as usual.

Example 7.3 Let Σ = {a, b}. If φ is the formula ⟨⟩^{(2,0)}End, then L_{φ}, the language defined by φ is (Σ^{2})^{∗}. Moreover, if ψ ≡ p_{a}U^{(2,0)}(□p_{b}), then L_{ψ} is the language (a^{2})^{∗}b^{∗}.

In his thesis [9], Kamp proved that temporal logic with past and future modalities is expressively complete in the sense that it can express every first-order property of words. Subsequently, it has been shown in [7] that future (or past) modalities alone suffice. An algebraic proof of this result, based on the Krohn-Rhodes decomposition theorem for finite semigroups and automata [4, 15], was later given by Cohen, Perrin and Pin in [3]. However, the simplest proof to date is the one found by Th. Wilke, cf. [19].

Theorem 7.4 (Kamp [9], Gabbay et al. [7]) A language L ⊆ Σ^{∗} is definable in LTL iff L is definable in FO[<].

Hence, L is definable in LTL iff L is in A. Our aim is to prove the following counting version of Kamp’s theorem.

Theorem 7.5 Suppose that M is a division ideal. Then a language L ⊆ Σ^{∗} is definable in LTL[M] iff L is definable in FO[M].

In our proof of Theorem 7.5, we will use:

Proposition 7.6 Suppose that L ⊆ Σ^{∗}, d ≥ 1 and v ∈ Σ^{∗} with |v| < d. If L^{(d,v)} is definable in LTL, then L ∩ (Σ^{d})^{∗}v is definable in LTL[d].

Proof. First we show that for every formula φ of LTL there is a formula φ′ of LTL[d] such that for all words w ∈ (Σ^{(d)})^{∗} it holds that w ⊧ φ iff (wh)v ⊧ φ′, where h denotes the homomorphism (Σ^{(d)})^{∗} → Σ^{∗} defined by ⟨w⟩ ↦ w, all w ∈ Σ^{d}. We construct φ′ by induction.

• φ ≡ p_{⟨u⟩}, where u = a_{0} … a_{d−1}. Then

φ′ ≡ p_{a_{0}} ∧ Xp_{a_{1}} ∧ … ∧ X^{d−1}p_{a_{d−1}},

where X^{n}φ is X … Xφ with X appearing n times.

• φ ≡ φ_{1} ∨ φ_{2}. Then φ′ ≡ φ′_{1} ∨ φ′_{2}.

• φ ≡ ¬ψ. Then φ′ ≡ ¬ψ′.

• φ ≡ Xψ. Then φ′ ≡ X^{d}ψ′.

• φ ≡ φ_{1}Uφ_{2}. Then φ′ ≡ φ′_{1}U_{1}^{(d,0)}φ′_{2}.

Suppose now that L^{(d,v)} is defined by φ. Then the formula

φ′ ∧ ⟨⟩^{(d,0)}(p_{a_{0}} ∧ Xp_{a_{1}} ∧ … ∧ X^{i−1}p_{a_{i−1}} ∧ X^{i}End)

defines L∩(Σ^{d})^{∗}v, where v = a_{0} … a_{i−1} and φ′ denotes the formula constructed above. ■

Corollary 7.7 Suppose that L ⊆ Σ^{∗} and d ≥ 1. If L^{(d,u)} is definable in LTL, for each u ∈ Σ^{∗} with u ∈ Σ^{∗}, |u| < d, then L is definable in LTL[d].

We are now ready to prove Theorem 7.5.

Proof of Theorem 7.5. It is well-known that temporal logic can be embedded in first order logic: any language definable in LTL is definable in FO[<]. The proof goes by formula induction, essentially by formalizing the definition of the semantics of LTL. It is easy to show in the same way that any language definable in LTL[M] is definable in FO[M].

Suppose now that L is definable in FO[M]. Then L is definable in FO[d], for some d ∈ M. Thus, by Corollary 6.8, L^{(d,u)} is definable in FO[<], for each u ∈ Σ^{∗} with |u| < d. Thus, by Theorem 7.4 and Corollary 7.7, L is definable in LTL[d], hence in LTL[M]. ■

8 Summary and future results

Our main results can be summarized in a single statement that establishes the equivalence between four descriptions of the same class of languages.

Corollary 8.1 Suppose that M is a set of the positive integers. The following conditions are equivalent for a language L ⊆ Σ^{∗}:

1. L can be constructed from the finite subsets of Σ^{∗} and the languages (Σ^{m})^{∗}, where m ∈ M, by the Boolean operations and concatenation.

2. L can be defined by a formula of LTL[M].

3. L can be defined by a formula of FO[M].

4. L can be accepted by a finite automaton whose degree of aperiodicity belongs to (M] (or equivalently, the minimal automaton accepting L is finite with aperiodicity degree contained in (M]).

As mentioned above, this result is a common extension of those obtained in [1, 7, 9, 10, 13]. In fact, we have shown that Corollary 8.1 is easily derivable from the classical results of Schützenberger [13], McNaughton and Papert [10], Kamp [9] and Gabbay et al. [7], using Corollary 4.10, which is in turn based on Theorem 4.8 and Theorem 4.6. (Of course, it is possible to prove Corollary 4.10 without using Theorem 4.6.)

Some of the implications of Corollary 8.1 are quite obvious. It is clear that the second condition implies the third as does the first. The fact that the second condition implies the first can be proved by generalizing an argument from [3] which concerns the case when M is empty. That the third condition implies the fourth can also be shown directly using Ehrenfeucht-Fraisse games, following the usual argument establishing the fact that any language definable in FO has an aperiodic syntactic monoid. In the classical case, i.e., when M = ∅, there are two different direct arguments in the literature establishing that the last condition implies the second. The first argument is based on (a weak form of) the Krohn-Rhodes decomposition theorem, and can be found in [3]. A more elementary argument is given in [19]. Both arguments can be generalized to any given set M of moduli.

Theorem 4.8 and Theorem 4.6 are also very useful in the characterization of the expressive power of other variants of first-order and temporal logic. Various fragments of LTL have been studied in [3] and [19]. In a forthcoming paper, we will characterize the expressive power of the extension of most of these fragments by counting. In [15, 16], the expressive power of first-order logic with modular quantifiers with respect to any given set of moduli has been characterized, as well as the expressive power of first-order logic with modular quantifiers and the predicates C_{m}^{r}(x), where m is any positive integer and r ∈ [m]. Using Theorem 4.8 and Theorem 4.6, we can give a characterization of the expressive power of the extension of first-order logic with any collection of modular quantifiers and any collection of predicates C_{m}^{r}(x). A further natural research topic is to extend these results to ω-languages.

9 Acknowledgments

The first author would like to thank the members of the Department of Mathematics of Kyoto Sangyo University and the members of the DSS group of the Department of Computer Science of Aalborg University for their hospitality.

References

[1] D. A. M. Barrington, K. Compton, H. Straubing and D. Therien, Regular languages in NC^{1}, J. Comput. Sys. Sci., 44(1992), 478–499.

[2] R. Büchi, Weak second-order arithmetic and finite automata, Z. Math. Logik Grundlag. Math., 6(1960), 66–92.

[3] J. Cohen, D. Perrin and J.-E. Pin, On the expressive power of temporal logic, J. Comp. Sys. Sci., 46(1993), 271–294.

[4] S. Eilenberg, Automata, Languages and Machines, v. A and B., Academic Press, 1974 and 1976.

[5] C. C. Elgot, Decision problems of finite automata design and related arithmetics. Trans. Amer. Math. Soc., 98(1961), 21–51.

[6] Z. Ésik, Results on homomorphic representation of automata by α_{0}- products, Theoret. Comp. Sci., 87(1991), 229-249.

[7] D. M. Gabbay, A. Pnueli, S. Shelah and J. Stavi, On the temporal analysis of fairness, in: proc. 12th ACM Symp. Principles of Programming Languages, Las Vegas, 1980, 163–173.

[8] F. Gécseg and I. Peák, Algebraic Theory of Automata, Akadémiai Kiadó, Budapest, 1972.

[9] J. A. Kamp, Tense Logic and the Theory of Linear Order, Ph. D. Thesis, UCLA, 1968.

[10] R. McNaughton and S. Papert, Counter-Free Automata, MIT Press, 1971.

[11] J.-E. Pin, Varieties of Formal Languages, North Oxford Academic, 1986.

[12] A. Pnueli, The temporal logic of programs, in: proc. 18th IEEE Symp. Foundations of Computer Science, Providence, RI, 1977, 46–57.

[13] M. P. Schützenberger, On finite monoids having only trivial subgroups, Inform. Comp., 8(1965), 190–194.

[14] H. Straubing, Constant-depth periodic circuits, Int. J. Algebra and Computation, 1(1991), 45–88.

[15] H. Straubing, Finite Automata, Formal Logic and Circuit Complexity, Birkhauser, 1994.

[16] H. Straubing, D. Therien and W. Thomas, Regular languages defined with generalized quantifiers, Information and computation, 118(1995), 289–301.

[17] W. Thomas, Automata on infinite objects, in: Handbook of Theoretical Computer Science, Vol. B, Elsevier, Amsterdam, 1990, 133–191.

[18] W. Thomas, Languages, automata, and logic, in: Handbook of Formal Language Theory, Vol. III, (G. Rozenberg, A. Salomaa, Eds.), Springer-Verlag, New York, 1997, 389-455.

[19] Th. Wilke, Classifying discrete temporal properties, in: proc. STACS 99, Trier, 1999, LNCS 1563, Springer, 1999, 32–46.

[20] M. Y. Vardi and P. Wolper, Reasoning about infinite computation, Information and Computation, 115(1994), 1–37.

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

Recent BRICS Report Series Publications

RS-01-53 Zoltán Ésik and Masami Ito. Temporal Logic with Cyclic Counting and the Degree of Aperiodicity of Finite Automata. December 2001. 31 pp.

RS-01-52 Jens Groth. Extracting Witnesses from Proofs of Knowledge in the Random Oracle Model. December 2001. 23 pp.

RS-01-51 Ulrich Kohlenbach. On Weak Markov’s Principle. December 2001. 10 pp.

RS-01-50 Jiří Srba. Note on the Tableau Technique for Commutative Transition Systems. December 2001. To appear in the proceedings of FOSSACS ’02.

RS-01-49 Olivier Danvy and Lasse R. Nielsen. A First-Order One-Pass CPS Transformation. 2001. Extended version of a paper to appear in the proceedings of FOSSACS ’02.

RS-01-48 Mogens Nielsen and Frank D. Valencia. Temporal Concurrent Constraint Programming: Applications and Behavior. December 2001. 36 pp.

RS-01-47 Jesper Buus Nielsen. Non-Committing Encryption is Too Easy in the Random Oracle Model. December 2001. 20 pp.

RS-01-46 Lars Kristiansen. The Implicit Computational Complexity of Imperative Programming Languages. November 2001. 46 pp.

RS-01-45 Ivan B. Damgård and Gudmund Skovbjerg Frandsen. An Extended Quadratic Frobenius Primality Test with Average Case Error Estimates. November 2001. 43 pp.

RS-01-44 M. Oliver Möller, Harald Rueß, and Maria Sorea. Predicate Abstraction for Dense Real-Time Systems. November 2001. 27 pp.

RS-01-43 Ivan B. Damgård and Jesper Buus Nielsen. From Known-Plaintext Security to Chosen-Plaintext Security. November 2001. 18 pp.

RS-01-42 Zoltán Ésik and Werner Kuich. Rationally Additive Semirings. November 2001. 11 pp.

RS-01-41 Ivan B. Damgård and Jesper Buus Nielsen. Perfect Hiding and Perfect Binding Universally Composable Commitment Schemes with Constant Expansion Factor. October 2001. 43 pp.