We provide a Myhill-Nerode-like theorem that characterizes the class of data languages recognized by deterministic nite-memory automata (DMA). As a byproduct of this characterization result, we obtain a canonical representation for any DMA-recognizable language. We then show that this canonical automaton is minimal in a strong sense: it has the minimal number of control states and also the minimal amount of internal storage.
Automata processing words and trees over in nite alphabets are attracting signi cant interest from the database and veri cation communities, since they can be often used as low-level formalisms for representing and reasoning about data streams, program traces, and serializations of structured documents. Moreover, properties speci ed using high-level formalisms (for instance, within suitable fragments of rst-order logic) can be often translated into equivalent automatonbased speci cations, easing, in this way, the various reasoning tasks.
Di erent models of automata which process words over in nite alphabets
have been proposed and studied in the literature (see, for instance, the surveys
[
Example 1. Consider the automaton from Figure 1. We have used an intuitive notation in the gure { a more precise syntax is given in Section 2. An edge labeled with g ⇒ a where, g is a guard (precondition) and a an action (postcondition); both g and a refer to the current symbol as x, and the ith register as ri. This accepts exactly the data words w such that there are an even number of places n ≤ SwS with w(n) ≠ w(n − 1).
store x in r1
Tuesday, 6 April 2010
One could hope that most of the fundamental results in standard (i.e.,
nitestate) automata theory can be carried on in the setting of words over in nite
alphabets. However, prior work has shown that many elementary closure and
decision properties of nite automata are absent in the in nite-alphabet case.
For example, the equivalence of the non-deterministic and deterministic variants
of automata is known to fail for both memory automata and pebble automata
[
Among several paradigmatic problems in automata theory, a crucial one, for
both theoretical and practical reasons, is certainly the minimization problem.
Roughly speaking, it consists of determining the automaton-based
representation that uses the \smallest space" for a given language. In the case of standard
nite-state automata, minimal space usage is usually translated in terms of the
minimum number of states. The well-known Myhill-Nerode theorem [
In this paper, we consider minimization for a particular model of register
automata, which process nite words over an in nite alphabet. On the one hand,
the class of memory automata we are dealing with (DMA, for short) is very
similar to that of deterministic nite memory automata introduced in [
The rst contribution of the paper is an isolation of the ideal \minimal storage" for a DMA. This is formalized in terms of the memorable values for any word in the language { the set of values that must be stored at any point. Using this we can give a characterization of the class of languages recognized by some DMA, which closely resembles the Myhill-Nerode theorem. Precisely, we associate with each language L a suitable equivalence ≡L, using the memorable values, and we characterize the class of DMA-recognizable languages as the class of languages L for which ≡L has nite index.
A similar characterization, with a more algebraic avor, has already appeared
in [
Organization: Section 2 gives preliminaries. Section 3 introduces the
notion of memorable value that will be used throughout the paper. Section 4
presents our characterization of DMA-de nable languages, along with the
results on canonical and minimal automata, while Section 5 gives conclusions. All
proofs can be found in [
We x an in nite alphabet D of (data) values. A (data) word is a nite sequence of values from the in nite alphabet D. Two words w and u are said to be isomorphic, and we denote it by w ≃ u, if SwS = SuS and w(i) = w(j) i u(i) = u(j) for all pairs of positions i; j in w. The ≃-equivalence class of a word w, denoted by [w]≃ or simply by [w], is called the ≃-type of w. A (data) language is a set of data words. Given two words w and u, we write w =L u if either both w and u are in L, or both are not. From now on, we tacitly assume that any data language L is closed under ≃-preserving morphisms, namely, ≃ re nes =L. 2.1
Finite-memory automata
In this section, we introduce a variant of Kaminski's nite-memory automata [
A con guration of A is de ned as a pair of the form (q; ) consisting of a control state q ∈ Qi, with 0 ≤ i ≤ k, and a memory content ∈ Di. The meaning of a transition rule of the form (q; ; E; q′) is that the automaton can move from a con guration (q; ) to a con guration (q′; ′) by consuming an input value a i the word ⋅ a has ≃-type and ′ is obtained from ⋅ a by removing all positions in E.
We enforce two sanity conditions to every transition rule (q; ; E; q′). To guarantee that the length of the target memory content ′ never exceeds k, we assume that E is non-empty whenever q ∈ Qk. Second, the memory is updated like a stack: if the ≃-type is of the form [ ⋅ a]≃, with (j) = a for some 1 ≤ j ≤ S S, then E contains the index j. This has two advantages: The memory content ′ always contains pairwise distinct elements and the order of the data values in the memory is the order of their last occurrences in the input word. We will exploit the latter property when we show that for every FMA language L there is a canonical FMA recognizing L.
A run of A is de ned in the usual way. If w is a data word and A has a run on w from a con guration (q; ) to a con guration (q′; ′), then we write w (q; ) ÐÐAÐ→ (q′; ′): The language recognized by A, denoted L (A), is the set of all words w such w that (q; ") ÐÐAÐ→ (q′; ′), for some q ∈ I and some q′ ∈ F .
We say that a nite-memory automaton A = (Q0; : : : ; Qk; T; I; F ) is deterministic if the set of initial states I is a singleton and there is no pair of transitions (p; ; E; q); (p; ; E′; q′) ∈ T , with either q ≠ q′ or E ≠ E′. Similarly, A is said to be complete if for every state q ∈ Qi and every ≃-type with i + 1 variables, T contains a transition rule of the form (q; ; E; q′). By a slight abuse of terminology, we abbreviate any deterministic and complete nite-memory automaton by DMA.
Our model of nite-memory automata is very similar the model of
nitememory automata introduced in [
Given a DMA-recognizable language L and a pre x w of an input word, there exist some values in w that need to be stored by any DMA that recognizes L. We will call these values memorable. As an example consider the language L = {w S w(1) = w(SwS)}. Observe that any DMA that recognizes L must store the rst symbol in its register. For this reason, we will de ne a to be memorable in the word abcde with respect to the language L.
De nition 2. Let L be a language. A value a is L-memorable in a word w if a occurs in w and there exists a word u and a value b such that ⎧⎪⎪ w ⋅ u ≃ (w ⋅ u)[a~b] ⎨ ⎪⎪ w ⋅ u ≠L w ⋅ u[a~b]: ⎩
Here u[a~b] denotes the word obtained from u by replacing each occurrence of a with b. Note that it follows from the de nition that b does not appear in any of w, u, and that a does appear in u.
It is convenient to x a string-based representation of the L-memorable values of a word w. We thus denote by memL(w) the nite sequence that consists of all L-memorable values of w ordered according to the positions of their last occurrences in w. This is well de ned because every L-memorable value of w must occur at least once in w.
The following proposition makes the intuition precise that any DMA has to store the memorable values of the input word. That is, if a DMA A reaches a con guration (q; ) after reading a word w, then memL(w) must be a subsequence of .
Proposition 1. Let A be a DMA and let L = L(A). Then, for every word w, memL(w) is a sub-sequence of the stored values of A after reading w. Moreover, if (q; ) and (q′; ′) are the con gurations reached by A after reading words w and w′, respectively, then ⎧⎪ q = q′ ⎨⎪⎩⎪⎪ ≃ ′ implies memL(w) ⋅ ≃ memL(w′) ⋅ ′:
Hence every DMA must store the memorable values of an input word. We will show in Section 4 that there is a DMA that does not need to store more than the memorable values.
Intuitively, the next proposition shows that, if two words u and v are isomorphic with respect to the L-memorable values of a word w, then L can not distinguish between w ⋅ u and w ⋅ v.
Proposition 2. Let L be a language over (D; R), where R is a either the identity or a dense total order on D. Then, for all words w; u; v we have memL(w) ⋅ u ≃ memL(w) ⋅ v implies w ⋅ u =L w ⋅ v: 4
This section is devoted to a characterization of the class of DMA-recognizable languages. This result also shows that these languages have automata that are • • • • • • • minimal in a strong sense: they have minimal number of control states and they store only the things that they must store, namely, the memorable values.
We begin by associating with each language L a new equivalence relation ≡L, which is ner than =L, but coarser than ≃.
De nition 3. Given a language L, we de ne ≡L ⊆ D∗ × D∗ by w ≡L w′ i memL(w) ≃ memL(w′), for all words u; u′ if memL(w) ⋅ u ≃ memL(w′) ⋅ u′ then w ⋅ u =L w′ ⋅ u′.
In a similar way, we associate with each DMA A a corresponding equivalence relation ≡A.
De nition 4. Given a DMA A, we de ne ≡A ⊆ D∗×D∗ by w ≡A w′ i whenever A reaches the con gurations (q; ) and (q′; ′) by reading w and w′, respectively, then q = q′ and ≃ ′ follow.
It is easy to see that both ≡L and ≡A are equivalence relations. In fact, ≡L is also a congruence with respect to concatenation of words to the right, namely, w ≡L w′ implies w⋅u ≡L w′⋅u, under the assumption that memL(w) = memL(w′). Note that, the ≡A-equivalence class of any word w is uniquely determined by the control state q and by the ≃-type of the register assignment of the con guration (q; ) that is reached by A after reading w. Hence, for any DMA A with n control states and storing at most k values, the corresponding equivalence ≡A has at most n ⋅ k! classes.
We are now ready to state the main characterization result.
Theorem 1. A language L is DMA-recognizable i ≡L has nite index.
We brie y summarize the key ingredients of the proof of Theorem 1. The full
proof is given in [
T is the set transitions ([w]≡L ; ; E; [w ⋅ a]≡L ), with w ∈ D∗, a ∈ D, = [memL(w) ⋅ a]≃, and E ⊆ {1; : : : ; SmemL(w)S + 1} such that memL(w ⋅ a) is the sub-sequence obtained from memL(w) ⋅ a by removing all positions in E; Minimal DMA. We now explain informally why it is that the canonical automaton for a given language L is minimal among all equivalent DMA recognizing L. Here, we adopt a general notion of minimality for DMA that takes into account both the number of control states and the number of stored values on each input word. Precisely, we say that a DMA A = (Q0; : : : ; Qk; T; {qI }; F ) is state-minimal if for every equivalent DMA A′ = (Q′0; : : : ; Q′k′ ; T ′; {qI′ }; F ′) that recognizes the same language, we have
SQS =
Q SQiS ≤ 0≤i≤k
Q SQ′iS = SQ′S: 0≤i≤k′ Similarly, we say that A is data-minimal if, for every equivalent DMA A′ = (Q′0; : : : ; Q′k′ ; T ′; {qI′ }; F ′) that recognizes the same language and every input word w, we have
w ⎧⎪⎪ (qI ; ") ÐÐA→ (q; ) ⎪ ⎨ w ⎪⎪⎪⎩ (qI′ ; ") ÐÐA→′ (q′; ′) implies
S S ≤ S ′S:
Finally, we say that A is minimal if it is both state-minimal and data-minimal.
Below, we state that the canonical automaton is minimal among all equivalent
DMA. The proof is given in [
Theorem 2. The canonical automaton AL for a given DRA-recognizable language L is minimal.
We conclude the section by explaining in what sense the minimal DMA, and in particular canonical automata, are unique up to isomorphisms. Here we think of each DMA A = (Q0; : : : ; Qk; T; {qI }; F ) as a nite directed graph, whose vertices are labeled by indices i ∈ {0; : : : ; k} and represent control states in Qi and whose edges are labeled by pairs ( ; E) and represent transitions of the form (q; ; E; q′)).
Corollary 1. Any minimal DMA recognizing a language L is isomorphic to the canonical automaton for L. 5
We provide a Myhill-Nerode-like theorem that characterizes the class of
DMArecognizable languages. As in the classical Myhill-Nerode Theorem over nite
alphabets, we show that for a given DMA language L there is an automaton
{ the canonical automaton for L { whose de nition depends only on L. This
answers a question left open in [
Some problems still remain open. It would be interesting to see whether or not analogous characterization results can be given in the case of DMA-recognizable languages over an in nite alphabet equipped with a partial order. Finally, more general models of automata could be taken into account, including, for instance, automata that process sequences of database instances and, possibly, use more powerful policies for updating their memory.