Finite state machines for strings over infinite alphabets.
Motivated by formal models recently proposed in the context of XML, we study automata and logics on strings over infinite alphabets. These are conservative extensions of classical automata and logics defining the regular languages on finite alphabets. Specifically, we consider register and pebble automata, and extensions of first-order logic and monadic second-order logic. For each type of automaton we consider one-way and two-way variants, as well as deterministic, nondeterministic, and alternating control. We investigate the expressiveness and complexity of the automata and their connection to the logics, as well as standard decision problems. Some of our results answer open questions of Kaminski and Francez on register automata.
Introduction
One of the significant recent developments related to the World Wide Web (WWW)
is the emergence of the Extensible Markup Language (XML) as the standard for data
exchange on the Web [1]. Since XML documents have a tree structure (usually defined
by DTDs), XML queries can be modeled as mappings from trees to trees (tree transduc-
tions), and schema languages are closely related to tree automata, automata theory has
naturally emerged as a central tool in formal work on XML [5, 17, 18, 19, 20, 21, 22, 23].
The connection to logic and automata proved very fruitful in understanding such languages
and in the development of optimization algorithms and static analysis techniques.
However, these abstractions ignore an important aspect of XML, namely the presence
of data values attached to leaves of trees, and comparison tests performed on them by
XML queries. These data values make a big di#erence - indeed, in some cases the difference
between decidability and undecidability (e.g., see [4]). It is therefore important
to extend the automata and logic formalisms to trees with data values. In this initial
investigation we model data values by infinite alphabets, and consider the simpler case
of strings rather than trees. Strings are also relevant in the tree case, as most formalisms
allow reasoning along paths in the tree. In the case of XML, it would be more accurate
to consider strings labeled by a finite alphabet and attach data values to positions in the
# A preliminary version with title Towards regular language over infinite alphabets appeared in the
proceedings of the 26th International Symposium on Mathematical Foundations of Computer Science
(MFCS 2001), Czech Republic, 2001.
Post-doctoral researcher of the Fund for Scientific Research, Flanders.
# This author supported in part by the National Science Foundation under grant number IIS-9802288.
string. However, this would render the formalism more complicated and has no bearing
on the results. Although limited to strings, we believe that our results provide a useful
starting point in investigating the more general problem. In particular, our lower-bound
results will easily be extended to trees.
We only consider models which accept precisely the regular languages when restricted
to finite alphabets. It is useful to observe that for infinite alphabets it is no longer
su#cient to equip automata with states alone. Indeed, automata should at least be able
to check equality of symbols. There are two main ways to do this:
1. store a finite set of positions and allow equality tests between the symbols on these
positions; and
2. store a finite set of symbols only and allow equality tests with these symbols.
The first approach, however, leads to multi-head automata, immediately going beyond
regular languages. Therefore, we instead equip automata with a finite set of pebbles
whose use is restricted by a stack discipline. The automaton can test equality by
comparing the pebbled symbols. In the second approach, we follow Kaminski and
Francez [15, 14] and extend finite automata with a finite number of registers that can
store alphabet symbols. When processing a string, an automaton compares the symbol
on the current position with values in the registers; based on this comparison it can
decide to store the current symbol in some register.
In addition to automata, we consider another well-known formalism: monadic second-order
logic (MSO). To be precise, we associate to strings first-order structures in the
standard way, and consider the extensions of MSO and FO denoted by MSO # and FO # ,
as done by Gr-adel and Gurevich in the context of meta-finite models [8]. MSO has
proven to be a good yardstick when other generalizations of regular languages were
investigated, e.g., for trees, infinite strings [25] and graphs [6].
Our results concern the expressive power of the various models, provide lower and
upper complexity bounds, and consider standard decision problems. For the above
mentioned automata models we consider deterministic (D), non-deterministic (N), and
alternating (A) control, as well as one-way and two-way variants. We denote these
automata models by dC-X where d # {1, 2},
1 and 2 stand for one- and two-way, respectively, D, N, and A stand for deterministic,
non-deterministic, and alternating, and PA and RA for pebble and register automata.
Our main results are the following (the expressiveness results are also represented in

Figure

1).
Registers. We pursue the investigation of register automata initiated by Kaminski and
Francez [15]. In particular, we investigate the connection between RAs and logic
and show that they are essentially incomparable. Indeed, we show that MSO #
cannot define 2D-RA. Furthermore, there are even properties in FO # that cannot
be expressed by 2A-RAs. The proof of the latter is based on communication
complexity [12]. Next, we consider the relationship between the various RA mod-
els. We separate 1N-RAs, 2D-RAs, 2N-RAs, and 2A-RAs, subject to standard
complexity-theoretic assumptions.
Pebbles. We consider two kinds of PAs: one where every new pebble is placed on the
first position of the string and one where every new pebble is placed on the position
of the current pebble. We refer to them as strong and weak PAs, respectively.
Clearly, this pebble placement only makes a di#erence in the case of one-way
PAs. In the one-way case, strong 1D-PA can simulate FO # while weak 1N-PA
cannot (whence the names). The proof of the latter separation is again based
on communication complexity. Furthermore, we show that all pebble automata
variants can be defined in MSO # . Finally, we provide more evidence that strong
PAs are a robust notion by showing that the power of strong 1D-PA, strong 1N-PA,
2D-PA, and 2N-PA coincide.
Decision Problems. Finally, we consider decision problems for RAs and PAs, and
answer several open questions from Kaminsky and Francez. First, we show that
universality and containment of 1N-RAs and non-emptiness of 2D-RA are unde-
cidable. Next, we obtain that non-emptiness is undecidable even for weak 1D-PAs.
As RAs are orthogonal to logically defined classes one might argue that PAs are better
suited to define the notion of regular languages over infinite alphabets. Indeed, they
are reasonably expressive as they lie between FO # and MSO # . Furthermore, strong
PAs form a robust notion. Adding two-wayness and nondeterminism does not increase
expressiveness and the class of definable languages is closed under Boolean operations,
concatenation and Kleene star. Capturing exactly MSO # most likely requires significant
extensions of PAs, as in MSO # one can express complete problems for every level of the
polynomial hierarchy, while computations of 2A-PAs are in P.
Related work. Kaminski and Francez were the first to consider RAs (which they
called finite-memory automata) to handle strings over infinite alphabets. They showed
that 1N-RAs are closed under union, intersection, concatenation, and Kleene star. They
further showed that non-emptiness is decidable for 1N-RAs and that containment is
decidable for 1N-RAs when the automaton in which containment has to be tested has
only two registers.
When the input is restricted to a finite alphabet, PAs recognize the regular languages,
even in the presence of alternation [18]. We point out that the pebbling mechanism we
employ is based on the one of Milo, Suciu, and Vianu [18] and is more liberal than
the one used by Globerman and Harel [9]: indeed, in our case, after a pebble is placed
the automaton can still walk over the whole string and sense the presence of the other
pebbles. Globerman and Harel prove certain lower bounds in the gap of succinctness of
the expressibility of their automata.

Overview

. This paper is organized as follows. In Section 2, we provide the formal
framework. In Section 3, we study register automata. In Section 4, we examine pebble
automata and conclude the section by comparing the register and pebble models. In
Section 6, we consider decision problems. We end with a discussion in Section 7.
We consider strings over an infinite alphabet D. Formally, a D-string w is a finite
sequence d 1 - d n # D # . A language is a set of D-strings. As we are often dealing with
2-way automata we delimit input strings by two special symbols, # for the left and
the right end of the string, neither of which is in D. I.e., automata always work on
strings of the form . We denote by dom(w) the set {1, . , |w|},
where |w| is the length of w. For i # dom(w), we also write val w (i) for d i .
2.1 Register automata
As explained in the introduction, register automata are finite state machines equiped
with a finite number of registers. These registers hold values from D. When processing
a string, an automaton compares the symbol on the current position with values in the
registers; based on this comparison it can decide to store the current symbol in some
register. We stress that the only allowed operation on registers (apart from assignment)
is a comparison with the symbol currently being processed. A transition depends on
the current state and whether the current symbol is already present in some register.
The transition relation specifies change of state, movement of the head, and possibly
whether the current symbol should be stored in a register. We follow the definition of
Kaminski and Francez [15, 14].
D is a tuple (Q, q 0 , F, # 0 , P ) where
. Q is a finite set of states;
. q 0 # Q is the initial state;
. F # Q is the set of final states;
. is the initial register assignment; and,
. P is a finite set of transitions of the forms (i, q) # (q # , d) or q # (q # , i, d).
Given a string w, a configuration of B on w is a tuple [j,
#}. The initial configuration is # 0 := [1, q 0 , # 0 ].
A configuration [j, q, # ] with q # F is accepting. Given the transition
(i, p) # (respectively, p #) applies to # i#
val w (j) #(i) for all i # {1, . , k}).
Given we define the one step transition relation # on
configurations as follows: # i# there is a transition (i, q) # (q # , d) that applies to
respectively; or there is a transition q # (q # , i, d) that applies to #, j # is as defined in
the previous case, and # is obtained from # by setting # (i) to val w (j).
We denote the transitive closure of # by # . Intuitively, transitions (i, q) # (q # , d)
can only be applied when the value of the current position is in register i. Transitions
d) can only be applied when the value of the current position di#ers from all
the values in the registers. In this case, the current value is copied into register i.
We require that the initial register assignment contains the symbols # and #, so
automata can recognize the boundaries of the input. Furthermore, from a # only right-
transitions and from a # only left-transitions are allowed.
As usual, a string w is accepted by B, if # 0 #, for some accepting configuration
#. The language L(B) accepted by B, is defined as {v | #v# is accepted by B}.
The automata we defined so far are in general non-deterministic. An automaton is
deterministic, if in each configuration at most one transition applies. If there are no
left-transitions, then the automaton is one-way. Alternating automata will be defined
below in Subsection 2.3. As explained in the introduction, we refer to these automata
as dC-RA where d # {1, 2} and Clearly, when the input is restricted to
a finite alphabet, RAs accept only regular languages.
2.2 Pebble automata
Pebble automata are finite state machines equiped with a finite number of pebbles. To
ensure a "regular" behavior, the use of pebbles is restricted by a stack discipline. That
is, pebbles are numbered from 1 to k and pebble only be placed when pebble i
is present on the string. The highest-numbered pebble present on the string acts as the
head of the automaton. A transition depends on the current state, the pebbles placed
on the current position of the head, and the equality type of the data values under the
placed pebbles. The transition relation specifies change of state, movement of the head,
and possibly whether the head pebble is removed or a new pebble is placed. If pebble i
is removed, pebble becomes the current head.
In our formal definition, we borrow some notation from Milo, Suciu, and Vianu [18].
k-pebble automaton A over D is a tuple (Q,
. Q is a finite set of states;
. q 0 # Q is the initial state;
. F # Q is the set of final states; and,
. T is a finite set of transitions of the form #, where
- # is of the form (i, s, P, V, q) or (i, P, V, q), where i # {1, . , k}, s # D #
- # is of the form (q, d) with q # Q and
d # {stay, left, right, place-new-pebble, lift-current-pebble}.
Given a string w, a configuration of A on w is of the form
{1, . , k}, q # Q and # : {1, . , i} # dom(w). We call # a pebble assignment and i the
depth of the configuration (and of the pebble assignment). Sometimes we denote the
depth of a configuration # (pebble assignment #) by depth(#) (depth(#)). The initial
configuration is # 0 := [1, q 0 , configuration [i, q, #] with q # F is
accepting.
A transition (i, s, P, V, p) # applies to a configuration
1.
2.
3.
4. val w
A transition (i, P, V, q) # applies to # if (1)-(3) hold and no transition (i, s, P, V, q) #
# of T applies to #. Intuitively, (i, s, P, V, p) # applies to a configuration if pebble
i is the current head, p is the current state, V is the set of pebbles that see the same
symbol as the top pebble, P is the set of pebbles that sit at the same position as the
top pebble, and the current symbol seen by the top pebble is s. As T is a finite set of
transitions, the automaton can only identify a finite number of distinguished symbols
s. Hence, every s can be regarded as a constant. In the register model, constants are
determined by the initial register assignment.
We define the transition relation # as follows: [i, q, # [i # , q # ] i# there is a transition
# (p, d) that applies to # such that q
and
. if
. if
. if
. if
. if lift-current-pebble then
The definitions of the accepted language, deterministic and one-way are analogous
to the case of register automata. We refer to these automata as dC-RA where d and C
are as before.
In the above definition, new pebbles are placed at the position of the most recent
pebble. An alternative would be to place new pebbles at the beginning of the string.
While the choice makes no di#erence in the two-way case, it is significant in the one-way
case. We refer to the model as defined above as weak pebble automata and to the latter
as strong pebble automata. Strong pebble automata are formally defined by setting
in the place-new-pebble case of the definition of
the transition relation.
2.3 Alternating Automata
For both automata models we also define an alternating version. Alternating automata
A additionally have a set U # Q of universal states. The sets from Q - U are called
existential. If #, then the automaton is non-deterministic.
A run of A on w is a tree where nodes are labeled with configurations as follows:
1. the root is labeled with the initial configuration;
2. every inner node labeled with an existential configuration # has exactly one child
# and # ; and,
3. every inner node labeled with a universal configuration # has children labeled with
An accepting run is a run where every leaf node is labeled with a final configuration.
The language accepted by A, is defined as
{w | there is an accepting run of A on #w#}.
2.4 Logic
We consider first-order and monadic second-order logic over D-strings. The representation
as well as the logics are special instances of meta-finite structures and their
logics as defined by Gr-adel and Gurevich [8]. A string w is represented by the logical
structure with domain dom(w), the natural ordering < on the domain, and a function
instantiated by val w . An atomic formula is of the form x < y,
D, and has the obvious semantics. The logic FO #
is obtained by closing the atomic formulas under the boolean connectives and first-order
quantification over dom(w). Hence, no quantification over D is allowed. The logic MSO #
is obtained by adding quantification over sets over dom(w); again, no quantification over
D is allowed.
A sentence # defines a set of strings in the usual way. More precisely, L(#) := {w #
As an example, consider the
defining the set of strings where every position carries a di#erent symbol.
2.5 Complexity Classes over Infinite Alphabets
Some of our separating results are relative to complexity-theoretic assumptions. To this
end, we consider a straightforward generalization of standard complexity classes (like
logspace, nlogspace, and ptime) to the case of infinite alphabets. We define such
classes using the Generic Turing Machines (GTM) device introduced by Hull and Su
[13] to model computable queries over infinite alphabets. Informally, a GTM is a Turing
machine with two right-infinite tapes. The tape alphabet is infinite. The input consists
of a string over the tape alphabet and is initially placed left-most on the first tape.
The moves are similar to those of classical Turing machines, except that equality of the
symbols under the heads can be tested at each move, and the symbol under one of the
heads can be written in the tape cell under the other head. The GTM can also test
for equality with constants from a distinguished finite subset of the tape alphabet, and
write such constants on either tape. For each classical complexity class C one can define
its analog C# for the GTM model in the natural way. For example, P# consists of the
languages accepted by GTMs which always stop after polynomially many moves with
respect to the length of their input. It is immediate to show that for usual complexity
2.6 Terminology
In the sequel we present several expressiveness and complexity results. We first introduce
some notation. If A and B are two formalisms defining languages of D-strings, we write
every language defined by A can be defined in B. That is, for every A # A
there is a B # B such that A.
Finally, we write A # B i# A # B and not A = B.
In addition to the expressive power of our formalisms, we are interested in the computational
complexity of the following problems. Let A be a formalism defining languages
of D-strings. Then membership in A is the problem of determining, for given A # A
and w # D # , whether w # L(A). We only consider data complexity, that is, we consider
A as fixed. Hence, the complexity is only measured in the size of w.
Two other problems we are interested in are universality and containment of A. The
first is the problem of deciding whether for a given A # A. The second
is determining whether A. Here, the complexity is
measured with respect to A, and A 1 and A 2 , respectively.
3 Register Automata
We start by investigating RAs. In particular, we compare them with FO # and MSO # .
Our main result is that RAs are orthogonal to these logics as they cannot even express all
FO # properties but can express properties not definable in MSO # . Further, we separate
the variants of RAs subject to standard complexity-theoretic assumptions.
3.1 Expressiveness
We show that there is a property of D-strings that is not definable in MSO # but is easily
expressible with a 2D-RA. In the rest of the paper we make extensive use of the symbol
# as a delimiter. We, therefore, assume that # D.
Theorem 3 2D-RA # MSO # .
Proof. Consider strings of the form u#v where u, v # (D - {# . Define N u and
N v as the set of symbols occurring in u and v, respectively. Denote by n u and n v their
cardinalities. We show that there is a 2D-RA A that accepts u#v i# n
there is no such MSO # sentence.
We first introduce some notation. For a string w, denote by lmow (d) the position in w
of the leftmost occurrence of d # D. Suppose N
where for every i < j, lmo u (a
n u with n v by visiting lmo u (a 1 sequence. Hence,
if a n and b m are not reached simultaneously, the automaton rejects the input string.
Otherwise, it accepts.
It remains to explain how the 2D-RA can visit lmo u (a 1
. in sequence. Clearly, lmo u (a 1 ) and lmo v (b 1 ) are the first positions of u and v, re-
spectively. If A has the values of a i and b i stored in its registers it can compute a i+1
and b i+1 . Indeed, to compute a i+1 it proceeds as follows. It first moves its head to
position lmow (a i ) by going to the left boundary and afterwards walking to the right
until it encounters a i . Now it tests, for all positions lmow (a starting with
carry a leftmost occurrence of a symbol d. This is done as follows:
from position lmow (a goes to the left until it either sees a d or reaches the left
end of the string. In the former case, it goes back to lmow (a (identified by the
first d) and proceeds with lmow (a 1. In the latter case lmow (a carries the
leftmost d, therefore a i+1 is identified. The computation of b i+1 can be done in a similar
way.
Assume towards a contradiction that # is an MSO # sentence such that u#v |= #
C be the set of D-symbols occurring in # . We call a string u#v
admissible each D-symbol occurs at most once in u or v; and, no
in C occurs in u or v. Let # be obtained from # by replacing each occurrence
of y, and every occurrence of
for every admissible string d 1 - d n #e 1
would be MSO definable and therefore regular. This
leads to the desired contradiction. #
As MSO has proven to be a good yardstick for generalizations of regular string
languages to trees and graphs [6, 25], the above theorem suggests that RAs can behave
in a "non-regular" manner.
The following proposition shows that this is essentially due to the ability to move
the head in both directions.
Proposition 4 MSO # can simulate every 1N-RA.
Proof. Let We describe the construction of an MSO #
formula # which holds for an input has an accepting computation on
w. First of all, # guesses, for each position i of w, the state that B is in after reading
. This can be done by existentially quantifying over sets (S q ) q#Q . Next, # guesses,
again for each position i, which transition B applies when it reads w i . This is done by
quantifying over sets (T t ) t#T . Now assume that there is an accepting computation of B
on w and that (S q ) q#Q and (T t ) t#T are chosen accordingly. Then, for each register j,
the register content of B before reading position i can be determined as follows: it is
the is of the form q # (q # , j, d)}. It
is straightforward to express this in MSO # (even in FO # ). With the ability to determine
register contents it is now easy to check (again in FO # ) that (S q ) q#Q and (T t ) t#T are
consistent with the transition relation of B. #
So far, one might think that 2-way register automata are simply too strong to be
compared with MSO logic. The next result provides more evidence that the computation
model based in registers is simply not comparable with logics. More precisely, we
show that RAs cannot capture FO # , even with alternation. The proof is based on a
communication complexity argument.
In communication complexity (see, e.g., [12]) the input string is divided in a pre-determined
manner between two parties (generally referred to as I and II) that can
send messages to each other according to a given protocol. A language is accepted
by a protocol if for each string both parties can decide after execution of the protocol
whether the string belongs to the language. Both parties have unlimited computation
power on their part of the string. The protocol only restricts the way in which the
parties communicate, typically by restricting the form and number of messages.
We next sketch the main idea for separation of 2D-RAs and FO # . This basic idea is
then extended to deal with alternation in the proof of Theorem 5. We consider strings
of the form u#v where u and v encode sets of sets of D-symbols in a suitable way. As
will be seen, the language
| u and v represent the same set of sets}
is definable in FO # . To show that the language is not accepted by a 2D-RA, we note
that each 2D-RA working on strings of the form u#v can be simulated by a protocol in
the following way: I is given u while II is given v. The first party simulates the 2D-RA
until this computation tries to cross the delimiter # to the right. At this point, it sends
the present state q and the data values d 1 , . , d k currently in its registers. Hence, II
gets full information about the configuration of A (as the position of the symbol #
is fixed). Then IIsends in turn the current configuration to I. This process continues
until one of the parties detects a final state. What kind of protocol can simulate such
behavior? First, we need a message for every configuration. Suppose we restrict to at
most N di#erent data values in the strings u#v. Then M := |Q| - N k di#erent messages
are needed. Here, k is the number of registers and Q is the set of states of the 2D-
RA. Call a sequence of messages a dialogue. We only need to consider dialogues up to
length M (as every message can only be sent once in every direction). Hence, there
are only M 2 M di#erent dialogues on input strings consisting of N di#erent D-symbols.
The latter value is exponential in N . However, there are 2 2 N
sets of sets of N di#erent
D-symbols. So for large enough N there must be di#erent strings u#u and v#v with
accepted by the protocol via the same dialogue. But, this means that u#v is also
accepted. Hence, no such protocol can define L, which implies that no 2D-RA accepts L.
In the proof of Theorem 5 we extend this idea to alternation. This requires exchanging
partial computation trees of the 2A-RA. To apply the same counting trick we then have
to consider more deeply nested hypersets.
Our proof technique is inspired by a proof of Abiteboul, Herr, and Van den Buss-
che [2] separating the temporal query languages ETL from TS-FO. To this end, they
show that every query in ETL on a special sort of databases can be evaluated by a
communication protocol with a constant number of messages, whereas this is not the
case for TS-FO. In our case, to simulate 2D-RA (and 2A-RA) we need a more powerful
protocol where the number of messages depends on the number of di#erent data values
in u and v.
Theorem 5 FO # 2A-RA.
Proof. We start with some terminology. Let D be a finite or infinite set. A 1-hyperset
over D is a finite subset of D. For i > 1, an i-hyperset over D is a finite set of (i - 1)-
hypersets over D. We often denote i-hypersets with a superscript i, as in S (i) .
For ease of presentation, we assume that D contains all natural numbers. For each
be D-{1, . , j}. Next, let j > 0 be fixed. We inductively define encodings
of i-hypersets over D j . First, a string is an encoding of the
1-hyperset . For each i # j, and encodings w 1 , . , w n
of (i - 1)-hypersets, iw 1 iw 2 - iw n i is an encoding of the i-hyperset {H(w
= as the language
{u#v | u and v are encodings of m-hypersets over Dm - {#} and
Lemma 6 For each m, L m
is definable in FO # .
Proof. Let k # 1 be fixed. For each i # k, we define an
expressing on input w that the intervals [x # , x r ] and [y # , y r ] encode the same i-hyperset
over
By x # [y, z] we abbreviate y # x#x # z. By clean i we abbreviate the formula
#}). For each i, the formula hyp i
express that [x # , x r ] encodes an i-hyperset. Therefore, let
and, for i > 1,
clean
The formula # i is inductively defined as follows:
and for i > 1,
The language L k
is then expressed by the formula
Here, 1 and max refer to the first and last element of the string, respectively, and +1 is
the successor function. #
Next, we show that no 2A-RA can recognize L m
As described above,
the underlying idea is that for large enough m, a 2A-RA simply cannot communicate
enough information between the two sides of the input string to check whether H(u)
Definition 7 Let P be a binary predicate on i-hypersets over D and let k, l # 0. We
say that P can be computed by a (k, l)-communication protocol between two parties
(denoted by I and II) if there is a polynomial p such that for each finite set D there is
a finite alphabet # of size at most p(|D|) such that, for all i-hypersets X (i) , Y (i) over
can be computed as follows:
1. I gets X (i) and II gets Y (i) ; both know D and #;
2. I sends a message a 1 (D, X (i) ) to II and II replies with a message b
to I. Each message is a k-hyperset over #.
3. I sends a message a to II and II replies with a message b
4. After exp l (p(|D|)) rounds of message exchanges, both I and II have enough information
to decide whether P (X (i) , Y (i) ) holds. More precisely, they apply a Boolean
function a r+1 (D, X (i) , b r ) (for I) or b r+1 (D, Y (i) , a r ) (for II) that evaluates to true
So, formally, a protocol consists of the functions a 1 , . , a r+1 , b 1 , . , b r+1 . Note that the
computing power of I and II can be completely arbitrary.
Lemma 8 For m > 4, L m
cannot be computed by a (2,2)-communication protocol.
Proof. Suppose there is a protocol computing L m
. For every finite set D with d el-
ements, the number of di#erent possible messages is the number of 2-hypersets which
is at most exp 2 (p(d)). Call a complete sequence of exchanged messages a 1 b 1 a 2 b 2 .
a dialogue. Every dialogue has at most exp 2 (p(d)) rounds. Hence, there are at most
di#erent dialogues. However, the number of di#erent m-hypersets
over D is exp m (d). Hence, for m > 4 and D large enough there are m-hypersets
Y (m) such that the protocol gives the same dialogue for P (X (m) , X (m) ) and
But that means it also gives the same dialogue on P (X (m) , Y (m) ) and
This leads to the desired contradiction. #
We refer to strings of the form u#v, where u and v do not contain #, as split strings.
A communication protocol computes on such strings by assigning u to I and v to II.
Lemma 9 On split strings, the language defined by a 2A-RA can be recognized by a
(2,2)-communication protocol.
Proof. Let working on split strings over
D. We assume w.l.o.g. that there are no transitions possible from final configurations.
Further we assume that B never changes direction at the symbol #. Hence, on a split
string u#v, when it leaves u to the right it enters v and vice versa. Define p as the
polynomial p(n) := |Q|n k , that is, the number of configurations that can be assumed
at the position labeled with # on strings with at most n di#erent data values. Let
u#v be an input split string; let D be the set of data values occurring in w.
Let the position in the string of the split symbol # be e. Then, set # := {[e, q, # ] |
is the set of configurations that can be assumed
at the position of the split symbol. We refer to these as #-configurations. Note that
In essence, both parties compute partial runs where they send the #-configurations
in which B walks o# their part of the string to the other party. To be concrete, I
computes all the runs of B on u. The leaves of these runs consist of #-configurations or
final configurations, and no inner vertex is labeled with a #-configuration. It then sends
to II the set of all sets of #-configurations appearing at leaves of such runs. Party II in
turn, computes the same information for runs starting from the sets of #-configurations
it received and sends it to I. This process is repeated. If after exp 2 (|#|) messages there
is a message containing the empty set then the input is accepted (as final configurations
are not transmitted, the presence of an empty set indicates a run where all leaves are
accepting configurations). We next describe this formally.
A configuration [i, q, # ] is called a u-configuration if i < e and a v-configuration if
#-configuration is called a u#-configuration if it is assumed from the left and
a #v-configuration if it is assumed from the right. Note that, by our assumption that
never changes direction at #, we can distinguish these two sets of configurations.
We introduce the following notions. For an arbitrary configuration #, a (#)-run is
a run where the root is labeled with #, all the leaves are labeled with final configurations
or #-configurations and no inner vertex, besides possibly the root, is labelled by a #-
configuration. For such a run t, we define Leaf-labels(t) as the set of #-configurations
occurring at the leaves of t. For a set C of configurations, define #(C (1) )
as the set of sets of configurations
{
Note that #(C (1) ) is computable for any set C (1) of configurations. Finally, for a set S (2)
of sets of configurations, define #(S (2)
#S (2) #(C (1) ).
be the singleton 2-hyperset containing the singleton set {# 0 }, that is, S 0 :=
{{# 0 }}. Recall that # 0 is the initial configuration. Define a sequence of 2-hypersets of
configurations by S i := #(S i-1 ), for all i # 1. Note that, for i > 0, if i is even then S i is a
2-hyperset of #v-configurations. If i is odd then S i is a 2-hyperset of u#-configurations.
Let us call a run t an i-pass run if all its leaf configurations are either accepting or
#-configurations that are reached by computations that have visited # exactly i times.
Clearly, if C (1)
there is an i-pass run t of B on w such that
C (1) and vice versa. Hence, B accepts w i# there is an i and a C (1)
containing the
empty set.
The protocol works as follows. Party I starts by sending S 1 . For i > 0, when party
II receives S 2i-1 it responds with S 2i ; when party I receives S 2i it responds with S 2i+1 .
The parties accept whenever a 2-hyperset with the empty set is transmitted. As there
are only exp 2 (|#|) di#erent 2-hypersets over # the parties can reject if the empty set
was never obtained after exp 2 (|#|) rounds of messages. #
By Lemma 8 and 9, L m
= is not computable by a 2A-RA. Hence, Theorem 5 follows.
3.2 Control
In the previous section we related RAs with logic. In this section we compare RAs
with various kinds of control. Kaminski and Francez already showed that 1D-RAs are
weaker than 1N-RAs and that there is a property (are all data values di#erent?) that
is in 2D-RA but not in 1N-RA. We can only separate the other classes by relying on
complexity theoretic assumptions as explained next.
The main observation is that on strings of a special shape, RAs can simulate multi-
head automata. These strings are of even length where the odd positions contain pair-wise
distinct elements and the even positions carry symbols from a finite alphabet, say
{a, b}. By storing the unique ids preceding the a's and b's, the RA can remember
the positions of the heads of a multi-head automaton. Note that 2D-RAs can check
whether the input string is of the desired form. As deterministic, nondeterministic, and
alternating multi-head automata recognize precisely logspace, nlogspace, and ptime
languages, respectively, membership for 2D-RA, 2N-RA, and 2A-RA is hard for these
classes, respectively [24, 16]. Furthermore, it is easy to see that the respective membership
problems also belong to the infinite alphabet variants of these classes and actually
are even complete for these classes, as one can always encode a string over an infinite
alphabet over a binary alphabet. Thus, we can show the following proposition.
Proposition 10 1. Membership of 2D-RA is complete for logspace# ;
2. Membership of 2N-RA is complete for nlogspace# ; and
3. Membership of 2A-RA is complete for ptime# .
The indexing technique above cannot be used for 1N-RAs, because they cannot check
whether the odd positions form a unique index. However, we can extend (2) to 1N-RAs
using a direct reduction from an nlogspace-complete problem: ordered reachability.
Proposition 11 Membership of 1N-RA is complete for nlogspace# .
Proof. Clearly, membership is in nlogspace# . For the hardness we use a reduction
from ordered reachability: given an ordered graph with the property that if there is
an edge from u to v then u < v; is there a path from the first node to the last one?
This problem is hard for nlogspace. Indeed, ordinary reachability is complete for both
nlogspace and nlogspace# and the following is a logspace reduction from ordinary
reachability to ordered reachability. Given a graph G with n nodes, a source s
and a sink t, we construct the graph G # with vertices {(i,
graphically, where there is an edge from (i, j) to (i # , is an
edge in G. The source and sink are (1, s) and (n, t), respectively. Clearly, t is reachable
from s in G i# (n, t) is reachable from (1, s) in G # . Further, G # is computable in
logspace. Hence, ordered reachability is hard for nlogspace# . We next reduce the
latter to the membership problem of 1N-RAs. The input to the 1N-RA is of the form
[1, a 11 - , a 1i 1
][2, a 21 - , a 2i 2
].[n]. Here, [j, a j1 - , a ji j
encodes that there is an edge
from j to each a jl , for . Then the 1N-RA accepts when n can be reached
from 1 by following edges. Every ordered graph can be encoded as such a list. Hence,
since ordered reachability is hard for nlogspace# , so is membership for 1N-RA. #
As a consequence of Proposition 11, all four classes defined by the mentioned automata
models are di#erent unless the corresponding complexity classes collapse. We
refer the reader to Figure 1 for a visual representation of these relationships.
4 Pebble Automata
We next focus on pebble automata. We show that PAs are better behaved than RAs
with respect to the connection to logic. In a sense, PAs are more "regular" than RAs.
Indeed, we show that strong 1D-PAs can simlate FO # and that even the most liberal
pebble model, 2A-PA, can be defined in MSO # . Furthermore, we can separate 2A-RAs
from MSO # under usual complexity-theoretic assumptions. Next, we show that weak
one-way PAs do not su#ce to capture FO # . Again, the proof is based on communication
complexity. Finally, we prove that for strong PAs, the one-way, two-way, deterministic
and nondeterministic variants collapse. Together with the straightforward closure under
Boolean operations, concatenation and Kleene star, these results suggest that strong PAs
define a robust class of languages.
4.1 Expressiveness
Proposition 12 FO # strong 1D-PA.
Proof. Clearly, FO # cannot define the D-strings of even length while 1D-PAs (strong
or can easily do so.
For the inclusion, note that an FO # sentence # in prenex normal form can be evaluated
straightforwardly by a strong 1D-PA. We use one pebble for each quantifier. Pebble
1 is used for the outermost quantifier, and the pebble with the largest number is used
for the innermost quantifier. The automaton cycles through all possible assignments of
positions to the pebbles hence to the variables. While doing so, it records in its state
all information about equalities and inequalities among the symbols at the pebbled
positions. #
We next show that PAs are subsumed by MSO # . Thus, they behave in a "regular"
manner.
Theorem 13 MSO # can simulate 2A-PA.
Proof. The proof is an extension to infinite alphabets of a proof in [18] where it is shown
that alternating tree-walking pebble automata over finite alphabets can be simulated
in MSO. In brief, we reduce the simulation problem of a k-pebble automaton to the
Alternating Graph Accessibility Problem, AGAP [10]. An alternating graph (or and/or
graph) is a graph E) whose nodes V are partitioned into and-nodes and or-
nodes: consists of all pairs (G, x), where G is an alternating graph
and x is an accessible vertex of G, with accessibility defined as follows: an and-node
is accessible if all its successors are accessible; an or-node is accessible if at least one
of its successors is accessible. Note that and-nodes with no successor are by definition
accessible. It can be shown that the set of accessible nodes is definable in MSO and
therefore in MSO # . Indeed, consider the formula
where reverse-closed(S) is:
Here, D# and D# are unary relations containing the or- and and-nodes, respectively.
Given an alternating k-pebble automaton and a string
we construct the following and/or graph E). Its or-nodes are all configurations
of A on w whose states are existential; its and-nodes are all configurations
whose states are universal, together with an additional distinguished and-node #. The
set of edges E is {(# is accepting}. It follows directly from the
definitions of L(A) and of AGAP that a string w is in L(A) i# the initial configuration
# 0 is accessible in the graph GA,w . Hence, it only remains to show that we can express
the AGAP problem on GA,w in MSO # . Here, the di#culty lies in the fact that the nodes
in GA,w are tuples of nodes from the input structure w (a configuration
represented by the i-tuple (#(1), . , #(i)); q does not depend on w and will be encoded
separately.) Hence, the set S in (1) is no longer unary. To circumvent that, we rely on a
special property of GA,w . Namely, if two nodes described by an i-tuple (#(1), . , #(i))
and a j-tuple (# (1), . , # (j)) are connected by an edge, then either
or and the tuples agree on all but the last position. This follows from the
stack discipline on pebbles in A (only the last pebble can be moved) and allows us
to quantify independently, on di#erent portions of the graph. The construction of the
relies on this observation. We outline this construction next.
For simplicity, we can assume w.l.o.g. that for each universal state q and (i, s,
either {# | (i, s, P, V, q) # or there are two states q 1 , q 2 such that {# |
(i, s, P, V, q) It is also convenient to assume that
Q is partitioned into disjoint such that states in Q i "control" pebble
i. Furthermore, we enumerate the states in Q such that
We consider first the case when A uses a single pebble, to illustrate how one encodes
the state in a configuration and how to encode the transitions. For simplicity
we only consider transitions involving constants; dealing with transitions without constants
is an easy generalization. In the case of only one pebble, configurations can be
assimilated with pairs (q, x), and transitions can be simplified to (s, q) # (p, d) where
{stay,left,right}. The MSO # formula #A defining acceptance by A uses a di#erent
unary relation S j for each state q j # Q. Namely #A is:
(reverse-closed
where reverse-closed is a formula stating that S 0 ,
are closed under reverse
transitions of A according to the and/or semantics. Thus, #A states that the initial
configuration of A is accessible in the and/or graph GA,w . It follows that #A holds i#
A accepts w.
The formula reverse-closed is a direct representation of the transitions in A (and
edges in GA,w ) in MSO # . For each transition (a, q u ) # of A where q u is existential,
reverse-closed includes one conjunct. For example, if the corresponding
conjunct is
where succ(x, y) is the FO # formula defining the successor relation on dom(w). If q u
is universal, a # D, and q u 's transitions under a are (a, q u
reverse-closed includes the conjunct
To see that #A holds on w i# A accepts w, it su#ces to notice the similarity between
(1) and (3). For that, one needs to observe how the formula for reverse-closed in a general
graph (2) becomes the formula above when instantiated to GA,w . For example notice
that each and-node in GA,w has zero or two successors (hence the universal quantifier
in (2) becomes a conjunction).
We now extend (3) to the case when k is arbitrary. We define a predicate reverse-closed (i) ,
for each stating that S n i-1 +1 , . , S n i
are closed under reverse transitions
of A. Then, the MSO formula equivalent to A will be #A in (3), with reverse-closed
replaced with reverse-closed (1) . The predicate reverse-closed (i) assumes that pebbles
are fixed, and their positions described by the free variables x 1 , . , x
it also has free variables
. The predicate only considers moves a#ecting
pebbles Partition A's transitions into is the
set of transitions from states in Q i . Then,
reversed-closed (i) := #
# .
For transitions # not lifting or placing a pebble, # is the same as for reverse-closed
above, except that now it also inspects the presence/absence of the previous i-1 pebbles
and tests equality/inequality of the corresponding values with the current value. For
example, for the corresponding # is
In general, for a transition (i, s, P, V, q) # we use the formulas
and
The new transitions are the lift-current-pebble and place-new-pebble transitions. These
determine the following conjuncts in reverse-closed (i) :
. for
(reverse-closed (i+1) =# S v Note the resemblance
of # (i+1) to (3): here q v acts as an initial state for pebble i + 1.
. for
Note that here q u acts as a terminal state for pebble i.
This completes the proof of the translation of A into MSO # . Note that the stack
discipline imposed on the use of pebbles is essential to the construction in the proof. #
It is open whether the above inclusion is strict. However, we can show the following.
Proposition 14 For every i # N, there are MSO # formulas # i and # i such that the
membership problem for # i and # i is hard for # P
, respectively. In contrast,
membership for 2A-PAs is ptime-complete.
Proof. Ajtai, Fagin, and Stockmeyer [3] showed that for every level of the polynomial
hierarchy (ph) there is an MSO formula over graphs such that model checking is hard
for that level. Hence, it su#ces to observe that graphs can readily be encoded as strings.
We describe a translation from MSO formulas # to MSO # formulas # and a translation
from graphs E) to strings w(G) such that G |= # if and only if
Hence, if model checking of # is hard for a level of ph then model checking
for # the corresponding level of ph# .
To this end, define w(G) as the string consisting of blocks of the form #i i 1 . i k
E(i, j)}. Further, let vertex(x) be the
is obtained from # by replacing
every occurrence of E(x, y) by
Then inductively replace from the inside to the outside every occurrence of a subformula
#x#X#, and #X#, by #x(vertex(x) #x(vertex(x) #X(#x # (X(x #
vertex(x #), and #X(#x # (X(x # vertex(x #). This completes the description
of the translation.
For the latter statement of the proposition recall that a configuration of a k-pebble
2A-PA consists of a state and at most k positions of the pebbles. This takes only
logarithmic space in the size of the input. Therefore, a 2A-PA can be simulated in
alogspace# which equals ptime# . Hardness follows from a reduction from AGAP as
defined in the proof of Theorem 13. #
Proposition 12 and Theorem 13 show that PAs fall nicely in between FO # en MSO # .
In the next subsection we show that, determinism, non-determinism, one- and two-way
coincide for strong PAs. It is open whether alternating control yields additional power.
We end this subsection by considering weak PAs. Recall that weak PAs place new
pebbles at the location of the current head rather than the beginning of the string.
Clearly, this only makes a di#erence for one-way models. Unlike their strong counter-
parts, we show that weak PAs cannot simulate FO # , which justifies their name. The
proof is once again based on communication complexity. We show that the language
defined in the proof of Theorem 5, cannot be computed by weak 1N-PAs. However,
we use a di#erent kind of communication protocol which better reflects the behaviour
of a weak 1N-PA.
Theorem 15 FO # weak 1N-PA.
Proof. The proof is similar to that of Theorem 5. We show by a communication
complexity argument that the FO # -expressible language L 2
defined in the proof of
Theorem 5 cannot be recognized by a weak 1N-PA. Recall that L 2
consists of strings
of the form u#v where u and v encode the same 2-hyperset. Let k be fixed and let
sets. The new protocol has only one agent which has arbitrary access to
the string u but only limited access to the string v. On u, its computational power is
unlimited. The access to v is restricted as follows. Let # D. There is a fixed function
and the agent can evaluate f on all arguments (v, -
d, s),
d is a tuple of length k of symbols from u and s # S 1 . Based on this information
and on u the agent decides whether u#v is accepted.
First, we show that there is no function f such that there is an agent which recognizes
. towards a contradiction assume otherwise and let S 1 , S 2 and f be the corresponding
finite sets and advice function, respectively. Let u#v be an input string and let D
denote the set of symbols that occur in u (containing 1 and 2, if u correctly encodes a
2-hyperset). Let d |. We can assume w.l.o.g. that
the agent always evaluates f for all possible arguments. As there are at most d k m 1
such arguments there are at most m d k m 1di#erent "interactions" between the agent and
function f . It is important here that the protocol is non-adaptive, i.e., the order of
the questions does not matter. Let
. Let u 1 , . , u h be encodings of all the h
possible 2-hypersets over D- {1, 2}. If d is large enough with respect to k, m 1 , and m 2
then there are more 2-hypersets on D - {1, 2} than di#erent interactions. Hence, there
must be encodings u, u # of 2-hypersets with H(u) #= H(u # ) such that the interactions on
u#u and u #u # are the same. Hence, the agent accepts u#u if and only if he accepts
which is a contradiction.
It remains to show that on split strings a weak 1N-PA can be simulated by a protocol.
Intuitively, this works as follows. On input u#v, as we consider one-way weak PAs,
whenever the current pebble enters v, the computation remains in v until that pebble
is lifted. Therefore, the set of states which can be obtained when lifting the pebble only
depends on v, the symbols below the pebbles placed in u and the placement information,
that is, which pebbles are located on the same positions. Hence, we define f(v, -
d, s) as
the set of states that can be reached when pebble i enters v in state q and the pebbles in
are placed on symbols -
d (with # indicating that a pebble is not present). Here, i and
q are coded into s. Additionally, s also contains the position placement of the pebbles
in u. This function provides enough information for the agent to simulate the 1N-PA.
4.2 Control
Our next result shows that all variants of strong pebble automata without alternation
collapse. This suggests that strong PAs provide a robust automaton model.
Theorem 16 The following have the same expressive power: 2N-PA, 2D-PA, strong
1N-PA and strong 1D-PA.
Proof. We show that, for each 2N-PA A, there is a strong 1D-PA B that accepts the
same language. Actually, in our construction B uses the same number of pebbles as A.
Therefore, let pebbles.
For technical simplicity, we assume w.l.o.g. that A lifts pebbles only at the right
delimiter (instead of lifting a pebble at an arbitrary position it can remember the target
state q, go to the right delimiter and lift the pebble there, moving into state q).
First, we informally describe the idea of the construction. Recall the classical power-set
construction which translates a non-deterministic 1-way automaton M (over a finite
alphabet and without pebbles) into a deterministic one, M # . Intuitively, M # computes,
for each prefix u of the input string , the set of states that M might reach
by reading u. M # performs an on-line simulation of M in the sense that each step in the
computation of M corresponds to exactly one step of M # .
One cannot expect such an on-line simulation to work for 2-way automata (even
for finite alphabets), as the non-deterministic behaviour of a 2-way automaton might
involve moving in di#erent directions. Instead (in the finite case without pebbles) the
deterministic automaton can compute, for each position i in the input string w, a function
f i which describes the aggregate behaviour of M on w 1 - w i , i.e., the portion of
the input which is at the left-hand side of the i-th position. The functions f i can be
computed inductively from left to right (forgetting f i-1 once f i is computed). In the
end, f n and the knowledge of the possible first states that the automaton assumes at
the right delimiter of the input provide all necessary information to decide whether w
is accepted.
It is maybe a bit surprising that this approach can, by and large, be adapted to the
case where pebbles are present and the alphabet is infinite. We proceed as follows. First,
we assume that A is further normalized in that it accepts its input only in configurations
[1, q, #], i.e., with only one pebble. By virtually adding two steps we view an accepting
computation as consisting of (1) a first step in which the first pebble is placed at the
first position, (2) a computation in which always at least one pebble is present, and
(3) a final step in which the only remaining pebble is removed. Writing [0,
(virtual) configuration without pebble, to determine whether A accepts, one has to find
out whether [0, q 0 , # [0, q, # ], for some final state q.
The latter can be done by recursively solving subproblems of the form [i, q, # >i
[i, q #], where the subscript > i indicates that only subcomputations are considered in
which, at every step, more than i pebbles are present.
More formally, we show the following claim by induction on i (starting from
Claim 17 For each i # {0, . , k} and each finite set R, there is a strong 1D-PA B i
(with k pebbles) such that, whenever B i starts from a configuration [i, p, #], where p # R,
the next configuration of depth i of B i is [i, (p, S), #], where
[i, q #]}. In particular, the set of states of B i contains R and R - 2 Q-Q .
First, it should be noted that the theorem follows from the claim. To this end, we
set intended initial state of B 0 ) and obtain an automaton
which ends up in a state (p 0 , S), where S is the set {(q, q # Q | [0, q, # >0 [0, q #]}.
The set of final states of B 0 simply consists of all states (p 0 , S), where S contains a pair
For the proof of the claim is trivial, as there are no configurations of depth > k.
Hence, B k can compute (p, S) by a stay-transition. Therefore, let i < k and suppose the
claim holds for all j > i.
Intuitively, the set S can be computed by one left-to-right pass of the (i+1)st pebble.
During this pass, B i computes, for each position l in the string the sets of pairs (q, q # ),
such that there is a sub-computation which starts from state q at position l (position 1,
respectively) and ends in state q # at position l, without moving pebble positions
l # l. Note that such subcomputations might move pebbles j positions # l.
To compute this information, the automaton B i+1 is used repeatedly.
We first introduce some more notation. Let the input string w of length n be fixed.
For l # n, let # l denote the (i 1)-pebble assignment that coincides with # in the first i
pebbles and for which # l (i l. We write S# l ) for the set of pairs (q, q # ) of states
such that there is a computation starting at [i + 1, q, # l ] and reaching [i
only includes configurations [j, q # ] that fulfill j > i +1 or (j
Intuitively, this says that pebble not allowed to move to the right of position l.
We write S# (l) for the set of pairs (q, q # ) of states for which [i l ] can be reached
from [i by a subcomputation satisfying the same property.
We are now ready to complete the proof of the claim. The set S# l ) can be
computed as follows. Let R# l ) be the set of pairs (q, q # ) for which one of the following
holds:
(a) There exist
1D-RA
1N-RA
MSO #
W1D-PA
W2N-PA

Figure

1: Inclusions between the classes under consideration. Solid lines indicate inclusion
(strictness shown as #=), dotted lines indicate that the classes are incomparable.
Dashed lines indicate strict inclusion subject to complexity-theoretic assumptions.
It is straightforward to see that S#) is simply the transitive closure of R#). The
information needed for (a) can be computed in one left-to-right pass of pebble i + 1.
By induction we can assume a subautomaton B i+1 that computes, for each position l,
the part of R#) contributed by condition (b). Note that (c) and the computation of
the transitive closure do not require any pebble movements. During the same pass, the
automaton can compute, for each position l, the set S# (l). The computation of S# (l)
makes use of the sets S#).
From S# n ), S# (n) and the transition relation of A one can deduce, during a lift-
pebble step, the set S as in the claim. Note that n is the position of the right delimiter
and recall that A lifts its pebbles only at that position.
This completes the proof of the claim and of the theorem. #
Registers versus Pebbles. The known inclusions between the classes that we considered
are depicted in Figure 1. The pebble and register models are rather incomparable.
Indeed, from the connection with logic we can deduce the following. As 2D-RA can
already express non-MSO # definable properties, no two-way register model is subsumed
by a pebble model. Conversely, as strong 1D-PAs can already express FO # , no strong
pebble model is subsumed by any register model. Some open problems about the relationships
between register and pebble automata are given in Section 6.
5 Decision Problems
We briefly discuss the standard decision problems for RAs and PAs. Kaminski and
Francez already showed that non-emptiness of 1N-RAs is decidable and that it is decidable
whether L(A) # L(B) for a 1N-RA A and a 1N-RA B with 2-registers. We
next show that universality (does an automaton accept every string) of 1N-RAs is un-
decidable, which implies that containment of arbitry 1N-RAs is undecidable. Kaminski
and Francez further asked whether the decidability of non-emptiness can be extended
to 2D-RAs: we show it cannot. Regarding PAs, we show that non-emptiness is already
undecidable for weak 1D-PAs. This is due to the fact that, when PAs lift pebble i, the
control is transferred to pebble i - 1. Therefore, even weak 1D-PAs can make several
left-to-right sweeps of the input string.
In our proofs, we use a reduction from the Post Correspondence Problem (PCP)
which is well-known to be undecidable [11]. An instance of PCP is a sequence of pairs
This instance has a solution
if there are m # N and # 1 , . , #m # {1, . , n} such that x # 1 - x . The
asks whether a given instance of the problem has a solution.
Suppose w.l.o.g. that the integer numbers {1, . , n} and the values a, b, &, # are in
D. Denote the latter set of symbols by Sym. We consider input strings of the form
is a delimiter and u and v are strings representing a candidate
solution
, . , y #m ) for the PCP instance in a suitable way.
To check whether such a candidate is indeed a solution, we roughly have to check
whether
each i, that is, corresponding pairs are taken; and
(2) both strings are the same, that is, corresponding positions in x# 1 - x#m and
carry the same symbol.
To check (1) and (2), we use a double indexing system based on unique data values.
We describe the encoding in more detail. Each item x # j
is encoded as a string of the
Here, & is a separator, # D- Sym represents j by a unique
data value, the a i are from {a, b} such that x # j
and the # i represent the
position of a i in x by a unique data value. To achieve uniqueness, all #- and #-symbols
are allowed to occur only once in u. Correspondingly, y # j
is encoded by a string of the
such that y # j
and the corresponding conditions hold.
A string u#v is syntactically correct if it has the properties described so far and fulfils
the following two conditions:
. the #-projection of u (i.e., the string consisting of the #-entries of u) equals the
#-projection of v; and
. the #-projection of u equals the #-projection of v.
A syntactically correct string u#v represents a solution of the PCP instance, if,
. for each #, the numer to the right of # is the same in u and in v, and
. for each #, the symbol from {a, b} at the right of # is the same in u and in v.
We next show that universality of 1N-RAs and weak 1D-PAs are undecidable. In
the former case, we construct an 1N-RA A that accepts an input string w if and only
if it is not syntactically correct or does not represent a solution. Hence, A accepts
all inputs if and only if the PCP instance has no solution. In the construction non-determinism
comes into play. The automaton simply tries to guess an error in the
encoding represented by the input string.
When showing undecidability of universality of weak 1D-PAs, we construct an automaton
that checks whether no error occurs in the encoding represented by the input
string. This happens by doing several sweeps over the input string.
5.1 Register Automata
Theorem It is undecidable whether a 1N-RA is universal.
Proof. The initial register assignment assigns the values in Sym to the first n
registers.
We construct an 1N-RA A that accepts an input string w if and only if it is not
syntactically correct or does not represent a solution. Hence, A accepts all inputs if and
only if the PCP instance has no solution.
A checks that one of the following conditions holds for its input string w.
1. w is of the wrong form.
(a) w is not of the form u#v or u or v is not of the form (&#i # 1 a
(i # {1, . , n}).
(b) x i #= a 1 - a k in some entry in u or y i #= a 1 - a k in some entry in v.
2. The #-projections are wrong.
(a) the first # in u di#ers from the first # in v;
(b) the last # in u di#ers from the last # in v;
(c) two #'s in u are the same;
(d) two #'s in v are the same; or
are successors in u but not in v.
The latter three conditions involve non-deterministic guesses of the positions where
the failure takes place.
3. The #-projections are wrong. This can be done in a completely analogous fashion.
4. w does not represent a solution:
(a) The #-value for some # in u is di#erent from the corresponding #-value in v.
(b) The a/b-value for some # in u is di#erent from the corresponding a/b-value
in v.
Clearly, w is not a solution i# one of these conditions holds. #
Corollary 19 Containment of 1N-RAs is undecidable.
The next question was also raised by Kaminski and Francez. In Section 3.2, we
observed that two-way RAs can simulate multi-head automata on strings of a special
shape. As non-emptiness of multi-head automata is undecidable the next proposition
easily follows.
Proposition 20 It is undecidable for a 2D-RA A whether
5.2 Pebble Automata
The next result implies that all standard decision problems are undecidable for all classes
of pebble automata.
Theorem 21 It is undecidable whether a weak 1D-PA is non-empty.
Proof. The weak 1D-PA A first checks whether the input is of the desired form and
then accepts if the input encodes a solution of the PCP instance. As pebbles can only be
moved to the right, we keep the first pebble on the first position and invoke subroutines
at that position which are then performed by the other pebbles. A puts the first pebble
down at the first position and then operates as follows.
1. A checks whether u and v are of the form (&#
a 1 - a k and y respectively, for all entries in u and v. This can be
achieved by one left to right scan of the second pebble. When reaching the end of
the string the pebble is simply lifted.
2. To check that w is syntactically correct, A further verifies the following.
(a) All #'s in u are di#erent: A places the second pebble on the first # and scans
the other #'s in u with the third pebble. If all are di#erent from the first one,
the second pebble is moved to the next # and the process is repeated.
(b) Checking that all #'s in v are di#erent is similar.
(c) The first # in u equals the first # in w: A puts the second pebble on the first
# and uses the third pebble to run to the first # in w.
(d) Checking that the last # in u equals the last # in w is similar.
are successors in u then they also are successors in v: this involves
four pebbles (numbered 2 to 5). The second pebble cycles through all # in u.
For each such value d, the automaton proceeds as follows. The third pebble is
placed on the # right after the second pebble. The fourth pebble then cycles
through the #-symbols in v until it finds d. If d is found, the fifth pebble is
placed on the # right after d and consistency can be checked. If this check
fails or d is not found in v then the input is rejected. Otherwise the three
most recent pebbles are removed.
(f) In an analogous way, it can also be verified that the #'s form an index.
3. To check that w represents a solution of the PCP instance A proceeds as follows.
(a) A checks that when x i is picked in u the corresponding choice in v is y i .
Hereto, the second pebble cycles through all # values of u. A keeps the
corresponding #-value in the finite memory, uses the third pebble to run to
the same # in v and checks whether the #-entry of the latter conforms to the
#-entry of the former.
(b) In an analogous way, A can also check that the a-values at corresponding
#-entry are the same.
This completes the description of the construction of A. It is straightforward to check
that A accepts an input if and only if it represents a solution of the PCP instance.
Hence the PCP instance has a solution if and only if L(A) is non-empty. #
6 Discussion
We investigated several models of computations for strings over an infinite alphabet.
One main goal was to identify a natural notion of regular language and corresponding
automata models. In particular, such a notion should agree in the finite alphabet case
with the classical notion of regular language. We considered two plausible automata
models: RAs and PAs. Our results tend to favor PAs as the more natural of the two.
Indeed, the expressiveness of PAs lies between FO # and MSO # . The inclusion of FO # provides
a reasonable expressiveness lower bound, while the MSO # upper bound indicates
that the languages defined by PAs remain regular in a natural sense. Moreover, strong
PAs are quite robust: all variants without alternation (one or two-way, deterministic or
non-deterministic) have the same expressive power.
Some of the results in the paper are quite intricate. The proofs bring into play a
variety of techniques at the confluence of communication complexity, language theory,
and logic. Along the way, we answered several questions on RAs left open by Kaminski
and Francez.
Several problems remain open:
(i) can weak 1D-PA or weak 1N-PA be simulated by 2D-RAs?
(ii are 1D-RA or 1N-RA subsumed by any pebble model? (We know that they can
be defined in MSO # . As 1N-RAs are hard for nlogspace they likely cannot be
simulated by 2D-PAs.)
(iii ) are weak 1N-PAs strictly more powerful than weak 1D-PAs?
(iv) are 2A-PAs strictly more powerful than 2N-PAs?



--R

Data on the Web

The Closure of Monadic NP.
XML with Data Values: Type-checking Revisited
A formal model for an expressive fragment of XSLT.
The Monadic Second-Order Logic of Graphs
Handbook of Formal Languages
Metafinite model theory.
Complexity results for two-way and multi-pebble automata and their logics
Limits to Parallel Computation.
Introduction to Automata Theory
Communication Complexity and Parallel Computing.
Algebraic and calculus query languages for recursively typed complex objects.



Structured document transformations based on XSL.
Type checking for XML transformers.
Extensions of attribute grammars for structured document queries.
Query automata.
Expressive and e

DTD inference for views of XML data.
On tape-bounded complexity classes and multihead finite au- tomata

--TR
Graph rewriting
Finite-memory automata
Limits to parallel computation
Complexity results for two-way and multi-pebble automata and their logics
Communication complexity and parallel computing
Languages, automata, and logic
Metafinite model theory
Temportal connectives versus explicit timestamps to query temporal databases
Alternation
Data on the Web
Intractability of decision problems for finite-memory automata
Typechecking for XML transformers
DTD inference for views of XML data
Expressive and efficient pattern languages for tree-structured data (extended abstract)
The closure of monadic NP
A Web Odyssey
XML with data values
On the power of walking for querying tree-structured data
Foundations of Databases
Query automata over finite trees
Introduction To Automata Theory, Languages, And Computation
A formal model for an expressive fragment of XSLT
Automata, Logic, and XML

--CTR
Michael Kaminski , Tony Tan, Regular Expressions for Languages over Infinite Alphabets, Fundamenta Informaticae, v.69 n.3, p.301-318, August 2006
Mikolaj Bojaczyk , Claire David , Anca Muscholl , Thomas Schwentick , Luc Segoufin, Two-variable logic on data trees and XML reasoning, Proceedings of the twenty-fifth ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems, June 26-28, 2006, Chicago, IL, USA
Stphane Demri , Ranko Lazi , David Nowak, On the freeze quantifier in Constraint LTL: Decidability and complexity, Information and Computation, v.205 n.1, p.2-24, January, 2007
Luc Segoufin, Static analysis of XML processing with data values, ACM SIGMOD Record, v.36 n.1, March 2007
Thomas Schwentick, Automata for XML---A survey, Journal of Computer and System Sciences, v.73 n.3, p.289-315, May, 2007
automata;expressiveness;first-order logic;monadic second-order logic;infinite alphabets;XML;registers;pebbles