Tree-Walking Automata and Monadic Second Order Logic

Jan-Pascal van Best

Preface

This report describes the results of a study in the field of theoretical computer science. It was written as my ``doctoraalscriptie'' (Master's thesis) for my study of Computer Science at Leiden University. The graduation tutor from the Department of Computer Science was J. Engelfriet, PhD.

This report was written using the L^AT_EX typesetting software on a computer running Linux and the KDE desktop environment.

I would like to thank Joost Engelfriet for his constant advice and his help in conducting this study. My parents have always supported me in many ways. And, last but certainly not least, thanks to Ellen for the title page she designed and for her love and support.

Jan-Pascal

Delft, July 1998

Preface
Introduction
1 Binary MSO Formulas and String-Walking Pebble Automata
    1.1 Preliminaries
    1.2 String-Walking Automata
    1.3 String-Walking Pebble Automata
    1.4 String-Walking Automata with MSO Tests
    1.5 From MSO Formulas to String-Walking Pebble Automata
    1.6 Another proof
    1.7 Pebble Necessity
    1.8 From String-Walking Pebble Automata to MSO Formulas
2 Extensions to String-Walking Pebble Automata
    2.1 String-Walking Multi-Pebble Automata
    2.2 From String-Walking Multi-Pebble Automata to MSO Formulas
    2.3 String-Walking Marble Automata
3 Binary MSO Formulas and Tree-Walking Automata
    3.1 Preliminaries
    3.2 Tree-Walking Automata
    3.3 Push-Down Tree-Walking Automata
    3.4 Equivalence of Finite Tree Automata and Push-Down Tree-Walking Automata
    3.5 Tree-Walking Marble Automata
    3.6 Tree-Walking Marble/Pebble Automata
    3.7 Tree-Walking Automata with MSO Tests
    3.8 Equivalence of Binary MSO Formulas and Tree-Walking Marble/Pebble Automata
Conclusion and Recommendations

Introduction

Monadic second order logic (MSO logic, [Büc60,,TW68]) is a way to describe properties of graphs. In this paper we will focus on strings and trees as special cases. Monadic second order logic combines great strength with great ease of expression. Closed MSO formulas define sets of trees, while MSO formulas with one or more unbound variables define node relations on trees. One perhaps less desirable property of MSO logic is that its formulas are global in a way that they define properties of trees as a whole. Another way to define node relations is by tree-walking automata. A tree-walking automaton can compute a binary node relation by starting on one node of the tree and finishing on another node. It has already been shown that tree-walking automata that can test unary MSO formulas at each node they visit, compute the same node relations that binary MSO formulas define [BE97]. However, these unary MSO formulas define in a way also global properties of the tree, in that they can test, e.g., the labels of several nodes of the tree they walk on in one formula. It can also be shown that ordinary tree-walking automata do not compute the same node relations that binary MSO formulas recognize. Therefore, in order to compute the node relations defined by binary MSO formulas, we need to extend tree-walking automata with features that make them more powerful. We need to make sure that these features result in only local operations, i.e., the resulting automata can, during their walk on a tree, only test properties of the current node. Also, we would like these operations to be more operational and less descriptive than unary MSO formulas. These considerations lead us to the central question of this paper.

Is it possible to define a type of tree-walking automaton, with only local operations, that computes the same binary node relations that binary MSO formulas recognize?

In this paper, we try to find an answer to this question. We start by attempting to find an answer for strings in Chapter 1. In this chapter, we introduce the concept of pebbles . During the walk of a string- or tree-walking automaton, the automaton can place a pebble on the current node. Later during its walk, the automaton can check for the presence of a pebble and pick it up. Variations are possible in the allowed number of pebbles, coloured pebbles and restriction in the use of pebbles. It is shown that string-walking pebble automata (with just one pebble) compute exactly the binary relations that binary MSO formulas define on strings. In the next chapter, we define some more powerful string-walking automata and show some of their properties. In Chapter 3, we move on to trees. The task of finding a proper extension for tree-walking automata proves to be a bit harder than for string-walking automata. Because it is already known [KS81] that push-down tree-walking automata recognize exactly the regular tree languages (which are the tree languages defined by closed MSO formulas), we develop tree-walking marble automata, similar in concept to push-down tree-walking automata, that also recognize exactly the regular tree languages but, unlike push-down tree-walking automata, allow for a natural definition of the computation of node relations. By adding one pebble, we obtain tree-walking marble/pebble automata. We show that these compute exactly the binary node relations that binary MSO formulas define on trees. In the last chapter, we conclude this paper and give some recommendations for future research.

Chapter 1
Binary MSO Formulas and String-Walking Pebble Automata

1.1 Preliminaries

In this section we recall some well-known concepts from formal language theory [HU79,], more specifically concerning strings, finite automata and monadic second order logic (on strings). Before doing so, we recall some standard terminology from set theory.

The set of natural numbers is \mathbb N = {0,1,2,¼} and, for m,n Î \mathbb N, [m,n] = { i Î \mathbb N \mid m £ i £ n}. For a set S, 2^S is its powerset, i.e., the set of all subsets of S. Let R Í A ×B be a binary relation. The transitive reflexive closure of R is denoted R^*. The inverse of R is R^-1 = { (y,x) \mid (x,y) Î R }. For two binary relations R₁ and R₂, their composition is R₁ °R₂ = {(x,z) \mid $y: (x,y) Î R₁ and (y,z) Î R₂ }. Note that the order of R₁ and R₂ is nonstandard. For each a Î A, R(a) = { b Î B \mid (a,b) Î R } and for each S Í A, R(S) = È{ R(a) \mid a Î S }. The domain of R is dom(R) = R^-1(B). A binary relation R is functional if it is a partial function, i.e., (x,y),(x,z) Î R implies x = z.

Let f:A® B be a function; for any a and b, f(a® b) denotes the ``perturbed'' function f¢:A È{a} ® B È{b} with f¢(a) = b and f¢(a¢) = f(a¢) for every a¢ Î A with a¢ ¹ a.

Strings

An alphabet is a finite set of symbols. Let S be an alphabet. A string over S is a finite string of symbols from S. The empty string is denoted l. The set of all strings over S is denoted S^*. A subset of S^* is called a language. If w is a string over S, |w| denotes the length of w. The set of positions in w is denoted by V_w = [1,|w|]. For a string w Î S^* and i Î V_w, we write lab_w(i) = s if the ith symbol of w is s. For k Î \mathbb N, a k-ary position relation over S is a subset of {(w,u₁,¼,u_k) \mid w Î S^* and u_i Î V_w for all i Î [1,k] }. A k-ary position relation associates with each string w a k-ary relation on the positions of w.

We define marked strings as follows. Let S be an alphabet, and k ³ 1. We define B_k = {0,1}^k \{0}^k. The alphabet SÈ(S×B_k) contains all symbols s Î S and the symbols (s, b₁, ¼, b_k) with b_i Î {0,1} for all i Î [1,k], but without (s, 0, ¼, 0). The role of the latter symbol is played by s itself. This alphabet is used to attach k different marks to the positions in a string. Let w Î S^* be a string over S, and let u₁, ¼, u_k Î V_w. The marked string w¢ = mark(w, u₁, ¼, u_k) Î (SÈ(S×B_k))^* is the string with lab_w¢(u) = lab_w(u) if u ¹ u_i for all i Î [1,k], and lab_w¢(u) = (lab_w(u), (u = u₁), ¼, (u = u_k)) otherwise (where (u = u_i) = 1 iff u equals u_i).

Finite Automata

Let S be an alphabet. A finite automaton over S is a quintuple M = (Q,S,d,I,F), where Q is a finite set of states, S is the input alphabet, d Í Q ×S×Q is the transition relation, I Í Q is the set of initial states and F Í Q is the set of final states. The elements of d are called transitions. For every string w Î S^*, the state transition relation R_M(w) Í Q ×Q is defined as follows. For s Î S, R_M(s) = { (p,q) \mid (p,s,q) Î d}. For s₁,¼,s_n Î S, R_M(s₁¼s_n) = R_M(s₁)°¼°R_M(s_n). The language recognized by M is L(M) = { w Î S^* \mid (q_in,q_fin) Î R_M(w) for some q_in Î I, q_fin Î F }. A language is regular if it is recognized by a finite automaton. The class of all regular languages is named REG.

Monadic Second Order Logic (on strings)

Monadic second order logic can be used to describe properties of strings [Büc60]. For an alphabet S, we define the language MSOL(S) of MSO formulas over S. This language has position variables x,y,¼ and position-set variables X,Y,¼. For a given string w Î S^*, position variables range over V_w = [1,|w|] and position-set variables range over the subsets of V_w.

There are three types of atomic formulas in MSOL(S): lab_s(x), for every s Î S, signifies that at position x there is a symbol s. When MSO logic is expanded to describe properties of trees and graphs, lab_s(x) means that node x is labeled s, hence the name lab_s. The atomic formula pre(x,y) signifies that position x comes directly before y, i.e. y = x+1; and x Î X signifies that x is an element of X. The connectives used to build formulas from these atomic formulas are Ø, Ù, Ú, ®, «, with the usual meaning. Both position variables and position-set variables can be quantified with $ and ". We will make use of the following abbreviations of MSO formulas:

head(x)

"y(Øpre(y,x))

tail(x)

"y(Øpre(x,y))

true(x)

$X(x Î X)

false(x)

Øtrue(x)

If an MSO formula f has free variables, say x, y, X and no others, we write f(x,y,X) to indicate the free variables of f. For every k Î \mathbb N, the set of MSO formulas over S with k free position variables and no free position-set variables is denoted MSOL_k(S), or the set of k-ary MSO formulas. For a closed formula f Î MSOL₀(S) and a string w Î S^*, we write w \models f if w satisfies f. The language defined by f is L(f) = { w Î S^* \mid w \models f}. L(f) is called an MSO definable language . The class of all MSO definable languages is named MSO.

Given a string w, a valuation function n is a function that maps each position variable to a position u Î V_w and each position-set variable to a subset U of V_w. Let f be an MSO formula. We write (w,n) \models f, if f holds in w, where the free variables of f are assigned values according to the valuation function n. If f has free variables x,y,X, we write (w,u,v,U) \models f(x,y,X) for (w,n) \models f, where n(x) = u, n(y) = v and n(X) = U.

Let f(x₁, ¼, x_k) Î MSOL_k(S) be an MSO formula with k free positions variables (and no free position-set variables). For each string w Î S^*, the k-ary relation that f defines on the positions of w is

R_w(f) = { (u₁, ¼, u_k) Î V_w^k \mid (w, u₁, ¼, u_k) \models f(x₁, ¼, x_k) } .

The MSO formula f(x₁, ¼, x_k) defines the position relation

R(f) = { (w, u₁, ¼, u_k) \mid w Î S^*, (u₁, ¼, u_k) Î R_w(f) } .

Büchi [Büc60] proved the following classical result.

Proposition 1 A language is MSO definable if and only if it is regular.

In [BE97], the following (well-known) results are proven for MSO formulas on trees. They also hold for the special case of strings. Corollary 3 is the result of Lemma 2 in the case j = k.

Lemma 2 Let S be an alphabet, k ³ 1, and j Î [1,k]. For every formula f(x₁, ¼, x_k) Î MSOL_k(S) there is a formula y(x_j+1, ¼, x_k) Î MSOL_k-j(SÈ(S×B_j)) such that, for all w Î S^* and u₁, ¼, u_k Î V_w,

(w, u₁, ¼, u_k) \models f(x₁, ¼, x_k) iff (mark(w, u₁, ¼, u_j), u_j+1, ¼, u_k) \modelsy(x_j+1, ¼, x_k),

and vice versa, i.e., for every formula y(x_j+1, ¼, x_k) Î MSOL_k-j(SÈ(S×B_j)) there is a formula f(x₁, ¼, x_k) Î MSOL_k(S) such that the above equivalence holds for all w Î S^* and u₁, ¼, u_k Î V_w.

Corollary 3 Let S be an alphabet and k ³ 1. For every formula f(x₁, ¼, x_k) Î MSOL_k(S) there is a formula y Î MSOL₀(SÈ(S×B_k)) such that, for all w Î S^* and u₁, ¼, u_k Î V_w,

(w, u₁, ¼, u_k) \models f(x₁, ¼, x_k) iff mark(w, u₁, ¼, u_k) \models y,

and vice versa, i.e., for every MSO formula y Î MSOL₀(SÈ(S×B_k)) there is a formula f(x₁, ¼, x_k) Î MSOL_k(S) such that the above equivalence holds for all w Î S^* and u₁, ¼, u_k Î V_w.

From Corollary 3 and Proposition 1 follows the following lemma.

Lemma 4 Let S be an alphabet and let k ³ 1. For every MSO formula f(x₁, ¼, x_k) Î MSOL_k(S) there exists a finite automaton M over SÈ(S×B_k) such that, for all w Î S^* and u₁, ¼, u_k Î V_w,

(w, u₁, ¼, u_k) \models f(x₁, ¼, x_k) iff mark(w, u₁, ¼, u_k) Î L(M) .

1.2 String-Walking Automata

String-walking automata are known in the literature as two-way finite automata (see [HU79]). We will call them string-walking automata to stress both the differences and the similarities with tree-walking automata. String-walking automata are like the well-known finite automata, except that they can walk both forwards and backwards along the string they are examining (hence the name two-way finite automata). At any moment in the execution of a string-walking automaton, the automaton is in one state and at one position of the string. Let S be an alphabet. Syntactically, a string-walking automaton over S is a finite automaton with a special set of directives as input alphabet. We define the set of directives as

D_SWA(S) = { ¬, ®, head, Øhead, tail, Øtail} È{ lab_s\mid s Î S} .

The meaning of the directives is as follows:

¬ means go back to the previous position in the input string.
® means go to the next position in the input string.
head checks whether the current position is the first position in the string.
tail checks whether the current position is the last position in the string.
Øhead and Øtail are the negations of head and tail respectively.
lab_s checks whether the current position is labeled with s.

Formally, we define for each string w Î S^* and each directive d Î D_SWA(S) the following binary relation R_w(d) on V_w:

R_w(¬)

{ (i, i-1) \mid 1 < i £ |w| }

R_w(®)

{ (i, i+1) \mid 1 £ i < |w| }

R_w(lab_s)

{ (i, i) \mid 1 £ i £ |w| and the ith symbol of w is s }

R_w(head)

{ (1, 1) }

R_w(Øhead)

{ (i, i) \mid 1 < i £ |w| }

R_w(tail)

{ (n, n) \mid n = |w| }

R_w(Øtail)

{ (i, i) \mid1 £ i < |w| }

A string-walking automaton over S is a finite automaton A over D_SWA(S). For a string-walking automaton A = (Q,D_SWA(S), d, I, F) and a string w Î S^*, an element (q,u) of Q ×V_w is a configuration of the automaton. The configuration (q,u) Î Q ×V_w signifies that A is in state q at position u. We say that the current position of the automaton on w is u. The set of all configurations of A and w is denoted by \mathbb C_A,w.

Let w Î S^*. One step of A = (Q,D_SWA(S),d,I,F) on w is defined by the binary relation \twoheadrightarrow_A,w on the set of configurations, as follows. For every (q,u), (q¢,u¢) Î \mathbb C_A,w,

(q,u) \twoheadrightarrow_A,w (q¢,u¢) iff $d Î D_SWA(S): (q,d,q¢) Î d and (u,u¢) Î R_w(d) .

For each string w Î S^*, A computes the binary relation

R_w(A) = { (u,v) Î V_w ×V_w \mid (q,u) \twoheadrightarrow_A,w^*(q¢,v) for some q Î I and q¢ Î F } .

Thus, A computes the position relation

R(A) = { (w,u,v) \mid w Î S^*, (u,v) Î R_w(A) } .

We define the language that A recognizes as all strings w with the property that there is a walk of A on w starting at the beginning of the string in an initial state and ending in a final state, or

L(A) = { w Î S^* \mid there exists v Î V_w such that (1,v) Î R_w(A)} .

The class of all languages recognized by a string-walking automaton is named SWA.

In the following we will also allow transitions of the form (p,s,q) with s Î D_SWA(S)^*. If s = d₁ d₂ ¼d_n, we define, for all w Î S^*,

R_w(s) = R_w(d₁) °¼°R_w(d_n).

These extended directives can easily be implemented by adding extra transitions and states.

A string-walking automaton A = (Q,D_SWA(S),d,I,F) over S is deterministic if the following three conditions hold:

#I = 1.
If (p,d,q) Î d, then p \not Î F.
For all distinct transitions (p,d₁,q₁), (p,d₂,q₂) Î d, d₁ and d₂ are two mutually exclusive directives in D_SWA(S).

Two directives d₁,d₂ Î D_SWA(S) are mutually exclusive exactly if, for all w Î S^* and u Î V_w, dom(R_w(d₁)) Çdom(R_w(d₂)) = Æ. The following pairs of directives in D_SWA(S) are mutually exclusive:

{®,tail},{¬,head}
{head,Øhead},{tail,Øtail}
{lab_s₁,lab_s₂} with s₁ ¹ s₂

1.3 String-Walking Pebble Automata

We will extend the concept of string-walking automata with a pebble [BH65]. A string-walking pebble automaton is able to drop its pebble at its current position in the string, pick it up at any (later) time, if it is at the same position again, and check whether or not the pebble is present at the automaton's current position. Let S be an alphabet. The directives for a string-walking pebble automaton are

D_SWPA(S)

D_SWA(S)È{ put, lift, here, Øhere}

{ ¬, ®, head, Øhead, tail, Øtail, put, lift, here, Øhere} È{ lab_s\mid s Î S}

The meaning of the new directives is as follows:

put means drop the pebble at the current position in the string.
lift means lift the pebble from the current position in the string (only if it is there now).
here checks whether the pebble is at the current position.
Øhere is the negation of here.

For all strings w Î S^*, we will denote the pebble positions with elements of P_w = V_w È{^}. Here ^ denotes that the pebble is not placed at any position of the string, i.e., the automaton ``carries'' the pebble. We now need to extend the binary relations R_w(d) (for d Î D_SWA(S)) to be on pairs (u,p) Î V_w ×P_w to take pebble-handling into account. Let, for all strings w Î S^* and directives d Î D_SWA(S), [R\tilde]_w(d) denote the binary relation R_w(d) as defined for string-walking automata in the previous section. We now define R_w(d) for string-walking pebble automata as follows:

R_w(d) = { ((i,p),(i¢,p)) \mid (i,i¢) Î

~
R

(d) and p Î P_w } .

This means that the directives from D_SWA(S) do not alter the pebble position.

The relations for the new directives are as follows.

R_w(put)

{ ((i,^), (i, i)) \mid 1 £ i £ |w|}

R_w(lift)

{ ((i, i), (i, ^)) \mid 1 £ i £ |w|}

R_w(here)

{ ((i, i), (i, i)) \mid 1 £ i £ |w|}

R_w(Øhere)

{ ((i,p), (i,p)) \mid1 £ i £ |w| and p ¹ i }

Let S be an alphabet. A string-walking pebble automaton is a finite automaton A over D_SWPA(S). For a string-walking pebble automaton A = (Q,D_SWPA(S), d, I, F) and a string w Î S^*, an element (q,u,p) Î Q ×V_w ×P_w is a configuration of the automaton. The set of all configurations of A and w is denoted by \mathbb C_A,w. A configuration (q,u,p) signifies that A is in state q at position u, while the pebble is at position p.

The step relation \twoheadrightarrow_A,w is extended in the obvious way. For a string-walking pebble automaton A, a string w Î S^* and configurations (q,u,p),(q¢,u¢,p¢) Î \mathbb C_A,w,

(q,u,p) \twoheadrightarrow_A,w^* (q¢,u¢,p¢) iff $d Î D_SWPA(S): (q,d,q¢) Î d and ( (u,p),(u¢,p¢) ) Î R_w(d).

For the relation that A computes, we now demand that A begins and ends with the pebble not on the string, or ``in its pocket''. For w Î S^*,

R_w(A) = { (u,v) Î V_w ×V_w \mid (q,u,^) \twoheadrightarrow_A,w^*(q¢,v,^) for some q Î I and q¢ Î F }.

The definitions of R(A) and L(A) remain the same. The class of all languages recognized by a string-walking pebble automaton is named SWPA.

Transitions of the form (p,s,q) with s Î D_SWPA(S)^* are treated as with string-walking automata. The definition of a deterministic string-walking pebble automaton is similar to that of a deterministic string-walking automaton. The only difference is that the directives are now taken from D_SWPA(S). The following pairs of directives in D_SWPA(S) are mutually exclusive:

{®,tail},{¬,head}
{here,put},{lift,put},{Øhere,lift}
{head,Øhead},{tail,Øtail},{here,Øhere}
{lab_s₁,lab_s₂} with s₁ ¹ s₂

1.4 String-Walking Automata with MSO Tests

Another way to extend string-walking automata (as done in [BE97] for tree-walking automata, see also Section 3.7) is to allow the automaton to test any MSO definable property of the current position of the string, using MSO formulas with one free position variable. This extension also requires the introduction of new directives. Let S be an alphabet. The set of directives over S is

D_SWA+M(S) = { ¬, ®} ÈMSOL₁(S) .

Note that head, tail, lab_s, etc. are MSO definable properties so they need not be explicitely stated in the definition of D_SWA+M(S). Note also that D_SWA+M(S) is an infinite set. Therefore we need to define for each string-walking automaton with MSO tests a finite subset of D_SWA+M(S) as the directives used by the automaton. For the directive d = y(x) with y Î MSOL₁(S), we define the following binary relation on V_w (w Î S^*):

R_w(y(x)) = {(i,i) \mid (w,i) \models y(x) } .

A string-walking automaton with MSO tests over S is a finite automaton A over a finite subset of D_SWA+M(S). The definitions of configurations, \twoheadrightarrow_A,w, R_w(A), etc. are unchanged with respect to the definitions for (ordinary) string-walking automata. The definitions of deterministic string-walking automata and mutually exclusive directives are also unchanged, although it is no longer possible to list all mutually exclusive pairs of directives. Note that it is decidable whether a given pair of directives in MSOL₁(S) is mutually exclusive.

The class of all languages recognized by a string-walking automaton with MSO tests is named SWA+M.

In [BE97] the following results are proven for trees. They also hold for the special case of strings.

Proposition 5 The following three statements hold:

SWA+M=REG
For every alphabet S and every binary MSO formula f(x,y) Î MSOL₂(S), there exists a string-walking automaton with MSO tests A such that R(A) = R(f).
For every alphabet S and every string-walking automaton with MSO tests A over S, there exists a binary MSO formula f(x,y) Î MSOL₂(S) such that R(f) = R(A).

1.5 From MSO Formulas to
String-Walking Pebble Automata

Both MSO formulas with two position variables and string-walking pebble automata compute binary position relations. In this section, we show that every binary position relation that can be defined by an MSO formula, can also be computed by a string-walking pebble automaton. In Section 1.8 we will show that the reverse is also true, i.e., every binary position relation that can be computed by a string-walking pebble automaton can also be defined by a binary MSO formula.

Let S be an alphabet and let f(x,y) be a binary MSO formula over S. We have seen (Lemma 4) that there exists a finite automaton M over SÈ(S×B₂) such that, for all w Î S^* and u,v Î V_w,

(w,u,v) \models f(x,y) iff mark(w,u,v) Î L(M) .

The following lemma states that there is a string-walking pebble automaton that computes the same relation as f(x,y) defines.

Lemma 6 For every finite automaton M over SÈ(S×B₂) there exists a string-walking pebble automaton A over S such that, for all w Î S^* and u,v Î V_w,

mark(w,u,v) Î L(M) iff (u,v) Î R_w(A).

Proof. Let M = (Q_M,SÈ(S×B₂), d_M, I_M, F_M) be a finite automaton over SÈ(S×B₂). We will define a string-walking pebble automaton over S, A, that simulates M, using the pebble to simulate the marked positions in M. A is defined as the (intuitive) union of three automata A₁, A₂, A₃. We define A as (Q₁ ÈQ₂ ÈQ₃, D_SWPA(S), d₁ Èd₂ Èd₃, I₁ ÈI₂ ÈI₃, F₁ ÈF₂ ÈF₃). A₁ deals with the case that u comes ``before'' v in w, A₂ deals with the case that v comes first and A₃ deals with the case u = v. For 1 £ i £ 3, A_i = (Q_i, D_SWPA(S), d_i, I_i, F_i).

A₁ simulates M, assuming that u comes before v in w. A₁ first drops its pebble at the start position u. This makes it possible to determine later where the automaton started. Then it walks to the head of the string. Next it simulates M in three stages. In the first stage of the simulation, it simulates M (only taking into account transitions of the form (p,s,q) with s Î S) until it finds the pebble. It picks up the pebble and treats the symbol s on this position as (s,1,0) in M. The automaton now continues simulating M (the second stage of the simulation), again without transitions with labels in S×B₂. Then, nondeterministically, A₁ drops the pebble at some position v and treats the symbol s at this position as (s,0,1) in M. A continues simulating M (the third stage) until it reaches the end of the string. If it reaches the end of the string in a final state of M, the choice for v was a good choice. The automaton then backs up until it finds the pebble at position v. This ends A₁.

We use the following states in A₁.

in₁ is the initial state.
tobegin₁ is used to walk to the head of the string.
q_1,i (for q Î Q_M) is used in the ith stage of the simulation.
backup₁ is used to back up to v after the three stages of simulation.
final₁ is the final state.

Formally, A₁ = (Q₁, D_SWPA(S), d₁, I₁, F₁) is constructed as follows:

Q₁

{ in₁, tobegin₁, backup₁, final₁ } È

{ q_1,i \mid q Î Q_M, 1 £ i £ 3 }

d₁

{ (in₁, put, tobegin₁),(tobegin₁, ¬, tobegin₁) } È

{ (tobegin₁, head, q_1,1) \mid q Î I_M } È

{ (p_1,1, (lab_s, ®), q_1,1)\mid (p,s,q) Î d_M } È

{ (p_1,1, (lift, lab_s, ®), q_1,2) \mid(p,(s,1,0),q) Î d_M } È

{ (p_1,2, (lab_s, ®), q_1,2)\mid (p,s,q) Î d_M } È

{ (p_1,2, (put, lab_s, ®), q_1,3) \mid(p,(s,0,1),q) Î d_M } È

{ (p_1,2, (put, lab_s, tail), backup₁) \mid(p,(s,0,1),q_fin) Î d_M for some q_fin Î F_M } È

{ (p_1,3, (lab_s, ®), q_1,3)\mid (p,s,q) Î d_M } È

{ (p_1,3, (lab_s, tail), backup₁)\mid (p,s,q_fin) Î d_M for some q_fin Î F_M } È

{ (backup₁, ¬, backup₁), (backup₁, lift, final₁) }

I₁

{in₁}

F₁

{ final₁ }

A₂ is similar to A₁, only here the automaton, after dropping its pebble on u, first walks to the right until the end of the string, then simulates M (inverted), starting in a state corresponding to a state in F_M, until it finds the pebble at u. It picks up the pebble and treats the symbol s at this position as (s,0,1) in M. A₂ continues with the second stage of the simulation. Then, nondeterministically, A₂ drops the pebble at some position v and continues with the third stage of the simulation until the beginning of the string. If it reaches the beginning of the string in an initial state of M, A₂ walks back to the pebble at v and the simulation is finished.

Formally, A₂ = (Q₂, D_SWPA(S), d₂, I₂, F₂) is constructed as follows:

Q₂

{ in₂, toend₂, backup₂, final₂ } È

{ q_2,i \mid q Î Q_M, 1 £ i £ 3 }

d₂

{ (in₂, put, toend₂),(toend₂, ®, toend₂) } È

{ (toend₂, tail, q_2,1) \mid q Î F_M } È

{ (q_2,1, (lab_s, ¬), p_2,1)\mid (p,s,q) Î d_M } È

{ (q_2,1, (lift, lab_s, ¬), p_2,2) \mid(p,(s,1,0),q) Î d_M } È

{ (q_2,2, (lab_s, ¬), p_2,2)\mid (p,s,q) Î d_M } È

{ (q_2,2, (put, lab_s, ¬), p_2,3) \mid(p,(s,0,1),q) Î d_M } È

{ (q_2,2, (put, lab_s, head), backup₂) \mid(p,(s,0,1),q_in) Î d_M for some q_in Î I_M } È

{ (q_2,3, (lab_s, ¬), p_2,3)\mid (p,s,q) Î d_M } È

{ (q_2,3, (lab_s, head), backup₂)\mid (p,s,q_in) Î d_M for some q_in Î I_M } È

{ (backup₂, ®, backup₂), (backup₂, lift, final₂) }

I₂

{in₂}

F₂

{ final₂ }

A₃ looks again like the previous two parts of A. A₃ however assumes that u = v, which implies that the only useful transitions with labels in S×B₂ are the ones of the form (p,(s,1,1),q) Î d_M. So A₃ first drops its pebble at position u ( = v), then (like A₁) walks to the head of the string and simulates M until it gets to the starting position (the pebble) again. It does not lift the pebble, because it needs to know the position of u = v. A₃ treats the symbol s at this position as (s,1,1) in M. Then it continues with the second stage of the simulation of M until the end of the string. If it arrives there in a final state of M, A₃ backs up to the pebble which ends the simulation of M.

Formally, A₃ = (Q₃, D_SWPA(S), d₃, I_A, F_A) is constructed as follows:

Q₃

{ in₃, tobegin₃, backup₃, final₃ } È

{ q_3,i \mid q Î Q_M, 1 £ i £ 2 }

d₃

{ (in₃, put, tobegin₃),(tobegin₃, ¬, tobegin₃) } È

{ (tobegin₃, head, q_3,1) \mid q Î I_M } È

{ (p_3,1, (lab_s, ®), q_3,1)\mid (p,s,q) Î d_M } È

{ (p_3,1, (here, lab_s, ®), q_3,2) \mid(p,(s,1,1),q) Î d_M } È

{ (p_3,1, (here, lab_s, tail), backup₃) \mid(p,(s,1,1),q_fin) Î d_M for some q_fin Î F_M } È

{ (p_3,2, (lab_s, ®), q_3,2)\mid (p,s,q) Î d_M } È

{ (p_3,2, (lab_s, tail), backup₃)\mid (p,s,q_fin) Î d_M for some q_fin Î F_M} È

{ (backup₃, ¬, backup₃), (backup₃, lift, final₃) }

I₃

{in₃}

F₃

{ final₃ }

\square

Using this lemma the following theorem becomes trivial to prove.

Theorem 7 For each formula f(x,y) Î MSOL₂(S), there exists a string-walking pebble automaton A over S such that R(f) = R(A).

1.6 Another proof

There is another way to prove Theorem 7. This method makes use of Proposition 5 to simulate the binary MSO formula by a string-walking automaton with MSO tests. The MSO tests are then simulated by making use of a pebble. Let S be an alphabet, and let f(x,y) Î MSOL₂(S) be an MSO formula with two free position variables. Then there exists a string-walking automaton with MSO tests A = (Q_A,D_A,d_A,I_A,F_A) with D_A a finite subset of D_SWA+M(S) such that R(f) = R(A) (Proposition 5). We will construct a string-walking pebble automaton A¢ = (Q¢,D_SWPA(S),d¢,I¢,F¢) such that R(A¢) = R(A) = R(f). We need the following result, which is Lemma 4 for the case k = 1.

Lemma 8 Let S be an alphabet. For every MSO test y(x) Î MSOL₁(S), there exists a finite automaton M over SÈ(S×B₁) such that, for all w Î S^* and u Î V_w,

(w,u) \models y(x) iff mark(w,u) Î L(M) .

We now construct A¢. In first approximation, A¢ equals A for transitions (p,d,q) with d Î { ¬, ® }. We define T = {(p,d,q) Î d_A \mid d Î MSOL₁(S)}, the collection of all transitions with MSO tests in A. For each transition t = (p,y(x),q) Î T, we use Lemma 8 to construct the finite automaton M_t that calculates the MSO test y(x). We will use this automaton to construct a ``subroutine'' in A¢ that simulates t. The idea is as follows, similar to the construction of A₃ in the proof of Lemma 6. A¢ first drops its pebble. Then it walks to the head of the string. From there, it checks the MSO test by following M_t. Any transitions in d_{M_t} with labels not in S are handled by using the pebble. The only possible form of such a transition is (p,(s,1),q). In place of this transition, we add transitions to check whether the position in the string where the automaton is now is marked, i.e., the pebble is there. Then the symbol s is checked and the automaton moves on to the next position in the string in state q. If M_t reaches a final state at the end of the string, A¢ moves back to the position where it dropped the pebble and lifts it. At this moment the MSO test y(x) is successfully verified by the automaton.

The following states are used for A¢. First, all states from A, Q_A. Then we need extra states for each MSO test. For all transitions t Î T we use, next to the states of M_t, tobegin_t to move to the beginning of the string and backup_t to back up to the pebble, the place where the simulation of M_t started. We assume that all the M_t for all t Î T have unique states that do not overlap with either Q_A or states of other M_t's.

Formally, A¢ = (Q¢,D_SWPA(S),d¢,I¢,F¢) is constructed as follows:

Q¢

Q_A È{ tobegin_t, backup_t \mid t Î T }È

È
t Î T

Q_{M_t}

I¢

I_A

F¢

F_A

d¢

{ (p,d,q) Î d_A \midd Î {¬,®} } È

{ d_t \mid t Î T }

Here the transitions needed to simulate t = (p,y(x),q) are as follows:

d_t

{ (p, put, tobegin_t),(tobegin_t, ¬, tobegin_t)} È

{ (tobegin_t, head, s_in)\mid s_in Î I_{M_t} } È

{ s,(Øtail, Øhere, lab_s,®),t) \mid (s,s,t) Î d_{M_t} } È

{ s,(Øtail,here,lab_s,®),t) \mid (s,(s,1),t) Î d_{M_t} } È

{ s,(tail,Øhere,lab_s),backup_t) \mid (s,s,t_fin) Î d_{M_t} for some t_fin Î F_{M_t} } È

{ s,(tail, here,lab_s),backup_t) \mid (s,(s,1),t_fin) Î d_{M_t} for some t_fin Î F_{M_t} } È

{ (backup_t, (Øhere, ¬), backup_t),(backup_t, lift, q) }

1.7 Pebble Necessity

The following theorem states that we really need the pebble in Theorem 7. The proof of this theorem is a simpler form of the proof for tree-walking automata (Theorem 15 in [BE97]). It is included here for completeness.

Theorem 9 There exist an alphabet S and a formula f(x,y) Î MSOL₂(S) such that there is no string-walking automaton A with R(A) = R(f).

Proof. We construct an MSO formula f(x,y) Î MSOL₂(S) with S = {b,r}, denoting black and red. For a string w over S, the binary relation R(f) connects certain positions of w. If w has exactly one position with symbol r, say v_red, then R(f) will connect any position to v_red. Otherwise, i.e., if there is no red symbol or more than one, R(f) will connect any position to the next in left-to-right circular order. We use the following abbreviations to define f(x,y):

ors

$y ( lab_r(y) Ù"z(lab_r(z) ® z = y))

succ(x,y)

pre(x,y) Ú( tail(x) Ùhead(y) )

f(x,y)

( orsÙlab_r(y) ) Ú( ØorsÙsucc(x,y) )

Here ors is a closed MSO formula which is true if there is exactly one red symbol in w, and succ(x,y) is an MSO formula which is true if y follows x in left-to-right circular order. Clearly, f(x,y) is a binary MSO formula with R(f) as indicated above.

Now we will show that there is no string-walking automaton A = (Q,D_SWA(S),d,I,F) with R(A) = R(f). Suppose that such an A exists. We may assume that I = {q_in}. The idea is that when A starts at any position u of a string with only b's, it first has to visit all positionsc of the string to check there is no r in the string. Because there is no way for A to remember its starting point u, A also cannot find the position after u in left-to-right circular order.

Let w be b^#Q+1, a string of #Q+1 black symbols. Let w¢ be rb^#Q. Thus, w¢ is w with the first symbol changed to red. We will use the following function:

succ(k) =

ì
í
î

k+1

if k £ #Q

otherwise (k = #Q+1)

which gives the successor to position k in left-to-right circular order. Because w does not contain a symbol r, there exists for every k Î [1,#Q+1] a state f_k Î F such that

(q_in,k) \twoheadrightarrow_A,w^* (f_k, succ(k)) .

On the other hand, because w¢ contains exactly one symbol r, for all k Î [1,#Q], there is no state f Î F such that

(q_in,k) \twoheadrightarrow_A,w¢^* (f, succ(k)) .

This difference implies that for all k Î [1, #Q] the walk of A on w from k to succ(k) must visit position 1, because the only different symbol is the first, which is black for w and red for w¢. Because the walk of A on w from #Q+1 to 1 also visits position 1, there is for all k Î [1,#Q+1] a q_k Î Q such that

(q_in,k) \twoheadrightarrow_A,w^* (q_k,1) \twoheadrightarrow_A,w^* (f_k,succ(k)) .

There are #Q+1 possibilities for k and only #Q states, which means there are k,k¢ Î [1,#Q+1] with k ¹ k¢ and q_k = q_k¢. Then

(q_in,k) \twoheadrightarrow_A,w^* (q_k,1) = (q_k¢,1) \twoheadrightarrow_A,w^* (f_k¢,succ(k¢)) .

This implies that A walks from k both to succ(k) and to succ(k¢) with k ¹ k¢, a contradiction to the fact that R(A) = R(f). \square

1.8 From String-Walking Pebble Automata to
MSO Formulas

In this section we will prove that a string-walking pebble automaton can be simulated by a string-walking automaton with MSO tests. Because it is already known that these automata can be simulated by binary MSO formulas (Proposition 5), and because we have shown in previous sections that a binary MSO formula can be simulated by a string-walking pebble automaton, we obtain the equivalence of binary MSO formulas and string-walking pebble automata.

To prove that it is possible to simulate the use of a pebble with MSO tests, we will need the following lemma. In the lemma, A is a string-walking pebble automaton that is not allowed to move its pebble, but it is allowed to check the presence of the pebble at the current position. The lemma states that the round-trip of A from the position where the pebble is, back to that position can be simulated by a unary MSO formula.

Lemma 10 Let A be a string-walking pebble automaton, with no transitions with directives put or lift, over S. Then, for every pair of states p,q Î Q_A, there exists a formula y_pq(x) Î MSOL₁(S) such that, for all w Î S^* and x Î V_w,

(p,x,x) \twoheadrightarrow_A,w^* (q,x,x) iff (w,x) \models y_pq(x) .

Proof. Let A be a string-walking pebble automaton over S without put and lift. Let p,q Î Q_A. First note that the pebble does not move during A's walk. We can therefore consider the pebble position a constant and mark it using a special symbol (s,1) where s is the original symbol at the pebble position. We will now define a string-walking automaton A¢ (without pebble) over SÈ(S×B₁) that simulates the walk of A from the pebble position and back. We define A¢ = (Q_A, D_SWA(SÈ(S×B₁)), d¢, {p}, {q}). Thus, the states of A¢ are the same as those of A, A¢'s initial state is p, and its final state is q. Furthermore, d¢ consists of the following transitions:

d¢

d_A Ç(Q_A ×D_SWA(S)×Q_A) È

{ (s,lab_(s,1),t) \mid (s,here,t) Î d_A, s Î S} È

{ (s,lab_s,t) \mid (s,Øhere,t) Î d_A, s Î S} È

{ (s,lab_(s,1),t) \mid(s,lab_s,t) Î d_A, s Î S}.

The directive ``here'' is simulated by checking whether the symbol at the current position is in S×B₁. Similarly, ``Øhere'' is simulated by checking whether the symbol at the current position is in S. Otherwise, the new symbols from S×B₁ are treated just like the corresponding symbols from S. Now, for all s,t Î Q_A, w Î S^* and x,y,z Î V_w, it is easy to see that

(s,x,z) \twoheadrightarrow_A,w^* (t,y,z) iff (s,x) \twoheadrightarrow_A¢,w¢^* (t,y)

where w¢ = mark(w,z). This means that A¢ on a string marked at position z walking from x to y simulates A on the unmarked string with the pebble at position z. Both automata start in state s and end in state t. Also, from the definition of R_w¢(A¢),

(p,x) \twoheadrightarrow_A¢,w¢^* (q,y) iff (x,y) Î R_w¢(A¢) .

According to Proposition 5 we can construct a formula f¢_pq(x,y) Î MSOL₂(SÈ(S×B₁)) that simulates the walk of A¢ on a marked string, so that, for all w Î S^*, x,y,z Î V_w and w¢ = mark(w,z),

(x,y) Î R_w¢(A¢) iff (w¢,x,y) \models f¢_pq(x,y) .

Using Lemma 2 yields a formula f_pq(x,y,z) Î MSOL₃(S) such that, for all w Î S^* and x,y,z Î V_w,

(mark(w,z),x,y) \models f¢_pq(x,y) iff (w,x,y,z) \models f_pq(x,y,z) .

We now define y_pq(x) = f_pq(x,x,x) Î MSOL₁(S). Then, for all w Î S^* and u Î V_w,

(p,x,x) \twoheadrightarrow_A,w^* (q,x,x) iff (w,x) \models y_pq(x) .

\square

Theorem 11 For every string-walking pebble automaton A there exists a string-walking automaton with MSO tests A¢ such that R(A) = R(A¢).

Proof. When A drops its pebble at some position u of string w, it must return there some later time to pick it up, because of the definition of R_w(A). In the mean time, i.e., until A returns to u, A does not move its pebble. By using Lemma 10, the actions of this automaton until its arrival in u can be simulated by a single MSO test. The details are as follows.

Let A = (Q,D_SWPA(S),d,I,F) be a string-walking pebble automaton over S. We will define a string-walking automaton with MSO tests A¢. The MSO tests y_pq are obtained by applying Lemma 10 to the automaton derived from A by removing all transitions of the form (p,d,q) with d Î {put,lift}. We define A¢ = (Q,D,d¢,I,F) with

{ ¬, ®, true(x), head(x), tail(x), Øhead(x), Øtail(x) } È

{ lab_s(x) \mid s Î S} È{ y_pq(x) \mid p,q Î Q }

d¢

{ (p,d,q) Î d\mid d Î { ¬, ® } } È

{ (p,head(x),q) \mid (p,head,q) Î d} È

{ (p,Øhead(x),q) \mid (p,Øhead,q) Î d} È

{ (p,tail(x),q) \mid (p,tail,q) Î d} È

{ (p,Øtail(x),q) \mid (p,Øtail,q) Î d} È

{ (p,lab_s(x),q) \mid (p,lab_s,q) Î d} È

{ (p,true(x),q) \mid (p,Øhere,q) Î d} È

{ (p,y_qr(x),s) \mid (p,put,q) Î d and (r,lift,s) Î d}

The directives ¬, ®, head, Øhead, tail, Øtail and lab_s (for s Î S) are simulated straightforwardly. The MSO test y_qr(x) simulates the actions of A between the put and the lift. \square

This theorem leads us to the grand finale of this chapter.

Theorem 12 The following two statements hold:

For every MSO formula f(x,y) Î MSOL₂(S) there exists a string-walking pebble automaton A over S such that R(A) = R(f).
For every string-walking pebble automaton A over S there exists an MSO formula f(x,y) Î MSOL₂(S) such that R(f) = R(A).

There is another way to prove that any string-walking pebble automaton can be simulated by an MSO formula with two position variables. Let A be a string-walking pebble automaton over S that recognizes the relation R(A). Then a string-walking pebble automaton A¢ over SÈ(S×B₂) can easily be constructed such that (w,u,v) Î R(A) just if mark(w,u,v) Î L(A¢). A¢ walks right until it encounters a symbol (s,1,x) with x Î {0,1}. Then A¢ starts simulating A directly until it encounters a symbol (s,y,1) with y Î {0,1} in a final state. Because SWPA=REG [BH65] and REG=MSO (Proposition 1), there exists an MSO formula y Î MSOL₀(SÈ(S×B₂)) such that L(A¢) = L(y). Using Corollary 3, we obtain an MSO formula f(x,y) Î MSOL₂(S) such that, for all w Î S^*, mark(w,u,v) Î L(y) just if (w,u,v) \models f(x,y).

Note that we can also use Theorem 12 to derive that SWPAREG, as follows:

Theorem 13 SWPAREG

Proof. First we will show that any language defined by a string-walking pebble automaton is MSO definable and hence regular. Let A be a string-walking pebble automaton over S. By definition, the language recognized by A is

L(A) = { w Î S^* \mid there exists v Î V_w such that (1,v) Î R_w(A) }.

Using the second part of Theorem 12 we obtain a formula f(x,y) Î MSOL₂(S) such that, for all w Î S^* and u,v Î V_w,

(u,v) Î R_w(A) iff (w,u,v) \models f(x,y) .

We now define

y = "x ( $y (head(x) ® f(x,y) ) )

to obtain that, for all w Î S^* and v Î V_w,

$v Î V_w ((1,v) Î R_w(A)) iff $v Î V_w ((w,1,v) \models f(x,y)) iff w \models y

L(A) = L(y)

and, since MSO=REG, L(A) is a regular language.

The other way around, we show that any regular language can be described by a string-walking pebble automaton. Let L be a regular language over an alphabet S. Let M = (Q,S,d,I,F) be a finite automaton such that L = L(M). We define a string-walking pebble automaton A = (Q¢,D_SWPA(S),d¢,I,F¢) with

Q¢

Q È{q_fin}

d¢

{ (p,(lab_s,®),q) \mid (p,s,q) Î d} È

{ (p,(lab_s,tail),q_fin) \mid (p,s,q) Î d for some q Î F }

F¢

{ q_fin}

It is obvious to see that L(A) = L(M) = L. \square

Chapter 2
Extensions to
String-Walking Pebble Automata

In this chapter we will introduce two extensions to the concept of string-walking pebble automata. These extensions will be constructed in such a way that the class of languages recognized by the automata is the same as the class of languages that the (ordinary) string-walking automata recognize, i.e., the class of regular languages.

2.1 String-Walking Multi-Pebble Automata

The first extension to the string-walking automaton is the string-walking multi-pebble automaton. This automaton can use more than one pebble. The number of pebbles available to the automaton is fixed. The pebbles will be taken from a finite set and must be used ``nested''. This means that, at any point in the automaton's walk, only the pebble that was dropped last can be lifted. It can easily be seen that we can, without changing the automaton's power, number the pebbles {1,2,¼,n} and demand that the pebbles must be used in order. In order to see this, suppose the pebbles are taken from a set P with |P| = n. Consider the set M of bijections from P to {1,2,¼,n} (there are n! such mappings). We can now simulate an automaton with pebble set P by an automaton with pebble set [1,n] by coding the pebble mapping into the states: for every state q we use additional states {q_m \mid m Î M}. We also modify the transitions with put and lift so that the information on the mapping is maintained. Note that the constraint of the nested use of pebbles is necessary to make sure that the automaton does not recognize non-regular languages. A string-walking 2-pebble automaton without this limitation could recognize the language L = {aⁿcbⁿ \mid n Î \mathbb N} by putting the pebbles at both ends of the string and moving them towards the middle of the string in turn, checking that both pebbles arrive at the middle c after the same number of moves. This kind of use of the pebbles is prohibited by demanding that the pebbles be used nested. In broader terms, it can be shown that unnested multi-pebble automata are equivalent to two-way multi-head automata, which in turn are equivalent to logarithmic space Turing machines.

Let n ³ 1. We use the following set of directives for a string-walking n-pebble automaton over S:

D_SWnPA(S)

D_SWA(S)È{ put_i, lift_i, here_i, Øhere_i \mid 1 £ i £ n }

For each w Î S^* the relations for the new directives are as follows. The relations are on tuples (u,k,p) Î V_w ×[0,n]×([1,n] ® P_w). Here k represents that pebbles 1,¼,k are currently on the string and p maps the pebbles to string positions. We define p₀ : [1,n] ® P_w with p₀(i) = ^ for all i Î [1,n] as the mapping with no pebbles on the string.

The relations hold for any u Î V_w, k Î [0,n], and pebble placement function p:[1,n] ® P_w.

R_w(put_i)

{ ((u, i-1, p), (u, i, p(i ® u))) \mid 1 £ i £ n }

R_w(lift_i)

{ ((u,i,p), (u,i-1,p(i ®