-
20- 


Games on Infinite Trees and Automata with Dead-Ends 
A new Proof for the Decidability of the Monadic Second Order 
Theory of Two Successors 


An.A.Muchnik 
Institute of New Technologies 
KirovogradskaJa 11, Moscow 113587, Russia. 
e-maIl: amuchnik@globlab.msk.su. 


A central problem of mathematical logic and the theory of 
algorithms IS the problem of the decidability of logical 
theorIes, that is the problem of constructing an algorithm which 
distinguishes which formulae of a gIven language belong to the 
theory (are true In a given semantics, provable in a given 
deductive system etc.). 
The study of decIsion problems has 
number of naturally arisIng theories 
desIred algorIthm does not exist. At the 
point of view of applications, either 
mathematIcs, the most important cases are exactly those for 
WhICh such an algorithm can be constructed. 
One of the basic results concerning the decidabllity of 
logIcal theorIes is the Theorem of the decidability of the 
monadic second order theory of several successors. ThIS Theorem, 
proven by M.O.Rabin In 1969 [1], YIelds as simple corollaries 


shown that a large 
are undecidable, the 
same tIme, from the 
inside or outside 



-221- 


many of the results on decidability known to that time. SInce 
then, it has been used many times In applIcations, namely in 
provIng the decidability of non-classical logics, such as the 
logic of programs. 
However, in his lecture at the International Congress of 
Mathematics held in Nice In 1970, M.O.Rabin formulated the 
problem of simplIfYIng his proof. The first problem of his 
1 ec t ur e [ 2 ] is: 
"1. Find a sImpler proof for Theorem 2(ii), possIbly avoiding 
the transf ini te induct ion used in [2]. II (Theorem 2 (i i) is the 
key statement of Rabin's proof, [2] is paper [1] of our 
references). Indeed, Rabin's proof, beyond the technical 
complicatIons, has a more fundamental Inconvenience. In order to 
obtaIn a perfectly constructIve result, it uses a very strong 
instrument - the principle of transfinite inductIon. 
In 1978, the author of thIS paper gave a new and simpler 
proof of RabIn Theorem without using transfinite Induction. This 
proof was presented In the course on decIdable theories given in 
1978/79 at the Faculty of Mechanics and MathematIcs of Moscow 
state University by A.L.Semenov and It was the subject of the 
author's graduatIon paper. The present version dIffers only In 
small detaIls from the verSIon given there. 
Another proof, close to ours, was presented in May, 1982 at 
the SymposIum on the Theory of Computing [3]. Some time ago, 
D.Muller and P.Schupp proposed the use of alternating finIte 
automata to prove the Rabin Theorem. 



-LL2- 


g1. THE MONADIC THEORY OF TWO SUCCESSORS AND FINITE AUTOMATA ON 
TREES. 


Let us give the defInItIon of the monadic theory of two 
successors, denoted by S2S, WhICh IS formed by all formulae of a 
certain language true in a certain interpretation. The language 


contains both Individual and set 


(= 


monadic 


predicate) 


varIables; its atomic formulae are of the form x E Q, L(x,y), 
R(x,y), where x,y are individual variables and Q IS a set 
variable. Both individual and set variables can be bounded by 
quantifies in the formulae of the language. To describe the 
interpretation we consider the binary tree of finite words in 
the alphabet {L,R}: 
\/ \/ \/ \/ 
LL
/
 L\/RR 
L -----A
 R 


Words in thIS alphabet will be called also vertices of the tree. 
Values of Individual variables are vertices of the tree, values 


of set variables are arbitrary sets 


of 


vertices. 


The 


InterpretatIon of atomic formulae IS the following: x E Q states 
that vertex x is a member of Q, R(x,y) is interpreted as the 
fact that word y is obtained by adding letter R to the end of x. 
L(x,y) is understood in a similar way. Theory S2S IS thereby 
fully descrIbed. 



-223- 
Ih
Qr

_Qf_B
Q!

 Theory S2S is decidable. 


The proof proceeds in the same way as Rabin's, converting 
the problem of the decidability of S2S Into that of 
demonstrating some propertIes of finIte automata. What IS new IS 
the method of demonstrating the most complIcated of these 
properties. The object of this paper is to present thIS method. 
To make our exposItion self-contained, we shall recall all 
, necessary defInitions concernIng fInite automata. 
We shall use the varIant of the theory S2S In whIch 
formulae contain only set variables and atomic formulae are of 
the form PeQ, Vert{P), R{P,Q), L{P,Q). Their Interpretation IS 
as follows. Vert(P) indIcates that P IS a one-element set; PeQ 
indIcates that P IS one-element and its unique element belongs 
to Q: R{P,Q) and L{P,Q) mean that P and Q are one-element, 
P={x}, Q={y} and x,y satisfy R(x,y) (L(x,y), respectIvely). It 
IS ObVIOUS that this varIant of S2S IS equIvalent to the 
preceding one from the pOInt of view of decidability. 
Let L be an alphabet. A 2-tree IS a binary tree whose 
vertices are labeled by the letters of 2, I.e. a total mappIng 
from the set of all vertIces to 2. We shall define below the 
notIon of an automaton on 2-trees and the notion of acceptance 
of a 2-tree by an automaton. In thIs way, to each automaton 
corresponds a set of all L-tree accepted by the automaton. Such 
sets of 2-trees will be called recognizable. 
Let us associate with any set of vertices of a bInary tree 
a {0,1}-tree assigning 1 to the vertices of this subset and 0 
elsewhere. Likewise, with each n-tuple <PI'" .Pn> of sets of 



-Ll:4- 


vertices, we assOcIate a {0,1}n- tree . A set of n-tuples of the 
form <P t ,.. .Pn> will be called recognizable if its associated 
n 
set of {0,1} -trees IS recognIzable. 
Ih
9


_!
 Let A(P t ,... ,Pn) be a formula of theory S2S, all 
parameters of which are among PI'... ,Pn' Then the set of aIr 
{O,1}n-trees corresponding to those tuples of values of 
PI' . . . , P n wh i ch mak e A (P 1 ' . . . , P n) true is r e co gn i z ab r e. The 
corresponding automaton can be effectively constructed whenever 
A(PI""'P n ) is given. 


The proof of thIS Theorem proceeds by induction on the 
structure of formula A. The main dIffIculty here is to construct 
for a gIven automaton 
 another automaton £ which accepts 
precisely those trees WhICh are not accepted by 
. A new method 
of dOIng thIS constructIon forms the basIs part of this paper 


(g3). 


To prove the decidability of S2S, it is sufficient to have, 
in addition to thIS Theorem, an algorithm deciding whether or 
not the set of trees accepted by the automaton is empty. Such an 
algorithm IS gIven In [1]. In the present paper we give the more 
simple method for constructing of such algorIthm (g2). 
Let us now proceed to some defInitIons and remarks 
concerning finite automata. 


Automata on Q-words 


We begIn with the important notion of an automaton on 
Q-words, even though in this paper It plays only an auxiliary 



-L25- 


role. 


If 2 is an alphabet, an Q-word over 
 IS an infinite 
sequence of letters of 2. An automaton 
 on Q-words is given by: 
1) a finite set S of states; the elements of 2 5 (subsets of 
S) will be called macrostates; 
2) a table of transItions, i.e. a subset PCSXLXS; for 
when 


<s,a,s'>EP, we say that if the automaton 
 IS in state s 
reading letter a then it can move to state s' . 
, 
3) a subset SocS of Initial states; 
4) a subset Fc2 5 of fInal macrostates. 


An automaton is called deterministic If It has exactly one 
InItial state and its table of transItions IS the graph of an 
everywhere defined function from SXL to S (being in any state 
and reading any letter of 
, the automaton can move to exactly 
one state). 
Let 
 be an automaton on Q-words over 
 and let A be an 
Q-word over 
. A run of 
 on A IS an InfInite sequence of states 
WhICh may occur when 
 reads A. There may be many runs as well 
as none. But it is clear that for a deterministic automaton, 
there IS always exactly one run on the given Q-word. More 
precisely, a run is such a sequence (Q-word) sOsI... of states 
of 
 that So IS an InItial state (i.e. soeS o ) and, for each i, 
If 
 IS in state S and reads a., then it can move to state 
L L 


Si+I' We can assocIate with any Q-word ItS limit - the set of 
all symbols occurrIng In it an InfInite number of times. A run 
whose lImIt IS a fInal macrostate is called accepting. We say 
that 
 accepts an Q-word A If there is an acceptIng run of 
 on 
A. OtherwIse, we say that 
 rejects A. In such a way, to every 



-2Z6- 


automaton there corresponds a set of Q-words, namely the set of 
all Q-words accepted by this automaton. Such a set of Q-words is 


called recognizable. It 


is 


well-known 


([4]) 


that 


any 


recognizable set can be accepted by a deterministic automaton. 


Automata on trees 


We recall that a bInary tree lhe vertIces of WhICh are 
labelled by the letters of an alphabet 
 is called tree over 
 
(or 
-tree). An automaton on 
-trees is given by 
1) a fInite set S of states with a dIstInguished initIal 


state SOES; (subsets of S will be called macrostates as before); 
2) a table of transitions 1 . e . a subset of the set 
SXLXSXS. 
Element <s,a,s' ,S"> of this set will be represented by the 
following scheme: 


S' S II 
V 
s,a 


A scheme belonging to the table of transitions of 
 IS called a 
transition of 
 and we say that, If it happens that at a certaIn 


vertex, 
 IS in state S and reads a, then It may be at the 
vertIces immedIately succeeding this vertex in states s' s II . 
, , 
3) a lISt of final macr os t at es ( eac h of them beIng, of 
course, a subset of S). 
Given an automaton on a 
-tree, there are many possible 



-LL7- 


runs of the automaton on the tree. Each run is an assignment of 
states to the vertIces of the binary tree accordIng to the table 
of transitions and such that the inItial state is assigned to 
the root of the tree. More precIsely, a run of 
 on L-tree A is 
an s-tree H satisfying the following conditIon: the initIal 
state IS at the root of H, and if x is an arbitrary vertex of 
the binary tree which in A is labelled by a and in H IS labelled 
by s, and if the vertices xL, xR of run H are respectively 
labelled by s' and s", then <s,a,s's"> is an element of the 
table of transitions of 
. Now any run has many lImit 
macrostates (which is not the case for the automata on Q-words): 


there is one for each path. More precIsely, let xOx I . . . be an 
Infinite path in the bInary tree (I.e. a sequence of vertIces In 
WhICh XO=A and Xt+1 is one of the two immediate successors of 


XL). If a run H and a path are given, then the letters which 
label the vertices lying along the path form an Q-word. The 
lImit of thIS Q-word (i.e. the set of states occurring In It 
infinitely many times) is called the limit macrostate of the run 
corresponding to the given path. A run is called accepting If 
all limit macrostates (correspondIng to all paths) are final. 
We say that an automaton accepts a tree if there eXIsts an 
accepting run, i.e. a run for WhICh all the limIt macrostates 
corresponding to all paths are fInal. OtherWIse, when for each 
run there exists a path whose lImit macrostate is not final, we 
say that the automaton rejects the input tree. A set of trees is 
called recognizable if there eXIsts an automaton accepting all 
the trees of thIS set and no others. As we said above, our aIm 
is to prove (a) that the problem of emptiness of automate set of 



-2L8- 


trees is solvable and (b) that the complement of any 
recognizable set a is recognizable and that the corresponding 
automaton can be constructed effectively from the automaton 
acceptIng a. The remaining part of the present paper is devoted 
to these proofs. 


92. THE PROOF OF SOLVABILITY OF EMPTINESS OF AUTOMATE SET OF 
TREES 


In thIS paragraph we shall construct an algorithm, which 
given an automaton on trees decides whether the set of trees 
recognIzed by this aulomata IS empty, and WhICh, moreover, fInds 
the regular tree in this set, If the set isn't empty (the 
definItIon of a regular tree IS given In the following two 
lines) . 
Let us gIve the definItion of a regular L-tree. In this 
defInItion the notIon of a fInIte determinIstic transducer is 


used. A fInite transducer on words is a finIte synchronous 
automaton with output. It has two alphabets: the input one and 
the output one. After reading current letter of the input 
alphabet the transducer outputs one letter from the output 


alphabet. The output letter depends on the input letter and on 
the current state of the automaton. The transducer outputs also 
one letter before reading the Input word (we'll call this letter 
initial). Thus a finIte transducer can be defIned by lhe Input 
alphabet L, output alphabet 6, the set of states S, the Initial 
state So' the initial letter 00 and the set of transitions. 



-2L9- 


regular L-tree and if this set is recognIzed by an 
wi th n states then there IS a transducer with 
generating a L-tree in this set. 


Formally, the set of transItion IS a everywhere 
function from SXL Into Sx8. 
R
[lnl!lQn
 A L-tree is regular If there is a finite 
transducer with the Input alphabet {L
R} and output alphabet L 
that after reading any word u over {L,R} outputs the mark of the 
vertex u in this tree. (Thus the mark of the root wIll be the 
initial letter.) 
Any transducer satisfYIng this definitIon wIll be called 
the transducer generating the tree. 
IQ.
9!:
!r\_

 1) There is an algorIthm that given an automaton 
on 
-trees decides whether the set recognized by the automaton 
is empty. 2) Any nonempty recognizable set of 
-trees has a 
automaton 
n! states 


defined 


ErQQ[
 a) Firstly
 let us proof the existence of a 
transducer generatIng a L-tree in recognizable nonempty set of 

-trees. This will be proved by Induction, the parameter of 


inductIon IS the number of states of the automaton on trees that 
recognIzes the set. In order to make the Induction step we must 
prove a more general assertion. Let us state it. Let us 
introduce the notIon of a L-tree with dead ends. Let D be a 
fInite set dIsjoInt with 
. The elements of D wIll be called 
dead-ends. 
Q
iinitiQn
 A L-tree with dead-ends from D is any subtree 
of the whole bInary tree each vertex of which has eIther 0 sons 
(IS a leaf) or 2 sons, the leaves of WhICh are marked by symbols 
from D and the internal vertIces of WhiCh are marked by letters 



-230- 


from L. 


EVIdently every L-tree is also a 2-tree with dead-ends from 
D (for any D). 
Let us gIve the definItion of a L-automaton with dead-ends 
from D. The only difference wIth a 
-automaton IS that a 
L-automaton wIth dead-ends from D can have transItions of the 


form 


Pv q 
s,a 


where p or q or both are dead-ends from D. That is the set of 
transItIons IS a subset of the set Sx
x(SUD)x(SuD). The sets S 
and D must be dIsJoInt. A possible run of a 
-automaton with 
dead-ends from D on a 
-tree T with dead-ends from D is any tree 
H that can be obtained from T by assignment to each internal 
vertex of D a state in such a way that the root is marked by 
initial state and the obtained markIng is consIstent with the 
set of transItions. That IS
 for every internal vertex x of H if 
a IS a mark of x from 
, S IS the assIgned mark from Sand p and 
q are respectively the marks from SuD of the vertices xL and xR 
then the tuple <s
a,p,q> belongs to the set of transItions. An 
ordinary automaton on 
-trees is a partIcular case of a 

-automaton wIth dead-ends from D (for any D). A possible run is 
called accepting if the limit macrostates of all its infinite 
paths are final. 
Now let us extend the notIon of a regular tree to the tree? 
with dead-ends. A transducer wIth Input alphabet {L,R} and 
output alphabet LUD generates a L-tree T with dead-ends from D 



-231- 


If after reading any word v over {L,R} it outputs the mark of 
the vertex v in T. 


We wIll prove by inductIon the following assertIon. 

-automaton 
 with dead-ends from D accepts some L-tree 
dead-ends from D then 
 accepts some L-tree with dead-ends 
D generated by a transducer with at most n! states. 


If a 
wi th 
from 
The 


parameter of inductIon IS the number of states of 
 (other 
parameters can be arbitrary). Let us call for brevIty the 
automata accepting nonempty sets the nonemptv automata. 
Base of induction. Let 
 be a nonempty 
-automaton with 
dead-ends from D having only one state. As 
 accepts some 
-tree 
with dead-ends the set of transitions isn't empty. Let us denote 
the single state by s. Consider two cases. 
1). There is a transItIon of the form 


t 1V : 2 
, 


where t 1 ,t 2 are dead-ends. 
Then 
 accepts the tree with dead-ends 


t 1v t 2 


generated by a transducer with one state. 
2). There is no transition wIth two dead-ends on the top. In 
thIs case every acceptIng run has infinIte path therefore the 
macrostate {s} is final. There is a transItIon of one of the 


followIng forms 



S t 
V 


s,a 


-232- 


t s 
V 


s,a 


s s 
V 
s,a 


where t is a dead-end. Correspondingly 
 accept one of the 
following trees 


a t 
Yt 
V 
a 


t a 
V 
t a 
V 
a 


a 


a a a 
\/ 
a 
/ 
a 


All these trees are generated by a transducer with 1 state. 
Induction step. Let a nonempty L-automaton 
 wIth dead-ends 
from D have n
2 states. We will regard the states as the 
residues modulo n. Thus for every state k we can speak about the 
state k+l. Without loss of generalIty we can assume that 
 has 
single initial state (as the recognized by 
 set is the union of 
the sets recognIzed by the automata obtained from 
 by leaving 
only one InItIal state). Let the InItIal state be O. Let us 
defIne 2n new automata 
o'" .'
n-I'
O".' '
n-1' havIng n-1 
states. 

k is obtained from 
 by the following transformation. The 
set of states of 
k is {O,... ,n-l}\{k} and the set of dead-ends 
IS D. All transitions in which the state k occurs are deleted 
and all macrostates havIng k are deleted. 

k is obtaIned from 
 by the following transformation. The 
inItIal state of 
k IS k. The set of states IS {O,... ,n-l}\{k+l} 
and the set of dead-ends is Du{k+1}. All the transItions having 
(k+l) on the bottom are deleted and all the macrostates having 



-233- 


(k+l) are deleted. 
Let us consider two cases 

Q

_l
 For some k the automaton 
k is nonempty. Let us 
define a regular 
-tree with dead-ends from D accepted by 
. Let 

' be the automaton obtained from 
 by deleting k from the set 
of states, adding k to the set of dead-ends, deletIng all 
transitions having k on the bottom and deleting all macrostates 
having k. Let us prove that 
' is nonempty. PIck some L-tree T 
with dead-ends from D accepted by 
. Let us fix an acceptIng run 
H of 
 on T. Let T' consist of all vertIces u of T such that no 
ancestor of u IS marked by k in H (u Itself can be marked by k). 
Evidently T' IS a L-tree wIth dead-ends from Du{k}. Evidently it 
is accepted by 
' . 
By Induction hypothesIs there is a 
-tree T I with dead-ends 
from Du{k} generated by a transducer with (n-1)! states and 


accepted by 
' . Again by Induction hypothesis there is a 
-tree 
T 2 with dead-ends from D accepted by 
k and generated by a 
transducer with (n-1)! states. Let us "glue" to all leaves of T 1 


marked by k the L-tree T 2 and erase the mark k In that leaves 
(now all leaves that were marked by k are marked by the root 
mark of T 2 ). We have obtained a 
-tree T3 with dead-ends from D. 
FIrstly, T3 is accepted by 
: the acceptIng run of 
 is 
obtained by the same gluing of an accepting run of 
' on T I and 
an acceptIng run of 
k on T 2 . Indeed, every Infinite path in the 
obtained run eIther belongs to the run of 
' (and hence has 
fInal limit macrostate) or from some place is In the run of 
k 
(and hence also has final limit macrostate). 
Secondly T3 is generated by the transducer obtained by 



-234- 


gluing the transducers generatIng T 1 and T 2 : in those states in 
which the first transducer outputs the dead-end k the new 
transducer outputs the initial letter of the second transducer 
and switch It on. The number of states of the new transducer is 


(n-l)!+(n-l)! 
n! (as n
2). 
Case 2. For all k the automaton 
k IS empty. Let us prove 
------- 
that in this case the whole macrostate {0,1,...,n-1} is final 


is a vertex va in H marked by 1 . As 
1 
vertex v t in H that is marked by 2 and 
IS v 1 =v O u for some word u over {L,R}). 


and for all k the automaton 
k is nonempty. By condition 
 
accepts some L-tree T with dead-ends from D. Let us fix some 
acceptIng run H of 
 on T. Let us prove that H has an infinite 
path with fInal macrostate {O,1,... ,n-1}. As 
o is empty there 
IS empty there is a 
follows vertex V o (that 
And so on. We have found 
an infinite path In H which passes through all states 
0,1,... ,n-l Infinitely many times. As H IS an acceptIng run, the 
macrostate {0,1,... ,n-l} is fInal. 
- 
Let us prove that for all k the automaton 
k IS nonempty. 
Let us take arbitrary k. Let us fix agaIn a run H of 
 on a 

-tree T wIth dead-ends from D. We have already proved that some 


vertex v of H is marked by k. Consider the 
-tree 
Ht={ulvu e H} , in which the vertex u is marked as the vertex vu 
in H. Consider the subtree H 2 of Ht consisting of all vertices u 


such that no their ancestor is marked by (k+l)(u itself can be 
marked by k+l; in this case we delete the L-mark of u). 
Evidently we have obtained an accepting run of 
k on some 
-tree 
with dead-ends from DU{k+l}. 
Now let us construct a regular 
-tree wIth dead-ends from D 



-235- 


accepted by 
. By InductIon hypothesis for each k there is a 

-tree Tk with dead-ends from Du{k+1} accepted by 
k and 
generated by a transducer with (n-1)! states. The L-tree T with 
dead-ends from D IS constructed as follows. Let us take To. Let 
us "glue" to all leaves of To marked by 1 the tree T 1 (and 
delete the mark 1 of those leaves). Let us "glue" the tree T 2 to 
all leaves marked by 2 of the obtained tree. And so on. Let us 
denote the tree obtained by repeating thIs procedure 
 times by 
T. Obviously T is a 
-tree with dead-ends from D. We claim that 

 accepts T and T IS regular. 
Let us prove that 
 accepts T. To this end let us fIX for 
every k an accepting run Hk of 
k on Tk. Let us perform with 
Ho" ..,Hn_1 the same IgluIng" as with To". .,Tn_t. We'll obtain 
a run H of 
 on T. Every infInite path in H either from some 
place belongs to some run of [k for some k (therefore has fInal 
limit macrostate) or passes Infinitely many tImes through all 
states (therefore its limit macrostate is {0,1,... ,n-l}, which 
is final). 
The tree T is regular because it can be generated by 
"gluing" the transducers generating To'" .,Tn_t. The number of 
its s tat e is e q ua 1 ton. (n - 1 ) ! = n! . 
b). Let us now prove that given a L-automaton 
 with 
dead-ends from D we can decide whether it IS empty and construct 
the transducer generating the accepted tree with dead-ends. Our 
algorithm IS recursive (in recursive calls the number of states 
decreases). Let us be gIven
. ConsIder two cases. 
Case 1. 
 has single state s. If the set of transItions is 
empty then 
 accepts empty set. Otherwise we look if there is a 



-236- 


transition wIth two dead-ends on the top. If there is such a 
transition then 
 is nonempty. Otherwise 
 is empty if and only 
if the macrostate {s} is final. Obviously we can construct the 
transducer with single state generating an accepted tree if it 
exists. 


Case 2. 
 has n
2 states. Making the recursive calls we 
check whether there is k such that 
k is nonempty. If there is 
such k then 
 IS empty if and only if 
' is empty (
' is defined 
in the item a». Making the recursive call we can decide whether 

' is empty. 
Otherwise (if for all k, 
k is empty) 
 is nonempty if and 
only If the macrostate {0,1,.. .,n-1} is final and for all k, 
k 
is nonempty (this IS in fact proved in the proof of case 2 of 
item a». Making recursive calls we can decide whether this is 
true. The transducer is constructed as it was described. 
The proof is finished. 


It turns out that the bound n! in theorem 2 cannot be 
improved. 
Ih
2£

_

 There is a constant c such that for aLL n there 
is a nonemptv set of {O, l}-trees accepted by an automaton with 
cn states and having no {O,l}-tree generated by a transducer 
with less than n! states. 
Proof. Let us introduce the notion of an n-ary 
-tree 
(n E 
). Recall that binary 
-tree is a mapping from the set of 
all words over {L,R} into 
. Likewise a n-ary 
-tree is a 
mapping from the set of all words over the alphabet {I,... ,n} 
into 
. If x O ,X 1 ,X 2 ,... is a path in n-ary 
-tree and xi=xi_ta i , 
a i E {I,... ,n} then a i wIll be called the direction of the path 



-237- 


on i-th leue
. The notIons of an automaton on 2-trees and of a 
transducer can be naturally generalized to n-ary 2-trees. 
Firstly we wIll construct for every natural n a nonempty 
set of n-ary {1,2,.. .,n}-trees accepted by an automaton with en 
states and havIng no tree generated by a transducer wIth less 
than n! states. Then this set of trees will be transformed into 
the set of binary {0,1}-trees wIth the same properties. This 
will complete the proof. 
Let us fix n e 
 and define the set M 
where L={1,2,.. .,n}. Let T be a n-ary 
-tree. 
case T belongs to M. Let us take an arbitrary 
at ,a 2 ,... ,a k ,... be its directIons and PO'P I ,p 2 '... ,Pk'... be 
its marks (that is Pk IS the mark of the vertex a l .. .a k in T). 
We'll call Pk the mark of the path on k-th level. Let N be the 
set of all a E {1,.. .,n} that occur Infinitely many tImes in the 
sequence a t ,a 3 ,a S '" .,a 2k + 1 ,... Briefly speakIng, N is the lImit 
set of the directIons on odd levels. Let P be the limit set of 
the marks on even levels. Let us call the path correct if the 
maximal element of P is equal to the number of elements of N 
(that is maxP=INI). By definition T belongs to M if all paths in 
T are correct. 
Let us prove that M Isn't empty. To this end we defIne a 
transducer with 2n! states generating a tree in M. Reading the 
sequence a 1 ,a 2 ,.. .,a k ,... of dIrections the transducer computes 
the so called "sequence of last occurrences of the dIrectIons on 
odd levels". Let us define this sequence. This IS a permutation 
of the set {1,2,.. .,n}. In the beginning it is equal to 
(1,2,.. .,n) and after reading the current direction a 2k + 1 on an 


of n-ary 
-trees 
Define in what 
path in T. Let 



-238- 


odd level the current permutation n 2k is transformed as follows; 


a 2k + 1 is moved in the beginning of TI 2k (the previous occurrence 
of a 2k + t is deleted). Let us defIne the output of the 
transducer. On the odd steps (i .e. after reading a t ...a 2k + t ) it 
outputs 1 . Let us define the output symbol on an even step, say 


after reading at.. .a 2k + t . Let 12k+t be the length of the prefix 
of TI 2k that was changed on the step 2k+l (i.e. 12k+t is equal to 
the number of the occurrence of a 2k + t In n 2k ). The transducer 
outputs this 12k+t on the step 2k+2. The initial letter of the 
transducer is 1. 


Let us prove that the tree generated by the defined 
transducer belongs to M. Let us fix an arbitrary path in this 
tree. Let N be the lImit set of the dIrectIons on odd levels of 
this path. Then for all sufficiently large k the prefix of ilk of 
the length INI IS a permutation of elements of N therefore the 

 
number output by the transducer on the k-th level will be less 
than or equal to INI. On the other hand, as every direction from 
N occurs infInitely many tImes on odd levels, the INI-th element 
of the sequence Infinitely many times IS moved in the beginning 
therefore the transducer will infInitely many times output INI. 
Let us prove that M is accepted by an automaton with 2n 
states. The states of this automaton are of two types: the first 
type consists of one state for every direction and the second 
type consists of one state for every lelter from 2 (alltogelher 
2n states). On the even levels (I.e. after reading at.. .a 2k ) the 


state of automaton IS equal to the mark of the current vertex 
(i .e. the mark of at.. .a 2k ). On the odd levels (i.e. after 
reading at.. .a 2k + t ) the state of automaton IS equal to the last 



-239- 


direction (I.e. a 2k + 1 ). The inItIal state is arbItrary state of 
the second type. The final macrostates are those states in which 
the maximum of the states of the second type IS equal to th
 
number of states of the first type. 
Let us prove that there is no transducer wIth less than n! 
states generatIng a 
-tree In M. Assume that 
 is a transducer 
with less than n! states generating a tree in M. 
Let p=(v 1 ,.. .,v n ) be a permutation of the set {1,... ,n} of 
directions. ConsIder the word 


n' n' n' 
up = ( . . . ( (v 1 . V 2 ) .... V n) . 
k 
where w denotes w w .. .w, k times. We'll call the word 


n' n' n' 
w.=((...((v 1 V 2 ) ....v. 1 ) V. 
t t - L 


the block of level i. Thus the block of level i consists of n! 
blocks of level (i-I) and of the letter vi and up consists of n' 
blocks of level n. DefIne for any word u the word u to be the 
word obtained by Inserting 1 before each letter of u (for 


example 010 =101110). Let 
 work on the Input word up. 
the states of 
 before reading the occurrences of wi in 
the number of occurrences is greater than the number of 


Consider 


up' As 
states 


there are two occurrences of W in U P and a state s such that 
 
n n 
is in the state sn before reading these two occurrences. Let us 
call these two occurrences of w n in up marked. Let now 
 start 
in the state sn and work on the input word w n ' Again there are 
two occurrences of w n _ I in w n and a state sn_I such that 
 is in 
the state sn_l before readIng these two occurrences. Let us call 
these two occurrences of W n _ 1 In W n marked. Let us call the 
marked occurrences of w n _ 1 in the marked occurrences of w n in up 
also marked. Thus we have four marked occurrences of w n _ t in up' 



-240- 


Repeating this procedure n times we get a state sl and 2 n marked 
occurrences of w t in up such that if 
 reads up then before 
reading each marked occurrence of w t in up it is in the state 
St. As St depends on p we'll write Step). As the number of 
permutations of the set {I,.. .,n} is greater than the number of 
states there are two dIfferent permutations p and p' such that 
St(p)=St(p'). Let p=(vt,...,v n ), p'=(vt',...,v n '). Let i
n is 
defined by the equalities vt=v t ',... ,vi_t=v t _ t ', vi;r.v i '. 
Let us prove that the word up has a subword y over 
{v t ,.. .v i } having occurrences of all the letters V t ,... ,vi and 
such that if 
 works on input word up then 
 IS in the state 
Step) before and after reading y. Indeed, let us pick a marked 


occurrence of w i + t in up . It has two marked occurrences 
(we'll call them left and right). Let us pick in each of 
two occurrences a marked occurrence of w t . Take the part 
from the occurrence of W t In the left occurrence of w t 


of 


W. 
t 


these 


(Including Wt) up 
- 
occurrence of w. In 
t 


to 


the 


occurrence 


of 


In 


of up 
in up 
rIght 


W t 


the 


for some word y over 
required conditions. 


up (excluding W t)' This part is equal to y 
{V t '... ,vi}' The word y satisfies th
 
Let us denote the word obtaIned from up' by 


the same procedure by y' . 
Now let us pick a word x such that after readIng x, 
 is in 
the state St (p). Consider three Q-words over 
 


- - - - 
x y y y y. . . 


X y' y ' y' y '... 
X y y ' yy ' y y '... 
Any of these three Q-words defines an infinite path in n-ary 
tree. 



-241- 


Evidently the limit sets of the directions on odd levels of 
these paths are respectIvely equal to 
{V t ,... ,V i _ t ,vi} 
{V t ,...,V. 1 ,V.'} 
t - t 


{V 1 '...,V. l 'V.'V '}. 
L - t L 


On the other hand let P and P' are the sets of letters 


output by 
 on even levels when It starts in the state Step) and 
reads respectively y and y'. Then the limit sets of the letters 
output by 
 on even levels on these Q-words are respectively 
equal to 
P 


P' 


puP' 


Thus we have maxP=i, maxP'=i, max(PUP')=i+1. ContradictIon. 


We have constructed the nonempty 


set 


M 


of 


n-ary 


{1,. ..,n}-trees accepted by a deterministic automaton wIth cn 
states and having no tree generated by a transducer with <n! 
states. Let us construct the set of binary {O,l}-trees with 
these properties. Clearly without loss of generality we may 
assume that n=2 k for some k. For every n-ary {1,... ,n}-tree T 
let us define its "counterpart" T, which is a binary {O,l}-tree. 
Let us do this in two steps. On the fIrst step let us defIne a 
binary {1,.. .,n}-tree T as follows. Each "fork ll in T the form 


T 1 


T 
n 


a 


C T 1 ,T 2 ,... ,Tn are trees) is replaced by the IIfork" 



-242- 
II I 2 I 
n 
1 1 1 ] k levels 


a 


The obtained binary tree is T. Then we replace in T every 
"fork" of the form 


T V T 2 


(T l' T 2 are trees) WI th the II fork" 


TIT 2 

k 


To 
'" 
Et 
where Et.. .E k is the binary code of the letter a (under some 
fixed coding of the elements of {I,.. .,n} with binary words of 
length k) and To is the bInary tree marked with only zeros. The 
obtained tree is T. 
Define M={TIT EM}. One can easily prove that R is accepted 
of the 
of the 


by a deterministic automaton wIth en states. The proof 
lower bound n! can be eas i 1 Y transformed to the proof 
same bound for M. 
The theorem is proved. 



-243- 


93. PROOF OF THE RECOGNIZABILITY OF COMPLEMENTATION 


strategies 


Let 
 be an automaton on 
-trees. Our aIm is to construct 
an automaton £ accepting precisely those trees which are 
rejected by 
. This will be done in two steps. First, we 
introduce the notion of "rejecting strategy" for 
automaton on a given tree. Such a strategy will eXIst 
9nly if the automaton rejects the tree. In the second 
shall construct an automaton £ having an accepting run 
only if there exists a rejecting strategy for
. This 
the required automaton. 
A rejecting strategy IS a strategy for finding a path with 
a non-final limit on any run of the given automaton. We look for 
such a path step by step, starting at the root of the tree and 
proceeding in the following way. Let a run X be given. In the 
first step, we consider the transition at the root and we choose 
one of the two possIble directIons - left or right. Suppose that 
the left IS chosen. In the next step, we consider the transition 
we have in the left vertex of the first level of run X (vertex 
L) and, once again, we choose a direction. Thus, at each step, a 
dIrection is chosen (by respecting the transItion observed in 
this step) and a move to the next vertex in the chosen direction 
is effected. In this way, applying a strategy to run X, we get 
an infinIte path in the run. A rejecting strategy applIed to any 
run must give a path with a non-fInal limit. 
Let us describe the notion of a strategy more formally. 


a given 
if and 
step we 
if and 
wIll be 



-244- 


Suppose that automaton 
 and input tree Tare 
all transitions possible at the root of T, i.e. 
of the form 


given. Consider 
all transitions 


s' Sll 
V 
S,x 


where s is the initIal state of 'U and x is the letter labe liing 
the root of T. Let us divide them in some way into IIleft 
transitIons II and "right trans it ions II . If a run X starts with a 


left (right) transition, then the strategy will seek in this run 
a path with a non-final limit going in the first step to the 
left (right, respectively). Having made this division, we have 
defined the states possibly occurring at L during the search. 
Let us call them states possible at L, or in short L-possible 
states. In other words, they are the states which are top left 
in the transitIons that have been chosen as left ones. We 
sImilarly define R-possible states or states possible at R. 
(Note that the sets of L-possible and R-possible states can by 
empty). Furthermore, we divIde the transitions of 
 having at 
the bottom an L-possible state and the letter labelling L in the 
input tree (the L-possible transitions), into the left and rIght 
ones. This dIvIsion determines how the strategy WIll seek a path 
wIth a non-final limit in the second step. Afterwards, we define 
which states are possible at the vertices LL and LR. Similarly, 
havIng divided the R-possible transItions into left and right 
ones, we define the states possible at the vertices RL and RR, 
and so on. 



-24b- 
To give a strategy for automaton 
 on input tree T means to 


decide for each vertex which of the transitions possIble at this 
vertex should be considered as left ones and which as right 
ones. Note that the set of states possIble at a given vertex 
( and, hence, the set of transitIons possible at this vertex) 


depends on the decisIon made in the precedIng step. 
So
 let a strategy for the given automaton 
 and input tree 
T be given. The strategy seeks, as descrIbed, a path in each run 
of 
. The strategy is called rejecting if all the paths it 
defines, for all runs of 
, have non-final (for
) limits, and 
moreover, each probable path of the given strategy has a 
non-final limit. By a probable path of the given strategy (the 
automaton and the input trees are fixed) we mean a path which 
can be obtained as follows. FIrst of all, choose one of the 
transitions possible at the root. Then look at what the strategy 
proposes - to consider thIS transition as left or as rIght. Let 


it be left. Take the state which is top left in thIS transition. 
It is one of the L-possible states. Then, choose an L-possible 
transition starting in this state. AgaIn consult the strategy. 


Suppose this transition is rIght. Take the state which is top 
right in this transition. This state is LR-possible. And so on. 
If this process does not terminate because of the absence of 
possible transitIons starting in the given state, we obtain a 
path In the tree and the states lYIng along It. These paths, 
obtained in this way, are called probable paths of the given 
strategy. Every path obtaIned by applying the strategy to a run 
of automaton 
 on tree T is probable. The inverse Implication 
IS, however, not generally true because a probable path requIres 



-246- 


a selection of transitions only II lying along" the path and we do 
not know whether this selection can be extended to a run on the 
whole tree. 
So far, we have Introduced the notion of a strategy (for a 
given automaton on a given input tree) and we have distinguished 
the rejectIng ones. The existence of a rejectIng strategy for 
 
on T is sufficIent for 
 to reject T. To make this condition 
necessary, we have to change the notion of strategy by accepting 
the existence of a "memory of finite size" in it. The above 
given notion of strategy a preliminary one becomes a 
particular case of the more general notion of strategy that we 
shall present in the next section. 


Modification of the notion of strategy 
- strategy with memory. 


A strategy with memory differs from the previous one when 
it is decidIng how to continue to seek a path with a non-final 
limit in a given run. The new strategy considers not only the 
transItion at the vertex it IS working on but also the history 
of the search reflected in the "inner state". Actually, applying 
the strategy to two different runs, it is possible to reach th
 
same vertex in both cases, with the same transitions at this 
vertex. The existence of a "memory" allows it to go, in one case 
to the left
 and in the second, to the right. 


The new notion of strategy will be defined as follows. 
Suppose that each state s of 
 divides into one or more 
dIfferent copies St,s2'.' (more formally, we are given a set C 



-247- 


of all copies of all states and a surjective mapping 
 of C onto 


S). 


Let for every paIr <s,s'> and every copy e of the state s a 
copy c' of the state s' be given. c' is called the result of the 
application of transition s 
 s' to the copy e. (More 
precisely, we are given a function q>: SxC 
 C s.t. 

(
(s' ,e»=s' for every S'ES and every CEC. We speak about a 
mapping from SxC rather than about a mapping from SxSxC because 
of s=
(e).) Finally, let one of the copies of the initial state 
be fixed and called the initial copy. In thIS situation we say 
that a strategy set for automaton 
 is given. We are going to 
define the notIon of a rejecting strategy for 
 on tree T based 
on the strategy set M. If M contains exactly one copy of each 
state, then the new defInition coincides with the old one. 
Previously, the chosen strategy was fIxing in each vertex a 
set of possible states, now, instead of this, we shall have a 
set of possible copies. (Note that it may happen that one copy 
of a state will be possible and another copy of the same state 
will not). 


Let 


s' S II 
V 
s,a 


be a transition of 
 and let e be a copy of 


the 


state s. Consider the scheme 


e' c" 
y. 
, 


where 


c' ell 
, 


are 


obtained as resul ts of the appl icat ion of trans it Ions s 
 s' 


and s t---+ S" to e. (Note that e' and e" are copies of s' and sIt 
, 
respectively.) All transitions of this form (obtained by 
applying all transitions of 
 to all copies e) wIll be ca 11 ed 


copy-transitions. The copy-transitions, with a copy possible in 



-248- 


some vertex at the bottom are called 
at thIs vertex. The strategy divides 
at a vertex Into the left and 
copy-transItions obtained from the 


copy-transitions possible 
copy-transitions possible 
the right ones. (Two 
same "ordinary" transition 


need not to be of the same direction). This division defInes the 
sets of copies possible in the successor vertices: for example, 
the set of copies possible in the vertex xL is the set of all 


copies which occur at the left top of copy-transitions that are 
possible In x and related by the strategy to the left ones. The 
initIal vertex has exactly one possible copy - the initial copy 
(of the initial state). The probable paths of the strategy are 
defined as before with the following modification: each path is 
related to a sequence of copies (and not to a sequence of 
states, as prevIously). However, when defining the notion of a 
rejectIng strategy, we shall be interested only in states 
(remainIng Indifferent to which copy of the gIven state occurs). 
That is, a strategy is called rejecting if for each probable 
path the corresponding sequence of states has a non-final limit. 
Now, let a rejectIng strategy for 
 on tree T based on the 
strategy-set M be gIven, and moreover, let a run on T be given. 
How can we fInd in this run, using the rejecting strategy, a 
path wIth a non-fInal lImit? This demands selecting a copy in 
each transition, starting at the bottom and moving upwords. We 
start at the initial copy of the initial state. Then we look at 
the copy-transItIon which lies in the root. Suppose It to have 
been desIgnated as the left. Hence, we have to move to the left 
into the vertex L. The copy-transition which lies there IS a 
possible copy-transition and It was, again, designated as left 



-249- 


or right. Depending on that, we have to move either to the 
vertex LL or to the vertex LR. And so on. The path we thus get 
will be one of the probable paths and, therefore, its limit will 
be non-final. We have now proved the ImplIcation (2) t---4 (1) of 
the following statement. 
Ih
2£

_

 For every automaton 
 there extsts such a ftnite 
strategy-set M that for any tree T the conditions 
(1) tI
 rejects T" 


and 


(2) "there exists a rejecting strategy for 
 on T based on 


M" 


ar e e qui v a 
 en t . 
Our first aim is to give the proof of this theorem by 
showing that for a suitable strategy-set M, (1) implIes (2). 
Then, the only remaining thing to establIsh will be that the 
existence of a rejecting strategy for 
 on T based on M is 
equivalent to the acceptance of the tree T by another automaton. 


Beginning of the Proof of Theorem 4: 
Introduction of Dead-ends in Automata and strategies 


To prove Theorem 4, we shall have to generalize it by 
introducing dead-ends to automata on trees. Let 8 be a fInite 
set of dead-ends. Instead of L-trees, we shall consider 
LxP(8)-trees and not the L-trees with dead-ends from 8 as in g2, 
i.e. trees the vertices of WhICh are labelled by both a letter 
from L and a set of dead-ends. The dead-ends of this set will be 
called dead-ends ar
owed in the given vertex. The definition of 



-250- 


automata with dead-ends was given in 92. 
Let us now give the definition of a run of an automaton 
with dead-ends on a 
xP(A)-tree. The run of automaton 
 on a 

xP(A)-tree is a subtree of the complete binary tree, in which 
each vertex has either 0 or 2 successors. The vertices with 0 
successors are labelled by dead-ends, those wIth 2 successors by 
states. Moreover, each transition occurring here has to be a 
transition of the automaton 
. End of the definition of a run. 
A run is called accepting if, first, all its dead-ends are 
allowed (that is, belong to the P(
)-label of the corresponding 
vertex) and second, the limits of all infinite paths are fInal 
macro-states. We say that a 
xP(8)-tree is accepted by 
 (the 
automaton with dead-ends) if there is an accepting run; 
otherwise, we say that the tree is rejected by 
. Let us now 
explain what is a rejecting strategy for a given automaton on a 
given 
xP(
)-tree based on a given strategy-set M. It seeks, 
starting in the root, either an infinite path wIth a non-final 
limit or a finite path ending in a non-allowed dead-end. When 
considering the possible copy-transitions, it relates them 
eIther to the left ones or to the right ones. What is new is the 
fact that in some of these transitions there may be one or two 
dead-ends at the top. (Dead-ends do not have any copies). 
Suppose for example that in a possible copy-transition, there 
is, top left, a dead-end and top right a state (or, more 
exactly, a copy of a state). If this transition is related to 
the right ones, then we get a possible copy at the right 
successor vertex; If it is related to the left ones, we get a 
dead-end in the left successor vertex. In this way we get, in 



-251- 


each vertex, in addition to the set of possible copies, a set of 


possible dead-ends. For example if a vertex is the left 
successor (of the preceding vertex) then this set is the set of 
all dead ends lying at the left hand side of the top of the copy 
transitions possIble at the precedIng vertex and related to the 


left ones. Probable paths will be of two kinds now: 
ones, defined as before, and finIte ones ending In a 
dead-end. We are ready now to formulate the 
generalization of Theorem 4. 


infInite 
possible 
promised 


!h
2[
m_1:. Let automaton 
 in aLphabet 2 and a set 8 of 
dead-ends be given. Then there exists such a finite strategy set 
M that for any 2xP(8)-tree T, the following statements are 
equtvalent: 
(1) "
 rejects T" 
(2) "there exists a rejecting strategy for 
 on T based on 
the strategy set M". 
The impllcat Ion (2) .
 
The implication (1) 
 
on the number of states 
dead-ends) . 


(1) can be proved as before. 
(2) is going to be proved by 
of 
 (with an arbItrary 


inductIon 


number 


of 


The case of the automaton with one inner state. 


We want to prove Theorem 4' for the automaton with one 
inner state (denoted in the following by 0) and an arbitrary 
number of dead-ends. As a strategy set, for thIS automaton, we 



-252- 


can use the set containing the unique copy of the unique state. 
We have to prove that one of the two following possibilities is 


always true: eIther there is an accepting run or there is a 
rejecting strategy. Let us consider two cases. FIrst case: 
macrostate {O} IS not final. In this case, the limit of any 


infInite path is not final and any accepting run must be finite. 
Moreover, the definitIon of a rejecting strategy requires the 
limits of all probable paths to be non-final and this condition 
IS here automatically fulfilled. In this case, we shall 
construct a rejecting strategy assuming that there is no 
accepting run. In the second case, when macrostate {a} is final, 
the limit of each path is final; and when constructing an 
acceptIng run, we have only to verify the condItion concerning 
dead-ends. In this latest case, we shall construct an accepting 
run assumIng that there is no rejecting strategy. 
El[
t_QQ


 {a} is not final. 
Let no accepting run exist. This means that no transition used 
at the root can be the beginning of such a run. More precisely, 
the following Lemma is true. 







_!
 Let tree T with the root Labelled by aE2 be 
rejected by automaton 
. 
o 0 
(a) If 
 is a transition of automaton 
O,a 
then the subtree with root in L or the subtree with root in R is 
rejected by 
 
o 5 
(b) If 
 is a transitIon of automaton 
O,a 



-
53- 


then the dead-end 5 is not allowed (in vertex R) or the subtree 


with root in L is rejected by 
. 
5 0 
(c) If Vts a transition of 'U then the dead-end 0 
O,a 
is no t allowed (in vertex L) or the subtree with root in R is 


rejected by 
. 
6 6' 
(d) If V is a transition of the automaton then at least 
o a 
, 


one of the two dead-ends is not allowed (in the corresponding 
vertex). 


Proof. ThIS Lemma IS almost obvious: if its statement were 


not true, then It would be possIble to construct an accepting 
run of 'U, by "gluing lJ the described parts ( in (a) , e.g. , 
"gluing" accepting runs on L-subtrees and R-subtrees). 


We are now ready to describe a rejecting strategy of 'U on T 
(recall: 
 rejects T, {O} is a non-termInal macrostate). On the 
first step, we have to divide all transitIons having at the 
bottom the same letter as the tree T has at its root, into left 
and right ones. This will be done as follows: the transition is 
considered as a left one if it has top left either a non-allowed 
dead-end or the macrostate {a} and, in this latest case, the 
L-subtree is rejected by 'U. If neither of those conditions is 
satisfied, then the transition is consIdered as a right one. 
Following Lemma 1, it then has top right either a non-allowed 
dead-end or the state {a} and, in the latter case, the R-subtree 
is rejected by 
. The previous considerations YIeld that all 
dead-ends possIble at Land R are not allowed; and, moreover, it 



-254- 


is clear that if the state 0 is possible at one of the vertices 
Land R, then the subtree with the root at this vertex will be 
rejected by 
. This gives us the opportunity to divide s imi lar ly 


all transitIons possible at Land R into left and right ones. 
ContInuIng thus, we finally get a rejecting strategy: the 
conditIon for dead-ends is satisfied and, as mentioned before, 
there IS no need to verify the condition for infinite paths. The 
first case IS complete. 


QQDQ_Qg


 {a} is final. 
We shall now proceed in the opposite directIon: SupposIng that 


there is no rejecting strategy, we shall construct an accepting 
run. So, let no rejecting strategy for 'U on the tree T exist. 
This means that in the first step, it was not possIble to assign 


certaIn transitions either to the right or to the left in such a 
way that we could continue with the construction of the 
strategy. To put it more precisely, we arrive at the following. 


k



_

 Let us suppose that there is no rejecting strategy 
for automaton 'U on the tree T, the root of which is labeled by 
letter a. Then there exists a transition of 
 for which one of 
the following statements holds: 


o 0 
form 
 and there is no 
O,a 
L-subtree and on the R-subtree; 
5 0 
form V, there is no 
O,a 
rejecting strategy on the R-subtree and 5 is an allowed (in L) 
dead-end; 


(a) the transition is of the 
rejecting strategy for 
 on the 
(b) the transition is of the 



-255- 


0 5 
(C) the transition is of the form V' 
rejecting strategy for 
 on the L-subtree and 0 is 
(in R) dead-end; 


there is no 


an allowed 


o 0 
(d) the transition is of the form 
, where 5 and 5' are 
O,a 
aLLowed in Land R dead-ends respectively. 


Proof. The Lemma is almost obvious: if such transitions did 
not exist then we would be able to designate each transition (at 
the root) as a left one or as a right one and, going on in the 
same way, to obtain a rejectIng strategy. (For example, either 
the L-subtree or the R-subtree would have a rejecting strategy 
o 0 
for any transition of the form V depending on the 
a,a ; 
subtree, we would simply follow the (existIng) rejecting 
strategy on this subtree). 
We shall now construct an accepting run (of automaton 
 
with final macrostate {O} which does not have any rejecting 
strategy on the tree T). Take the transition guaranteed by 
Lemma 2 and put it in the root of the run. Suppose for example 
5 0 
that it is of the form 
 
O,a 
Then 5 is an allowed dead-end and the R-subtree does not have 


any rejectIng strategy. If we apply Lemma 2 to the R-subtree we 
obtain the next transition, and so on. The resulting run wIll be 
accepting: the condition for dead-ends is satisfied and the 
condition for paths is obvious because of {O} being final. 



-256- 


The case of one-state automaton is proved. 


Induction step 
(description of the strategy set and two lemmas) 


So, we are now to prove Theorem 4' for automaton 
 with n+1 
states
 assumIng it to be true for any automaton with n states 
(and an arbItrary number of dead-ends). Let us denote the states 
of 
 by 0,1.. .,n and consider them as the elements of N/(n+l) in 
order to speak convenIently about state (i+l) as following state 
i. 0 is considered as the InitIal state. 
For the purposes of proof, we shall introduce some 
auxiliary automata. 
i will denote the automaton that has the 


same table of transitIons and the same set of final macrostates 
. 
as 
, but the initial state of 'U. is i . 
. wIll denote the 
t t 
automaton derived from 
 by considering state i as the initial 


state and i+l as a dead-end. This means that the number of 
states decreases by one (because of the exclusion of i+1), and 
the number of dead-ends increases by one (because of the 
addition of i+l). Further, all transitions having i+l at the 
bottom are excluded, and all final macrostates containing i+l 


are excluded, while the transitions having i+l on the top are 
kept (but i+l is considered as a dead-end and not as a state). 
Automata 
. have n states (
 has n+l states). By the induction 
t 


assumption, for any i=O,... ,n-l, there exists a strategy set M i 
I 
which satisfies the following condition: tree T is rejected by 
automaton 
i If and only if there exists a rejectIng strategy 
for 
i on T based on Mt' This strategy set contains a certain 



-257- 


number of copies of each state of 
., hence, the copies of all 
t 
states of 'U except for 1+1. Assume that sets M. are pairwise 
t 
dIsjoint. We sha 11 now describe the strategy set M for '!l. It 
contains all the copies contained in the sets M.. (In this way, 
t 


a copy of i belongs to M if and only if it belongs to one of the 
sets M k . Note that M k does not contain any copy of the state 
k+1). Let us describe what IS the result of the actIon of the 
trans it ion i 
 j on copy c of state 1. Let cEM k . If the 
o 
result of the action of the transItion i 
 j on C is defined 
in M k (i.e. if j
ko+l; i
ko+1 is always true because c belongs 
o 
to M k ), then it will be consIdered as the result of the action 
o 
of i 
 j on C in M. Otherwise (i.e. when j=ko+1), the result 
is defined as the initial copy of state j in set MJ. To finish 
the description of set M, it remains to designate its inItial 
copy. It will be the initial copy of state 0 In Mo' 
The above constructed set M is the required set: automatop 

 rejects T If and only if there exists a rejectIng strategy for 

 based on M. To prove this, we shall need the following two 
lemmas. 


k
mm
_

 Automaton 
i accepts tree T if and only if 
automaton 
i accepts tree T', which is obtained by taking T and 
adding the dead-end i+l into the vertices which are roots of 
subtrees accept ed by 'U. 1 . 
t + 


Before formulating the second lemma, let us Introduce a 
notation: M t IS the strategy set which differs from M in a 



-258- 


unique point - the initial copy is the initial copy of state i 
in M.. 
t 


i 
k



_

 There exists a rejecting strategy based on M for 
automaton 
i on tree T if and only if there extsts a rejecting 
strategy (based on M i ) for automaton $t on tree T", which is 
obtained by taking T and adding the dead-end 1+1 to the vertices 
which are roots of subtrees on whtch there is no rejecting 
strategy for 
i+t based on M i + t . 


Proof of Lemma 3. This lemma has nothing to do 
strategies, and therefore it is simple. If 
i accepts 
cutting the accepting run at the point, where it goes 
state i+1, we get an accepting run of automaton 
i on 
cut parts guarantee that the dead-ends i+1 are allowed. 
On the other hand, if 
i has an accepting run on T' , 
"gluing" at the dead-ends i+l, which occur in this run, 
accepting runs of automaton 
i+t (they exist because 
dead-ends 1+1 are allowed), we get a run of 
ion T. 


with 


T, then, 
through 
T': the 


then, 
the 
the 


Proof of Lemma 4. This lemma is more complicated because of 
its connectIon with strategIes. To clarify its formulation and 
understand its analogy with Lemma 3, let us introduce the 
following terminology. Let us say that an automaton 
quasi-accepts a tree, if there is no rejecting strategy for this 
automaton on this tree (strategy based on the corresponding set 
described in the lemma). Then Lemma 4 can be reformulated as 
follows: 



-259- 


Automaton 
i quasi-accepts tree T if and only if automaton 
. 
t 
quasi-accepts tree T" , which is obtained by taking T and 
i ns er t i ng the dead-end i+1 into the vertices which are roots of 
subtrees quasi-accepted by 
. t. 
t + 


Hence, suppose that there eXIsts a rejecting strategy on 
tree Tn based on M. for automaton 
 . . All we need is to 
t t 
construct a rejecting strategy based on M t for 
. on T. As first 
t 


step, we have to divide into left and right the same 
copy-transitions as in the strategy for 
. (here, the definition 
t 
of action of a transition on a copy in M. is used). In the 
t 
following step we select the same copies as in the strategy for 


$i except for one case: it is possible that the dead-end i+l has 
been selected for the strategy for 
i' we then select (the 
initial copy in M i + 1 of) state i+1. But as the dead-end has been 
selected, this means that it IS not allowed, in other words, 
there is a rejecting strategy for 
t+l based on M i + 1 on the 
subtree, the root of which is in the vertex labelled by this 
dead-end. Thus this strategy divides the copy-transitions having 


at the bottom the initial copy of i+l. Therefore, we can go on 
with the construction of the strategy for 
 . : the 
t 
copy-transitions at the bottom of which there is a copy of a 
state different from i+l, will be divIded into left and right 


copies as in the strategy for 
i' and the copy-transitions, at 
the bottom of which there IS the initial copy of be 
divided by following the existing strategies for the 
following steps, we can proceed in a similar a 
strategy for 
 i . 


i+l, WIll 
'U. 1. In 
t + 
way and get 



-260- 


However, in the previous analysis, there is an important 
point we have not discussed. Indeed, the selected copies could 


have been selected for different reasons: following a 

i-strategy and at the same tIme following an 
i+l-strategy, or 
even several 
i+l-strategies! The picture represents one of 
these situations: circles contain selected copies, full lines 
represent transitions due to 
i-strategy, dotted lines represent 
transitions due to 
i+l-strategy. In the left top cIrcle, we see 
a copy A which has been selected for three reasons. One 
selection has been done according to 
i-strategy, the second 
according to 
i+l starting at C, and the third according to 

i+l-strategy starting at E. Copy B has been selected for two 
reasons: one selection has been made following 
i-strategy and 
another followIng 
i+l-strategy starting at E. What should be 
done in such cases? Which strategy should we follow? Answer: if 
possible, follow 
i+l-strategies and, among them, the strategy 
coming into effect as early as possible. This leads to the goal, 
namely, the rejecting strategy for 
i' Indeed, the condition for 
dead-ends is satisfied. Let us verify the condition for paths. 
Take an arbItrary one. Either it is out of range of 



-261- 



i+t-strategy (then the limit is not final SInce 
i-strategy IS 
rejecting), or, if not, it never leaves this range (because we 
prefer 
i+l-strategies). It may only happen that It comes Into 
the range of another, earlier 
i+l-strategy. But this is 
possible only a finite number of times. Hence, beginning at a 
certaIn point, the path lIes entIrely In the range of one 

i+l-strategy and its limit is not fInal. 
We have proved one Implication of Lemma 4. The opposite 
Implication is much simpler. Let us have a rejectIng strategy 
for 
i on T. Consider those selected copies of state i+l, whIch 
have been selected as the first ones (this means that on the 
paths they lie on there are no other copies of i+l before them). 
These copies are initial in M i + 1 (by the rules of application of 
transitions to the copies in M). Therefore, subtrees with roots 
in the vertIces labelled by these copies have a rejecting 
strategy for 
i+l (based on M L ). Hence, by considering these 
copies as dead-ends, we get a rejecting strategy for 
i on T H 


based on M . . 
t 
The proofs of Lemma 3 and 4 are complete. In the followIng 
section, we shall use in fact only that part of Lemma 3 which 
has been proved as second and that part of Lemma 4 WhICh has 


been proved as first. The converse implications were included 
just to make the statements complete. 


Last part of the induction step 
What is the outcome of the Lemmas proved in the previous 
paragraph? Knowing that tree T' of Lemma 3 cOIncIdes wIth tree 
I" of Lemma 4, we can use the induction assumptIon for automaton 



-262- 



i and get what we need - the existence of an accepting run of 

i on T would be equivalent to the fact that there is no 
rejecting strategy for 
i on T. However, the assertion T'=T" 
states that the existence of an accepting run for 
i+l is 
equivalent to the fact there being no rejecting strategy for 

i+l which has the same number of states as 
i! Nevertheless, 
the proved Lemmas are of some value. 
We shall consider two cases: in the first, we shall assume 
that the set S of all states is final, in the second, that it is 
not. In the first case, we shall apply Lemma 4 and use the same 
Ideas as when proving Lemma 3. In the second, Lemma 3 and ideas 
of the proof of Lemma 4 will be used. 
First case. The set of all states is final. Let us prove 
that if there is no rejecting strategy on T for 
o' then there 
is an acceptIng run for 
o' As there is no rejecting strategy on 
T for 
o' there is an accepting run on T" (constructed in 
Lemma 4) for 
o (remember that for 
o' by induction assumption, 


the existence of a run is equivalent to the non-existence of a 
strategy). For what reason is this not a run for 
o? In some 
places, it comes to dead-ends 1 allowed in T" . Subtrees with 


roots in these vertices do not have any rejectIng strategy for 

1' hence, even wIthout having an accepting run for 
t (which 
would permit us to use directly Lemma 3), they have at least a 
run for 
1' which will be accepting if we add at certain places 
dead-and 2. But in those places it IS possible to start the run 
of 
2 and so on. We get a run for 
o by "gluing" all these runs 
together. It will be accepting: any path either lies in a run of 
some of the 
i'S? (from a certain point) - (and has therefore a 



-L63- 


final limit) - or it describes a circle, going infinitely many 
times from $0 to $t' from 
t to 
2'. .., from 
n to 
O' its limit 
being equal to the set of all states, which is fInal by 
assumption. So much for the fIrst case. 
Second case. The set of all states is not final. ThIS case 
is more complicated; at this pOInt we shall use the structure of 
the strategy set M we have constructed. Let us prove, supposing 
that there is no accepting run, the eXIstence of a rejecting 
strategy. Hence, let us suppose there is no accepting run on 
tree T for automaton 
o. By Lemma 3, as there is no accepting 
run for 
o on T', which was obtained from T by addIng in some 
vertices dead-end 1 there IS a rejecting strategy for 
o' What 
does it lack in order to be an 
o-strategy? It contains at 
several places possible dead-ends 1. When constructing 

o-strategy, at the same places there appear possible copIes of 
state 1 (Initial copies in M t ). What should be done 
The subtrees with root in the vertices labelled by 
do not have any accepting run for 
t. We do not 
there is a rejecting strategy on these subtrees, 
allow us to use Lemma 4). As there is no acceptIng run, we can 
once more apply Lemma 3 and state that by adding dead-end 2, we 
get trees without accepting runs for 
t on it and hence (by the 
induction assumption) with a rejecting strategy for 
1' Using 
these rejecting strategies, It is possible to go on with the 
construction of 
o-strategy. Note that, untIl now, we have not 
met any problematical case (similar to those which were 
discussed in the proof of Lemma 4), because the 
o-strategy 
deals with copies from Mo and 
t-strategy deals with copies from 


with them? 
these copIes 
know whether 
(which would 



-264- 


M J . Going on wi th this procedure, we put strategies for 

2".' '
n into actIon. The strategy for !B k + 1 comes into action 
at the places in which the strategy for 
k has possible 


dead-ends k+1: in these places, there is no accepting run for 

k+l' At a certain moment, the circle is completed and it is 
necessary to use the 
o-strategy, and so on. Now, the question 
can arise about the choice between the different strategies for 

.. The answer is - the one which is put into action earlier. We 
L 
shall verify whether we indeed get a rejecting strategy for 
o' 
The condItion with dead-ends is obviously satIsfied. Let us 
verIfy the conditIon for paths. Every probable path is of one of 
the two following kinds: eIther the path, starting from a 
certaIn point, goes through the copies of only one strategy set 
Mt, or goes infinItely many times from the strategy sets M j to 
the following ones, M J + t " In the fIrst case, the path, beginning 
at a certain place, follows the strategy for 
i; to switch from 
one strategy to another is possible only if the second one 
started earlier. Therefore, such switches are possible only 
finitely many times and the path almost everywhere coincides 
with the probable path of the strategy for 
i and its limit is 
not final. In the second case, the path passing from M to M l ' 
J J+ 
goes through the initial copy of MJ and therefore its limit is 
the set of all states, which is (by assumption) not final. 
So, the case when the set of all states is not final, is 
finished and the inductive proof of Theorem 4' is hence 
completed. Thus we have proved the above formulated Theorem 4. 



-265- 


Final stage of the proof of the complementation theorem 


Corresponding to the announced plan, it remains to prove 
the following statement. 
Ih
Q[

_

 Let L be an alphabet, 
 an automaton on 
-trees 
(without any dead-end!), M a strategy set. Then the set of all 
I-trees on which there exists rejecting strategy for 
 based on 
M is recognizable. 
To prove this statement, introduce the notion of a 
semiautomaton on 2-trees. A semiautomaton is given by a set of 
inner states S, a table of transitions, a set of Initial states 
(until now, everything listed has been the same as in the case 
of the usual automata on 2-trees) and moreover, a certain 
automaton 
 on Q-words in the alphabet S. A run is defIned In 
the same manner as in the case of usual automata. It is called 
accepting if all paths, regarded as sequences of states (i.e
 
elements of S) are rejected by 
. The sets of trees accepted by 
semiautomata will be called (temporary) semirecognizable. It is 
clear that any recognizable set is semirecognizable. The 
following Lemma states that the converse implication is also 
true. 







_

 Any semirecognizable set is recognizable. 
Proof. It is known (see [4]) that every (nondeterministic) 
automaton on Q-words is equIvalent to some deterministic one. 
Hence, the automaton 
, belonging to the given semiautomaton 
, 
can be considered as determInIstIc. Then, it is not difficult to 
construct an automaton WhICh will be equivalent to the 
semiautomaton 
. Its set of states has to be the product of the 



-266- 


sets of states of 
 and
; its run is in fact constructed from a 
run of 
 and the runs of 
 on Q-words (letters are the states of 

) which lie in the chosen run of along all paths. 
Now It remains to prove that the set of all trees, on which 


there exists a rejecting strategy for 
 based on M is 
semirecognizable. But this is quite clear: it is not difficult 
to for m u 1 a t I
 the notion of strategy itself in the form of an 
accepting run of a semiautomaton. The different possibilities of 


dIviding copy-transitions to left and right ones correspond to 
the possibilities of continuing the run in different ways. It is 
possible to consider the states of the semiautomaton as pairs of 
disjoint sets of copy transitions (the members of the pair 
correspond to the sets of left and right copy-transitions). 
Automaton 
 wIll look for the paths which do not satisfy the 
definition of a strategy (i.e. the paths with final limits) and 
hence, the acceptance by automaton $ of the sequences of states 
lying along all paths will indeed mean that the strategy is 
rejecting. 
In this way, we have proved Theorem 4 and hence we have 
proved that the complement of a recognizable set is 
recognizable. 


Acknoledgments. The author is sincerely grateful to 
J.Ryslinkova, A.Shen, W.Thomas and N.Vereshchagin for the help 
In preparing this text. 



-267- 


References 


[1] Rabin
 M.O. DecidabIIlty of second order theories and 
automata on infinIte trees. - TAMS, 1969, 171, p.1-35. 
[2] Rabin, M.O. Decidability and definability in second order 
theor ies. - In: Actes du Congres des Math., Nice, 1970, 1 , 
p.239-277. 
[3] Gurevich Y., Harrington L. Trees, automata and games. - In: 
Proceedings ACM Symp. on the Theory of Computing, San Francisco, 
1982, May, p.60-65. 
[4] McNaughton R. TestIng and generating infinIte sequences by a 
f ini te automaton _ Informat ion and contro 1 , 1966, 9, tf5, 
p.521-530.