Weak alternating automata are not that weak.
Automata on infinite words are used for specification and verification of nonterminating programs. Different types of automata induce different levels of expressive power, of succinctness, and of complexity. Alternating automata have both existential and universal branching modes and are particularly suitable for specification of programs. In a weak alternating automata the state space is partitioned into partially ordered sets, and the automaton can proceed from a certain set only to smaller sets. Reasoning about weak alternating automata is easier than reasoning about alternating automata with no restricted structure. Known translations of alternating automata to weak alternating automata involve determinization, and therefore involve a double-exponential blow-up. In this paper we describe a quadratic translation, which circumvents the need for determinization, of Bchi and co-Bchi alternating automata to weak alternating automata. Beyond the independent interest of such a translation, it gives rise to a simple complementation algorithm for nondeterministic Bchi automata.
INTRODUCTION
Finite automata on innite objects were rst introduced in the 60's. Motivated
by decision problems in mathematics and logic, Buchi, McNaughton, and Rabin
developed a framework for reasoning about innite words and innite trees [Buchi
1962; McNaughton 1966; Rabin 1969]. The framework has proved to be very pow-
erful. Automata, and their tight relation to second-order monadic logics were the
key to the solution of several fundamental decision problems in mathematics and
logic [Thomas 1990]. Today, automata on innite objects are used for specication
First author's address: O. Kupferman, School of Computer Science and Engineering, Hebrew Uni-
versity, Jerusalem 91904, Israel. Email: orna@cs.huji.ac.il, URL: http://www.cs.huji.ac.il/  orna.
Second author address: M. Y. Vardi, Department of Computer Science, Rice University, Houston
Partly
supported by NSF grants CCR-9700061 and CCR-9988322 and by a grant from the Intel Corporation

Permission to make digital/hard copy of all or part of this material without fee for personal
or classroom use provided that the copies are not made or distributed for prot or commercial
advantage, the ACM copyright/server notice, the title of the publication, and its date appear, and
notice is given that copying is by permission of the ACM, Inc. To copy otherwise, to republish,
to post on servers, or to redistribute to lists requires prior specic permission and/or a fee.
c
ACM Transactions on Computational Logic, Vol. TBD, No. TBD, TBD TBD, Pages 111{131.
Kupferman and Moshe Y. Vardi
and verication of nonterminating programs. The idea is simple: when a program
is dened with respect to a nite set P of propositions, each of the program's states
can be associated with a set of propositions that hold in this state. Then, each
of the program's computations induces an innite word over the alphabet 2 P , and
the program itself induces a language of innite words over this alphabet. This
language can be dened by an automaton. Similarly, a specication for a pro-
gram, which describes all the allowed computations, can be viewed as a language
of innite words over 2 P , and can therefore be dened by an automaton. In the
automata-theoretic approach to verication, we reduce questions about programs
and their specications to questions about automata. More specically, questions
such as satisability of specications and correctness of programs with respect to
their specications are reduced to questions such as nonemptiness and language
containment [Vardi and Wolper 1986; Kurshan 1994; Vardi and Wolper 1994]. The
automata-theoretic approach separates the logical and the combinatorial aspects of
reasoning about programs. The translation of specications to automata handles
the logic and shifts all the combinatorial di-culties to automata-theoretic problems.
As automata on nite words, automata on innite words either accept or reject an
input word. Since a run on an innite word does not have a nal state, acceptance
is determined with respect to the set of states visited innitely often during the run.
There are many ways to classify an automaton on innite words. One is the type of
its acceptance condition. For example, in Buchi automata, some of the states are
designated as accepting states, and a run is accepting i it visits states from the
accepting set innitely often [Buchi 1962]. Dually, in co-Buchi automata, a run is
accepting i it visits states from the accepting set only nitely often. More general
are Muller automata. Here, the acceptance condition is a set  of sets of states,
and a run is accepting i the set of states visited innitely often is a member of
[Muller 1963].
Another way to classify an automaton on innite words is by the type of its
branching mode. In a deterministic automaton, the transition function - maps
a pair of a state and a letter into a single state. The intuition is that when the
automaton is in state q and it reads a letter , then the automaton moves to state
-(q; ), from which it should accept the su-x of the word. When the branching
mode is existential or universal , - maps q and  into a set of states. In the existential
mode, the automaton should accept the su-x of the word from one of the states
in the set, and in the universal mode, it should accept the su-x from all the states
in the set. In an alternating automaton [Chandra et al. 1981], both existential and
universal modes are allowed, and the transitions are given as Boolean formulas over
the set of states. For example, -(q; means that the automaton
should accept the su-x of the word either from state q 1 or from both states q 2 and
It turns out that dierent types of automata have dierent expressive power.
For example, unlike automata on nite words, where deterministic and nondeterministic
(existential) automata have the same expressive power, deterministic
Buchi automata are strictly less expressive than nondeterministic Buchi automata
[Landweber 1969]. That is, there exists a language L over innite words such that
L can be recognized by a nondeterministic Buchi automaton but cannot be recognized
by a deterministic Buchi automaton. It also turns out that some types of
Weak Alternating Automata Are Not That Weak  113
automata may be more succinct than other types. For example, though alternating
Buchi automata are as expressive as nondeterministic Buchi automata (both
recognize exactly all !-regular languages), alternation makes Buchi automata exponentially
more succinct. That is, translating an alternating Buchi automaton to
a nondeterministic one might involve an exponential blow-up (see [Drusinsky and
Harel 1994]).
Since the combinatorial structure of alternating automata is rich, translating
specications to alternating automata is much simpler than translating them to
nondeterministic automata. Alternating automata enable a complete partition between
the logical and the combinatorial aspects of reasoning about programs, and
they give rise to cleaner and simpler verication algorithms [Vardi 1996]. The ability
of alternating automata to switch between existential and universal branching
modes also makes their complementation very easy. For example, in order to complement
an alternating Muller automaton on innite words, one only has to dualize
its transition function and acceptance condition [Miyano and Hayashi 1984; Lindsay
1988]. In contrast, complementation is a very challenging problem for nondeterministic
automata on innite words. In particular, complementing a nondeterministic
Buchi automaton involves an exponential blow-up [Safra 1988; Michel 1988].
In [Muller et al. 1986], Muller et al. introduced weak alternating automata.
In a weak alternating automaton, the automaton's set of states is partitioned into
partially ordered sets. Each set is classied as accepting or rejecting. The transition
function is restricted so that in each transition, the automaton either stays at the
same set or moves to a set smaller in the partial order. Thus, each run of a
alternating automaton eventually gets trapped in some set in the partition.
Acceptance is then determined according to the classication of this set. The special
structure of weak alternating automata is re
ected in their attractive computational
properties and makes them very appealing. For example, while the best known
complexity for solving the membership problem for Buchi alternating automata is
quadratic time, we know how to solve the membership problem for weak alternating
automata in linear time [Kupferman et al. 2000].
Weak alternating automata are a special case of Buchi alternating automata.
Indeed, the condition of getting trapped in an accepting set can be replaced by a
condition of visiting states of accepting sets innitely often. The other direction, as
it is easy to see, is not true. In fact, it is proven in [Rabin 1970; Muller et al. 1986],
that, when dened on trees, a language L can be recognized by a weak alternating
automaton i both L and its complement can be recognized by Buchi nondeterministic
automata. Nevertheless, when dened on words, weak alternating automata
are not less expressive than Buchi alternating automata, and they can recognize all
the !-regular languages. To prove this, [Muller et al. 1986; Lindsay 1988] suggest a
linear translation of deterministic Muller automata to weak alternating automata.
Using, however, the constructions in [Muller et al. 1986; Lindsay 1988] in order
translate a nondeterministic Buchi or co-Buchi automaton A into a weak alternating
automaton, one has no choice but to rst translate A into a deterministic Muller
automaton. Such a determinization involves an exponential blow-up [Safra 1988].
Even worse, if A is an alternating automaton, then its determinization involves a
doubly-exponential blow-up, and hence, so does the translation to weak alternating
automata. Can these blow-ups be avoided?
114  Orna Kupferman and Moshe Y. Vardi
In this paper we answer this question positively. We describe a simple quadratic
translation of Buchi and co-Buchi alternating automata into weak alternating au-
tomata. Beyond the independent interest of such a translation, it gives rise to a
simple complementation algorithm for nondeterministic Buchi automata. The closure
of nondeterministic Buchi automata under complementation plays a crucial
role in solving decision problems of second order logics. As a result, many eorts
have been put in proving this closure and developing simple complementation al-
gorithms. In [Buchi 1962], Buchi suggested a complementation construction, which
indeed solved the problem, yet involved a complicated combinatorial argument and
a doubly-exponential blow-up in the state space. Thus, complementing an automaton
with n states resulted in an automaton with 2 2 O(n)
states. In [Sistla et al.
1987], Sistla et al. suggested an improved construction, with only 2 O(n 2 ) states,
which is still, however, not optimal. Only in [Safra 1988], Safra introduced an optimal
determinization construction, which also enabled a 2 O(n log n) complementation
construction, matching the known lower bound [Michel 1988]. Another 2 O(n log n)
construction was suggested by Klarlund in [Klarlund 1991], which circumvented the
need for determinization.
While being the heart of many complexity results in verication, the optimal
constructions in [Safra 1988; Klarlund 1991] are complicated. In particular, the
intricacy of the algorithms makes their implementation di-cult. We know of no
implementation of Klarlund's algorithm, and the implementation of Safra's algorithm
[Tasiran et al. 1995] has to cope with the involved structure of the states in
the complementary automaton. The lack of a simple implementation is not due to
a lack of need. Recall that in the automata-theoretic approach to verication, we
check correctness of a program with respect to a specication by checking containment
of the language of the program in a language of an automaton that accepts
exactly all computations that satisfy the specication. In order to check the latter,
we check that the intersection of the program with an automaton that complements
the specication automaton is empty. Due to the lack of a simple complementation
construction, verication tools have to restrict the specication automaton or
improvise other solutions. For example, in the verication tool COSPAN [Kurshan
1994], the specication automaton must be deterministic (it is easy to complement
deterministic automata [Clarke et al. 1993]). In the verication tool SPIN [Holz-
mann 1991], the user has to complement the automaton by himself; thus, together
with the program, SPIN gets as input a nondeterministic Buchi automaton, called
the Never-Claim, which accepts exactly all computations that do not satisfy the
specication.
The complementary automaton constructed in our procedure here is similar to the
one constructed in [Klarlund 1991], but as our construction involves alternation, it
is simpler and easily implementable. Consider a nondeterministic Buchi automaton
B. We can easily complement B by regarding it as a universal co-Buchi automaton.
using our construction, we translate this complementary automaton to a
alternating automaton W . By [Miyano and Hayashi 1984], weak alternating
automata can be translated to nondeterministic Buchi automata. Applying their
(exponential yet simple) translation to W , we end up with a nondeterministic Buchi
automaton N that complements B. For B with n states, the size of N is 2 O(n log n) ,
Weak Alternating Automata Are Not That Weak  115
meeting the known lower bound [Michel 1988] and the complicated constructions
suggested in [Safra 1988; Klarlund 1991].
2. ALTERNATING
Given an alphabet , an innite word over  is an innite sequence
of letters in . We denote by w l the su-x  l   l+1   l+2    of w. An automaton on
innite words is  is the input alphabet, Q is a nite
set of states,  is an initial state, and
is an acceptance condition (a condition that denes a subset of Q
(q; ) is the set of states that A can move into when it is in state q and it reads the
letter . Since the transition function of A may specify many possible transitions
for each state and letter, A is not deterministic. If  is such that for every q 2 Q
and  2 , we have that j(q; then A is a deterministic automaton.
A run of A on w is a function r in (i.e., the run starts
in the initial state) and for every l  0, we have r(l (i.e., the run
obeys the transition function). In automata over nite words, acceptance is dened
according to the last state visited by the run. When the words are innite, there
is no such thing \last state", and acceptance is dened according to the set Inf (r)
of states that r visits innitely often, i.e.,
for innitely many l 2 IN; we have
As Q is nite, it is guaranteed that Inf (r) 6= ;. The way we refer to Inf (r) depends
on the acceptance condition of A. Several acceptance conditions are studied in the
literature. We consider here two:
|Buchi automata, where   Q, and r accepts w i Inf (r) \  6= ;.
|co-Buchi automata, where   Q, and r accepts w i Inf (r) \
Since A is not deterministic, it may have many runs on w. In contrast, a deterministic
automaton has a single run on w. There are two dual ways in which
we can refer to the many runs. When A is an existential automaton (or simply
a nondeterministic automaton, as we shall call it in the sequel), it accepts an input
word w i there exists an accepting run of A on w. When A is a universal
automaton, it accepts an input word w i all the runs of A on w are accepting.
Alternation was studied in [Chandra et al. 1981] in the context of Turing machines
and in [Brzozowski and Leiss 1980; Chandra et al. 1981; Miyano and Hayashi 1984]
for nite automata. In particular, [Miyano and Hayashi 1984] studied alternating
automata on innite words. Alternation enables us to have both existential and
universal branching choices.
For a given set X , let (X) be the set of positive Boolean formulas over X (i.e.,
Boolean formulas built from elements in X using ^ and _), where we also allow the
formulas true and false. For Y  X , we say that Y satises a formula
i the truth assignment that assigns true to the members of Y and assigns false to
the members of X n Y satises . For example, the sets fq both
satisfy the formula (q 1 while the set fq 1 does not satisfy this formula.
Consider an automaton A as above. We can represent (Q). For ex-
ample, a transition (q; of a nondeterministic automaton A can be
written as (q; If A is universal, the transition can be written as
Kupferman and Moshe Y. Vardi
While transitions of nondeterministic and universal automata
correspond to disjunctions and conjunctions, respectively, transitions of alternating
automata can be arbitrary formulas in B (Q). We can have, for instance, a transition
meaning that the automaton accepts a su-x
w i of w from state q, if it accepts w i+1 from both q 1 and q 2 or from both q 3 and
q 4 . Such a transition combines existential and universal choices.
Formally, an alternating automaton on innite words is a tuple
in , and  are as in automata, and
function. While a run of a nondeterministic automaton is a function r : IN ! Q, a
run of an alternating automaton is a tree r : T r ! Q for some T r  IN  . Formally,
a tree is a (nite or innite) nonempty prex-closed set T  IN  . The elements of
are called nodes, and the empty word " is the root of T . For every x 2 T , the
nodes x  c 2 T where c 2 IN are the children of x. A node with no children is a
leaf . We sometimes refer to the length jxj of x as its level in the tree. A path  of a
tree T is a set   T such that  2  and for every x 2 , either x is a leaf, or there
exists a unique c 2 IN such that x  c 2 . Given a nite set , a -labeled tree is a
maps each node of T to a letter in .
A run of A on an innite word is a Q-labeled tree hT r ; ri such that
the following hold:
in .
There is a (possibly empty) set
such that S satises  and for all 1  c  k, we have x  c 2 T r
and r(x  c) = q c .
For example, if -(q in ;  0 possible runs of A on w have a
root labeled q in , have one node in level 1 labeled q 1 or q 2 , and have another node in
level 1 labeled q 3 or q 4 . Note that if  = true, then x need not have children. This
is the reason why T r may have leaves. Also, since there exists no set S as required
for false, we cannot have a run that takes a transition with
A run hT r ; ri is accepting i all its innite paths, which are labeled by words
in the acceptance condition. A word w is accepted i there exists an
accepting run on it. Note that while conjunctions in the transition function of A
are re
ected in branches of hT r ; ri, disjunctions are re
ected in the fact we can
have many runs on the same word. The language of A, denoted L(A), is the set of
innite words that A accepts. Thus, each word automaton denes a subset of  ! .
We denote by L(A) the complement language of A, that is the set of all words in
In [Muller et al. 1986], Muller et al. introduce weak alternating automata (WAAs).
In a WAA, the acceptance condition is   Q, and there exists a partition of Q into
disjoint sets, Q i , such that for each set Q i , either Q i  , in which case Q i is an
accepting set, or Q i \ ;, in which case Q i is a rejecting set. In addition, there
exists a partial order  on the collection of the Q i 's such that for every q 2 Q i and
occurs in -(q; ), for some  2 , we have Q
transitions from a state in Q i lead to states in either the same Q i or a lower one. It
follows that every innite path of a run of a WAA ultimately gets \trapped" within
some Q i . The path then satises the acceptance condition if and only if Q i is an
accepting set. Thus, we can view a WAA with an acceptance condition  as both a
Weak Alternating Automata Are Not That Weak  117
Buchi automaton with an acceptance condition , and a co-Buchi automaton with
an acceptance condition Q n . Indeed, a run gets trapped in an accepting set i it
visits innitely many states in , which is true i it visits only nitely many states
in Q n .
3. USEFUL OBSERVATIONS ON RUNS OF ALTERNATING CO-B
UCHI
Consider a co-Buchi alternating automaton ri be an
accepting run of A on a word w. For two nodes x 1 and x 2 in T r , we say that
x 1 and x 2 are similar i jx We say that the run
ri is memoryless i for all similar nodes x 1 and x 2 , and for all y 2 IN  , we
have that x 1  y Intuitively, similar
nodes correspond to two copies of A that have the same \mission": they should
both accept the su-x w jx1 j from the state r(x 1 ). In a memoryless run, subtrees
of hT r ; ri with similar roots coincide. Thus, same missions are fullled in the same
way. It turns out that when we consider runs of co-Buchi automata, we can restrict
ourselves to memoryless runs. Formally, we have the following theorem.
Theorem 3.1. [Emerson and Jutla 1991] If a co-Buchi automaton A accepts a
word w, then there exists a memoryless accepting run of A on w.
We note that [Emerson and Jutla 1991] proves a stronger result, namely the
existence of memoryless accepting runs for parity alternating automata. Since the
co-Buchi acceptance condition is a special case of the parity acceptance condition,
the result cited above follows.
It is easy to see that for every run hT r ; ri, every set of more
than n nodes of the same level contains at least two similar nodes. Therefore, in a
memoryless run of A, every level contains at most n nodes that are roots of dierent
subtrees. Accordingly, we represent a memoryless run hT r ; ri by an innite dag
(directed acyclic
QIN is such that hq; li 2 V i there exists x 2 T r with
For example, hq in ; 0i is the only vertex of G r in Q f0g.
l0 (Q flg)  (Q fl+ 1g) is such that E(hq; li; hq there exists
Thus, G r is obtained from hT r ; ri by merging similar nodes into a single vertex. We
say that a vertex hq 0 ; l 0 i is a successor of a vertex hq; li i E(hq; li; hq 0 ; l 0 i). We say
that is reachable from hq; li i there exists a sequence hq
of successive vertices such that hq; li there exists i  0 such that
Finally, we say that a vertex hq; li is an -vertex i q 2 . It
is easy to see that hT r ; ri is accepting i all paths in G r have only nitely many
-vertices.
Consider a (possibly nite) dag G  G r . We say that a vertex hq; li is endangered
in G i only nitely many vertices in G are reachable from hq; li. We say that a
vertex hq; ii is safe in G i all the vertices in G that are reachable from hq; li are
not -vertices. Note that, in particular, a safe vertex is not an -vertex.
Given a memoryless accepting run hT r ; ri, we dene an innite sequence G 0
dags inductively as follows.
Kupferman and Moshe Y. Vardi
li j hq; li is endangered in G 2i g.
li j hq; li is safe in G 2i+1 g.
Lemma 3.2. For every i  0, there exists l i such that for all l  l i , there are at
most n i vertices of the form hq; li in G 2i .
Proof. We prove the lemma by an induction on i. The case where
from the denition of G 0 . Indeed, in G r all levels l  0 have at most n vertices of
the form hq; li. Assume that the lemma's requirement holds for i, we prove it for
1. Consider the dag G 2i . We distinguish between two cases. First, if G 2i is
nite, then G 2i+1 is empty, G 2i+2 is empty as well, and we are done. Otherwise, we
claim that there must be some safe vertex in G 2i+1 . To see this, assume, by way
of contradiction, that G 2i is innite and no vertex in G 2i+1 is safe. Since G 2i is
innite, G 2i+1 is also innite. Also, each vertex in G 2i+1 has at least one successor.
Consider some vertex hq 0 ; l 0 i in G 2i+1 . Since, by the assumption, it is not safe,
there exists an -vertex hq 0
reachable from hq be a successor
of hq 0
i. By the assumption, hq 1 ; l 1 i is also not safe. Hence, there exists an -
vertex
reachable from hq 1 be a successor of hq 0
By the
assumption, is also not safe. Thus, we can continue similarly and construct
an innite sequence of vertices
i such that for all i, the vertex hq 0
an -vertex reachable from hq j ; l j i, and hq j+1 ; l j+1 i is a successor of hq 0
Such a
sequence, however, corresponds to a path in hT r ; ri that visits  innitely often,
contradicting the assumption that hT r ; ri is an accepting run.
So, let hq; li be a safe vertex in G 2i+1 . We claim that taking l
the lemma's requirement. That is, we claim that for all j  l, there are at most
vertices of the form hq; ji in G 2i+2 . Since hq; li is in G 2i+1 , it is not
endangered in G 2i . Thus, there are innitely many vertices in G 2i that are reachable
from hq; li. Hence, by Konig's Lemma, G 2i contains an innite path hq; li;
:. For all k  1, the vertex hq k ; l + ki has innitely many vertices
reachable from it in G 2i and thus, it is not endangered in G 2i . Therefore, the path
exists also in G 2i+1 . Recall that hq; li is safe. Hence,
being reachable from hq; li, all the vertices ki in the path are safe as well.
Therefore, they are not in G 2i+2 . It follows that for all j  l, the number of vertices
of the form hq; ji in G 2i+2 is strictly smaller than their number in G 2i . Hence, by
the induction hypothesis, we are done.
By Lemma 3.2, G 2n is nite. Hence the following corollary.
Corollary 3.3. G 2n+1 is empty.
Each vertex hq; li in G r has a unique index i  1 such that hq; li is either endangered
in G 2i or safe in G 2i+1 . Given a vertex hq; li, we dene the rank of hq; li, denoted
rank(q; l), as follows.
2i If hq; li is endangered in G 2i .
li is safe in G 2i+1 .
For denote the set f0; denote the set of
odd members of [k]. By Corollary 3.3, the rank of every vertex in G r is in [2n].
Weak Alternating Automata Are Not That Weak  119
Recall that when hT r ; ri is accepting, all the paths in G r visit only nitely many -
vertices. Intuitively, rank(q; l) hints how di-cult it is to get convinced that all the
paths of G r that visit the vertex hq; li visit only nitely many -vertices. Easiest
to get convinced about are vertices that are endangered in G 0 . Accordingly, they
get the minimal rank 0. Then come vertices that are safe in the graph G 1 , which
is obtained from G 0 by throwing away vertices with rank 0. These vertices get the
rank 1. The process repeats with respect to the graph G 2 , which is obtained from
G 1 by throwing away vertices with rank 1. As before, we start with the endangered
vertices in G 2 , which get the rank 2. We continue with the safe vertices in G 3 ,
which get the rank 3. The process repeats until all vertices get some rank. Note
that no -vertex gets an odd rank.
In the lemmas below we make this intuition formal.
Lemma 3.4. For every vertex hq; li in G r and rank i 2 [2n], if hq; li 62 G i , then
Proof. We prove the lemma by an induction on i. Since G , the case
immediate. For the induction step, we distinguish between two cases.
For the case i +1 is even, consider a vertex hq; li 62 G i+1 . If hq; li 62 G i , the lemma's
requirement follows from the induction hypothesis. If hq; li 2 G i , then hq; li is safe
in G i . Accordingly, rank(q; meeting the lemma's requirement. For the case
consider a vertex hq; li 62 G i+1 . If hq; li 62 G i , the lemma's requirement
follows from the induction hypothesis. If hq; li 2 G i , then hq; li is endangered in
G i . Accordingly, rank(q; meeting the lemma's requirement.
Lemma 3.5. For every two vertices hq; li and hq reachable
from hq; li, then rank(q
Proof. Assume that rank(q; We distinguish between two cases. If i is
even, in which case hq; li is endangered in G i , then either hq 0 ; l 0 i is not in G i , in
which case, by Lemma 3.4, its rank is at most i 1, or hq 0 ; l 0 i is in G i , in which
case, being reachable from hq; li, it must be endangered in G i and have rank i. If
i is odd, in which case hq; li is safe in G i , then either hq 0 ; l 0 i is not in G i , in which
case, by Lemma 3.4, its rank is at most i 1, or hq 0 ; l 0 i is in G i , in which case, being
reachable from hq; li, it must by safe in G i and have rank i.
Lemma 3.6. In every innite path in G r , there exists a vertex hq; li with an odd
rank such that all the vertices in the path that are reachable from hq; li have
Proof. By Lemma 3.5, in every innite path in G r , there exists a vertex hq; li
such that all the vertices in the path that are reachable from hq; li have
We need to prove that the rank of hq; li is odd. Assume,
by way of contradiction, that the rank of hq; li is some even i. Thus, hq; li is
endangered in G i . Then, the rank of all the vertices in the path that are reachable
from hq; li is also i. By Lemma 3.4, they all belong to G i . Since the path is
innite, there are innitely many such vertices, contradicting the fact that hq; li is
endangered in G i .
We have seen that if a co-Buchi alternating automaton has an accepting run
on w, then it also has a very structured accepting run on w. In the next section
Kupferman and Moshe Y. Vardi
we employ this structured run in order to translate Buchi and co-Buchi alternating
automata to weak alternating automata. In [Loding and Thomas 2000], Loding and
Thomas use the structured runs in order to a priori dene runs of weak alternating
automata as dags of bounded width. This enables them to prove the appropriate
determinacy result directly. In [Piterman 2000], Piterman uses the structured runs
in order to extend linear temporal logic with alternating word automata.
The ranks dened in this section are closely related to the progress-measures
introduced in [Klarlund 1990] and to their properties studied in Section 3 there.
Progress measures are a generic concept for quantifying how each step of a program
contributes to bringing a computation closer to its specication. Progress measures
are used in [Klarlund 1991] for reasoning about automata on innite words. The
ranks dened above also measure progress: they indicate how far the automaton
is from satisfying its co-Buchi acceptance condition. When we use these ranks, we
consider, unlike [Klarlund 1991], alternating automata. Consequently, we do not
need to follow a subset construction and to consider several ranks simultaneously.
Thus, much of the complication in [Klarlund 1991] is handled by the rich structure
of the automata. In Section 5 we will get back to this point and see that once
alternation is removed, the two approaches essentially coincide.
4. FROM B
UCHI AND CO-B
UCHI TO WEAK ALTERNATING
In this section we present a translation of Buchi and co-Buchi alternating automata
to weak alternating automata. We rst describe a quadratic construction and then
suggest a pre-processing that reduces the blow-up in the average case.
4.1 The construction
Theorem 4.1. Let A be an alternating co-Buchi automaton. There is a weak
alternating automaton A 0 such that and the number of states in A 0
is quadratic in that of A.
Proof. Let
where
Intuitively, when the automaton is in state hq; ii as it reads
the letter  l (the l'th letter in the input), then it guesses that in a memoryless
accepting run of A on w, the rank of hq; li is i. An exception is the initial state
in explained below.
That is, q in is paired with 2n, which is an upper bound on the
rank of hq in ; 0i.
by means of a function
release
Given a formula  (Q), and a rank i 2 [2n], the formula release(; i) is
obtained from  by replacing an atom q by the disjunction
example,
Weak Alternating Automata Are Not That Weak  121
for a state hq; ii 2 Q 0 and  2 , as
follows.
or i is even.
false If q 2  and i is odd.
That is, if the current guessed rank is i then, by employing release , the run can
move in its successors to any rank that is smaller than i. If, however, q
and the current guessed rank is odd, then, by the denition of ranks, the current
guessed rank is wrong, and the run is rejecting.
That is, innitely many guessed ranks along each path should
be odd.
We rst show that A 0 is weak. For that, we dene a partition of the states of
A 0 and an order on this partition so that the weakness conditions hold. Each rank
induces the set Q in the partition. Thus, two states hq; ii and
are in the same set i dene the order  by Q
It is easy to see that the weakness conditions hold: for every state hq; ii 2 Q 0 and
the states appearing in - 0 (hq; ii; ) belongs to sets Q and every set
contained in  or disjoint from . By the denition of  0 , it follows
that the copies of A 0 are allowed to get trapped in sets with odd ranks and are not
allowed to get trapped in sets with even ranks.
We now prove the correctness of the construction. We rst prove that
L(A). Consider a word w accepted by A 0 . Let hT r ; r 0 i be the accepting run of A 0
on w. Consider the Q-labeled tree hT r ; ri where for all x
we have ri projects the labels of hT r ; r 0 i on their Q element.
It is easy to see that hT r ; ri is a run of A on w. Indeed, the transitions of A 0 only
annotate transitions of A by ranks. We show that hT r ; ri is an accepting run. Since
by the denition of  0 , each innite path of hT r ; r 0 i gets
trapped in a set Q fig for some odd i. By the denition of - 0 , no accepting run
can visit a state hq; ii with an odd i and q 2 . Hence, the innite path actually
gets trapped in the subset (Q n )  fig of Q fig. Consequently, in hT r ; ri, all the
paths visits states in  only nitely often, and we are done.
It is left to prove that L(A)  Consider a word w accepted by A. Let
ri be the accepting run of A on w. Consider the Q 0 -labeled tree hT r ; r 0 i where
is the rank of hr(x); jxji in G r . We claim that hT r ; ri is an accepting run of
A 0 . We rst prove that it is a run. Since in and q 0
2ni, the
root of the tree hT r ; r 0 i is labeled legally. We now consider the other nodes of
be the set of labels of "'s successors in hT r ; ri. As
2n is the maximal rank that a vertex can get, each successor c of " in T r has
2n. Therefore, the set S
Hence, the rst level of hT r ; r 0 i is also labeled legally. For
the other levels, consider a node x 2 T r such that x 6= " and rank(r(x);
be the set of labels of x's successors in hT r ; ri. By Lemma 3.5,
each successor x  c of x in T r has rank(r(x  c); jx  cj)  i. Also, by the definition
of ranks, it cannot be that r(x) 2  and i is odd. Therefore, the set
Hence, the tree hT r ; r 0 i is a run of A 0 on w. Finally, by Lemma 3.6, each innite
122  Orna Kupferman and Moshe Y. Vardi
path of hT r ; r 0 i gets trapped in a set with an odd index, thus hT r ; r 0 i is accepting.
Remark 4.2. As explained above, the automaton A 0 being at state hq; ii as it
reads the l'th letter in the input, corresponds to a guess that in a memoryless
accepting run of A on w, the rank of hq; li is i. Accordingly, the function release (and
the transition function - 0 that is based on it) enables the transition from a guessed
rank i to any rank that is smaller than i. As a result, while the number of states
in A 0 is O(n 2 ), a transition - 0 (hq; ii; ) may be n times longer than the transition
leading to - 0 that is O(n 2 ) times larger than -. Nevertheless, since for all
is a subformula of
the formula release(; i), the blow-up described above is not present if we maintain
- 0 as a dag, so that subformulas that are shared by several transitions are not
duplicated. Another way to keep - 0 only O(n) times larger than - is to redene
release(; i) to replace an atom q by the disjunction (q; i) _ (q; i 1) _ (q; i 2).
Thus, instead of a transition to any rank smaller than i, a transition is enabled
only to ranks i, i 1 and i 2. Then, the automaton A 0 being at state hq; ii as
it reads the l'th letter in the input, corresponds to a guess that in a memoryless
accepting run of A on w, the rank of hq; li is at most i. Since we can simulate one
big decrease in the guessed rank by several small decreases (in particular, having
in the transition enables us to \jump over" odd ranks), the correctness proof
given above can easily be adjusted to the new denition of release.
As discussed in [Muller and Schupp 1987], one can complement an alternating
automaton by dualizing its transition function and acceptance condition. Formally,
given a transition function -, let ~
- denote the dual function of -. That is, for every q
and  with -(q;
, where ~  is obtained from  by switching
_ and ^ and by switching true and false. If, for example,
then ~ The dual of an acceptance condition  is a condition
that accepts exactly all the words in Q ! that are not accepted by . In particular,
we have the following.
Theorem 4.3. [Muller and Schupp 1987] For an alternating Buchi automaton
the alternating co-Buchi automaton ~
ises L( ~
The complementation construction in Theorem 4.3 is not only conceptually sim-
ple, but it also involves no blow-up. In addition, complementing a WAA does not
sacrice its weakness. Hence, Theorems 4.1 and 4.3 imply the following theorem.
Theorem 4.4. Let A be an alternating Buchi automaton. There is a weak alternating
automaton A 0 such that and the number of states in A 0 is
quadratic in that of A.
In Section 5, we use the translation described in Theorem 4.1 in order to obtain
a simple complementation construction for nondeterministic Buchi automata. As
we shall note there, the known lower bound on the complexity of the latter then
implies that the quadratic blow-up involved in moving from co-Buchi alternating
automata to WAA cannot be reduced to a linear one.
Weak Alternating Automata Are Not That Weak  123
4.2 Improving the construction
A drawback of our construction is that it never performs better than its worst-case
complexity. Indeed, the quadratic blow-up is introduced in the translation of A
to A 0 regardless of the structure of A and would occur even if, say, A is a weak
automaton. In order to circumvent such an unnecessary blow up, we suggest to
rst calculate the minimal rank required for A (formally dened below), and then
to construct A 0 with respect to this rank. The discussion below assumes that A
is a co-Buchi automaton, yet applies also for the dual case, where A is a Buchi
automaton.
Consider the sequence of dags G . With every G i , we can associate
a maximal width, namely the maximal number of vertices of the form hq; li,
for some xed l, in G i . Following Lemma 3.2, the maximal width of G 2i is n i.
In practice, the transition from G 2i to G 2i+2 often reduces the width by more than
one vertex. We say that is required for A i there exists a word w 2 L(A)
such that for every memoryless run hT r ; ri of A on w, the sequence G
dags with G is such that the width of G 2j is bigger than 0. Note that this
implies that G 2j+1 is not empty.
Let A
i. For every j 2 [n], we dene the weak alternating
automaton A 0
j as follows. Intuitively, A 0
restricts the runs of A 0 to guess only
ranks smaller than 2j. Formally, the state space of A 0
j is Q [2j], its initial state is
hq in ; 2ji, and its transition function and acceptance condition are the restrictions
of - 0 and  0 to the states in Q [2j]. It is easy to see that for every j, the language
of A 0
j is contained in the language of A 0 . On the other hand, the language of A 0
contains only these words in is empty. It follows that the
minimal rank required for A is the minimal j 2 [n] for which L(A)
Theorem 4.5. Let A be an alternating co-Buchi automaton. The problem of
nding the minimal rank required for A is PSPACE-complete.
Proof. Recall that the minimal rank required for A is the minimal j 2 [n]
for which L(A)
the language-containment problem for alternating
co-Buchi automata is in PSPACE, we can nd the minimal rank in polynomial
space by successive language-containment checks. For the lower bound, we do a
reduction from the emptiness problem for alternating co-Buchi automata, whose
PSPACE-hardness follows from the results in [Chandra et al. 1981]. Given an
alternating co-Buchi automaton we prove that A is empty i
the minimal rank required for A is 0. For technical convenience, we assume that
no formula  in the range of - is a tautology (since we can replace a transition to
a  that is a tautology by a transition to an accepting sink, the emptiness problem
is clearly PSPACE-hard already for automata satisfying this assumption). Assume
rst that A is empty. Then, L(A)
[n], and in particular for
For the other direction, note that the set of states in A 0
0 is Q f0g, and its
transitions coincide with these of A. Also, since 0 is even, the accepting set of A 0
0 is
empty. Hence, as no formula in - 0 is a tautology, A 0
accepts no word. Accordingly,
A is empty.
Since for all i 2 [2n] we have that
the automaton A 0
the minimal rank required for A, is equivalent to A. Hence the following theorem.
124  Orna Kupferman and Moshe Y. Vardi
Theorem 4.6. Let A be an alternating co-Buchi automaton with n states and
let j be the minimal rank required for A. There is a weak alternating automaton
A 0 such that and the number of states in A 0 is 2nj.
We note that while the problem of nding the minimal rank required for A
requires space that is polynomial in A, the automaton A is typically small, and
the bottle-neck of the computation is usually the application of A 0 (e.g., taking its
product with a system with a large state space). Thus, nding the minimal rank j
required for A and using A 0
j instead of A 0 may be of great practical importance.
5. COMPLEMENTING NONDETERMINISTIC B
UCHI
In this section we apply our results in order to complement nondeterministic Buchi
automata. We rst describe, in Section 5.1, a construction that uses alternating
automata. We then describe, in Section 5.2, a construction that uses the analysis
in Section 3 without explicitly using alternating automata.
5.1 Complementation via alternating automata
Unlike the case with alternating automata, complementation of nondeterministic
automata is a complicated problem. Following Theorem 4.3, all one needs in order
to complement a nondeterministic Buchi automaton is some translation of universal
co-Buchi automata to nondeterministic Buchi automata. In [Miyano and Hayashi
1984], Miyano and Hayashi suggest a translation of alternating Buchi automata
to nondeterministic Buchi automata. We present (a simplied version of) their
translation in Theorem 5.1 below.
Theorem 5.1. [Miyano and Hayashi 1984] Let A be an alternating Buchi au-
tomaton. There is a nondeterministic Buchi automaton A 0 , with exponentially
many states, such that
Proof. The automaton A 0 guesses a run of A. At a given point of a run of A 0 ,
it keeps in its memory a whole level of the run tree of A. As it reads the next input
letter, it guesses the next level of the run tree of A. In order to make sure that every
innite path visits states in  innitely often, A 0 keeps track of states that \owe" a
visit to . Let
|If O 6= ;, then
q2S
q2O
q2S
The translation in Theorem 5.1, however, does not handle alternating (and in
particular universal) co-Buchi automata, which is what one gets by dualizing a
nondeterministic Buchi automaton. Here is where our construction in Theorem 4.1
Weak Alternating Automata Are Not That Weak  125
becomes essential. Thus, given nondeterministic Buchi automaton B, we suggest
the following complementation construction for B.
(1) Following Theorem 4.3, construct from B its dual co-Buchi universal automaton
~
B. The automaton ~
(2) Following Theorem 4.1, construct from ~
its equivalent weak alternating automaton
W . The automaton W satises
(3) Following Theorem 5.1, construct from W its equivalent nondeterministic Buchi
automaton N . The automaton N satises L(N
If B has n states, then ~
B has n states as well, W has O(n 2 ) states, and N has
states. By [Michel 1988; Safra 1988], however, an optimal complementation
construction for nondeterministic Buchi automata results in an automaton N with
O(n log n) states. Before we describe how we do get, using Theorem 4.1, such an
optimal automaton N , let us note that the above scheme implies that the translation
described in Theorem 4.1 cannot be improved to a linear translation. Indeed, being
able to construct from ~
B to an equivalent WAA W with only O(n) states, we are
also able to construct N with 2 O(n) states, contradicting the 2 O(n log n) lower bound.
In order to get N with 2 O(n log n) states, we exploit the special structure of W as
follows. Consider a state hS; Oi of N . Each of the sets S
and O is a subset of Q [2n]. We say that P  Q [2n] is consistent i for every
two states hq; ii and hq We claim the following.
Claim 1. Restricting the states in N to pairs hS; Oi for which S is a consistent
subset of Q [2n] is allowable; that is, the resulting N still complements B.
2. There are 2 O(n log n) consistent subsets of Q [2n].
By the two claims, as O is always a subset of S, it is easy to restrict the state space
of N to 2 O(n log n) states. In order to prove Claim 1, recall that the automaton W
visiting a state hq; ii after reading l letters of an input word w corresponds to a
guess that the rank of hq; li in an accepting and memoryless run of ~
on w is i. We
have seen that if there is an accepting and memoryless run hT r ; ri of ~
B on w, then
a run of W that follows the ranks in G r is accepting. Since every vertex in G r has
a unique rank, the copies of W that are created in each level l in this accepting run
are consistent, in the sense that the set of states visited by copies of W in level l in
the run is consistent. In N , all the states in S correspond to copies of W that read
the same prex of w. Hence, a state hS; Oi for which S is inconsistent corresponds
to a level l in a run of W whose copies are inconsistent. Hence, the automaton N
can ignore states hS; Oi with inconsistent S.
In order to prove Claim 2, observe that we can characterize a consistent set by
the projection of its pairs on Q, augmented by an assignment f
there are 2 n such projections and n log n) such assignments, we are done.
Composing the three constructions is straightforward. Below we dene the automaton
N directly, by means of B's components. Given a nondeterministic Buchi
automaton
such that n. For a set P 2 2 Q[2n] , we say that P is
possible there exists no pair hq; ii in P such that i is odd and q 2 . For two sets
P and P 0 in 2 Q[2n] and a letter  2 , we say that
126  Orna Kupferman and Moshe Y. Vardi
such that the pair hq
in P 0 .
The automaton A
O  S, and S is possible and consistent g.
|For a state hS; Oi 2 Q 0 and a letter  2 , we dene - 0
- If O 6= ;, then
O 0 covers hO; i; and S 0 is possible and consistent g:
and S 0 is possible and consistent g:
is possible and consistentg.
As discussed in Section 4.2, we advise to construct the automaton W according to
the minimal rank j required for ~
B. Then, each state of N corresponds to a consistent
set augmented by an assignment f Accordingly, the automaton N has
only 2 O(n+j log n) states.
5.2 Complementation without alternating automata
In this section we give an alternative description of our complementation construc-
tion, which is independent of alternating automata. The ideas behind the construction
are these used in Section 4 for the transformation of alternating co-Buchi
automata to weak alternating automata. We repeat these ideas here for the ben-
et of readers who'd like to see a complementation construction that does not go
through alternating automata. 2 The construction that follows essentially coincides
with the one described in [Klarlund 1991].
be a nondeterministic Buchi automaton with
and let be a word in  ! . We dene an innite dag G that embodies
all the possible runs of A on w. Formally,
IN is the union
in g and Q
-(q;  l ).
l0 (Q l flg)(Q l+1 fl+1g) is such that E(hq; li; hq
We refer to G as the run dag of A on w. We say that a vertex hq
successor of a vertex hq; li i E(hq; li; hq We say that is reachable from
li i there exists a sequence hq successive vertices such
that hq; li Finally, we
say that a vertex hq; li is an -vertex i q 2 . It is easy to see that A accepts w
i G has a path with innitely many -vertices. Indeed, such a path corresponds
to an accepting run of A on w.
We have found it easier to teach the direct construction. (See
http://www.cs.rice.edu/vardi/av.html.)
Weak Alternating Automata Are Not That Weak  127
A ranking for G is a function that satises the following two
conditions:
(1) For all vertices hq; li 2 V , if f(hq; li) is odd, then q 62 .
(2) For all edges hhq; li; hq li).
Thus, a ranking associates with each vertex in G a rank in [2n] so that the ranks
along paths decreased monotonically, and -vertices get only even ranks. Note
that each path in G eventually gets trapped in some rank. We say that the ranking
f is an odd ranking if all the paths of G eventually get trapped in an odd rank.
Formally, f is odd i for all paths hq G, there is j  0 such
that f(hq j ; ji) is odd, and for all i  1, we have f(hq j+i
Lemma 5.2. A rejects w i there is an odd ranking for G.
Proof. We rst claim that if there is an odd ranking for G, then A rejects w.
To see this, recall that in an odd ranking, every path in G eventually gets trapped
in an odd rank. Hence, as -vertices get only even ranks, it follows that all the
paths of G, and thus all the possible runs of A on w, visit  only nitely often.
Assume now that A rejects w. We describe an odd ranking for G. As in Section 3,
we say that a vertex hq; li is endangered in a (possibly nite) dag G 0  G i only
nitely many vertices in G 0 are reachable from hq; li. The vertex hq; li is safe in
all the vertices in G 0 that are reachable from hq; li are not -vertices. Note
that, in particular, a safe vertex is not an -vertex. We dene an innite sequence
dags inductively as follows.
G.
li j hq; li is endangered in G 2i g.
li j hq; li is safe in G 2i+1 g.
Consider the function
2i If hq; li is endangered in G 2i .
li is safe in G 2i+1 .
Recall that A rejects w. Thus, each path in G has only nitely many -vertices.
Therefore, the same arguments used in the proof of Lemma 3.2 can be used here
in order to show that G 2n is nite and G 2n+1 is empty, implying that f above
maps the vertices in V to [2n]. We claim further that f is an odd ranking. First,
since a safe vertex cannot be an -vertex and f(hq; li) is odd only for safe hq; li,
the rst condition for f being a ranking holds. Second, as in Lemma 3.5, for
every two vertices hq; li and hq is reachable from hq; li, then
li). In particular, this holds for that is a successor of hq; li.
Hence, the second condition for ranking holds too. Finally, as in Lemma 3.6, for
every innite path in G, there exists a vertex hq; li with an odd rank such that all the
vertices in the path that are reachable from hq; li have f(hq li).
Hence, f is an odd ranking.
By Lemma 5.2, an automaton A 0 that complements A can proceed on an input
word w by guessing an odd ranking for the run dag of A on w. We now dene
such an automaton A 0 formally. We rst need some denitions and notations.
128  Orna Kupferman and Moshe Y. Vardi
A level ranking for A and w is a function such that if g(q)
is odd, then q 62 . Let R be the set of all level rankings. For two level rankings g
and g 0 , we say that covers g if for all q and q 0 in Q, if g(q)  0 and q 0 2 -(q; ),
then
We dene A
in (q in in in . Thus, the odd
ranking that A 0 guesses maps the root hq in ; 0i of the run dag to 2n.
|For a state hg; P i
covers g, and
there is
covers
Thus, when A 0 reads the l'th letter in the input, for l  1, it guesses the level
ranking for level l in the run dag. This level ranking should cover the level
ranking of level l 1. In addition, in the P component, A 0 keeps track of states
whose corresponding vertices in the dag have even ranks. Paths that traverse
such vertices should eventually reach a vertex with an odd rank. When all the
paths of the dag have visited a vertex with an odd rank, the set P becomes
empty, and is initiated by new obligations for visits in odd ranks according to
the current level ranking. The acceptance condition R  f;g then checks that
there are innitely many levels in which all the obligations have been fullled.
Note that the automaton A 0 here is equivalent to the one described in Section 5.
Indeed, each state hg; P i 2 R  2 Q in A 0 above corresponds to the state hS; Oi 2
?g. Clearly, S and O and possible and consistent, and O  S.
Similarly, since the sets S and O in the state space of A 0 of Section 5 are possible
and consistent, each state hS; Oi there induces a level ranking and thus corresponds
to a state here.
6. DISCUSSION
We described a quadratic translation of Buchi and co-Buchi alternating automata
to weak alternating automata and showed how our translation yields a simple complementation
algorithm for nondeterministic Buchi automata. Another application
of our translation is the solution of the nonemptiness problem. It is shown in
[Kupferman et al. 2000] that the nonemptiness problem for nondeterministic tree
automata and the nonemptiness problem for alternating word automata over a singleton
alphabet are equivalent and that their complexities coincide. We refer to
both problems as the nonemptiness problem. Recall that the nonemptiness problem
for weak automata can be solved in linear time [Kupferman et al. 2000]. On the
other hand, the best known upper bound for the nonemptiness problem for Buchi
and co-Buchi automata is quadratic time. Using our translation, one can solve the
nonemptiness problem for a Buchi or a co-Buchi automaton A by rst translating
Weak Alternating Automata Are Not That Weak  129
it to a weak automaton A 0 . The size of A 0 is O(nj), where j is the minimal rank
required for A, yielding a nonemptiness algorithm of the same complexity.
In [Kupferman and Vardi 1998b], we extend the ideas of this paper and describe
an e-cient translation of stronger types of alternating automata to weak alternating
automata. This enables us to improve known upper bounds for the nonemptiness
problem. Given an alternating parity automaton [Mostowski 1984; Emerson and
Jutla 1991] with n states and k sets, we construct an equivalent weak alternating
automaton with O(n k ) states. Given an alternating Rabin automaton [Rabin 1969]
with n states and k pairs, we construct an equivalent weak alternating automaton
with O(n 2k+1  k!) states. Our constructions yield O(n k ) and O(n 2k+1  k!) upper
bounds for the nonemptiness problem for parity and Rabin automata, respectively,
matching the known bound for parity automata [Emerson et al. 1993] and improving
the known O(nk) 3k bound for Rabin automata [Emerson and Jutla 1988; Pnueli
and Rosner 1989].
Recall that while weak alternating word automata are not less expressive than
Buchi alternating word automata, weak alternating tree automata are strictly less
expressive than Buchi alternating tree automata. Precisely, when dened on trees,
a language L can be recognized by a weak alternating automaton i both L and its
complement can be recognized by Buchi nondeterministic automata. This result
follows from expressiveness results in second order logic [Rabin 1970], and the
equivalence of weak alternating tree automata and weak second-order logic [Rabin
1970]. In [Kupferman and Vardi 1999], we extend the ideas in this paper to handle
tree automata. Given two nondeterministic Buchi tree automata U and U 0 that
recognize a language and its complement, we construct a weak alternating tree
automaton A equivalent to U . The number of states in A is quadratic in the number
of states of U and U 0 . Precisely, if U and U 0 has n and m states, respectively, the
automaton A has (nm) 2 states. The known linear translation of weak alternating
tree automata to formulas in the alternation-free fragment of -calculus [Kupferman
and Vardi 1998a] then implies a quadratic translation of Buchi automata as above to
alternation-free -calculus, extending the scope of e-cient symbolic model checking
to highly expressive specication formalisms.

Acknowledgment

We thank Nils Klarlund for clarifying the relation between
[Klarlund 1991] and this work, and Wolfgang Thomas for helpful discussions.



--R

Finite automata and sequential networks.




On the power of bounded concurrency I: Finite automata.
Journal of the ACM
The complexity of tree automata and logics of programs.
On model-checking for fragments of -calculus
Design and Validation of Computer Protocols.
Progress measures and
Progress measures for complementation of

Weak alternating automata and tree automata emptiness.

The weakness of self-complementation

An automata-theoretic approach to branching-time model checking
Computer Aided Veri
Decision problems for
On alternating

Testing and generating in
Complementation is more di-cult with automata on in nite words

Regular expressions for in

Alternating automata
Alternating automata on in
Extending temporal logic with
On the synthesis of a reactive module.
Decidability of second order theories and automata on in
Weakly de
On the complexity of
Language containment using non-deterministic omega-automata

Automata on in
An automata-theoretic approach to linear temporal logic
An automata-theoretic approach to automatic program veri- cation
Reasoning about in
Received: June
--TR
Alternation and MYAMPERSANDohgr;-type Turing acceptors
Alternating automata, the weak monadic theory of the tree, and its complexity
The complementation problem for BuMYAMPERSANDuml;chi automata with applications to temporal logic
Alternating automata on infinite trees
On the synthesis of a reactive module
Design and validation of computer protocols
Automata on infinite objects
Progress measures for complementation of MYAMPERSANDohgr;-automata with applications to temporal logic
Tree automata, Mu-Calculus and determinacy
A unified approach for showing language inclusion and equivalence between various types of MYAMPERSANDohgr;-automata
On the power of bounded concurrency I
Reasoning about infinite computations
Computer-aided verification of coordinating processes
An automata-theoretic approach to linear temporal logic
Weak alternating automata and tree automata emptiness
Alternation
An automata-theoretic approach to branching-time model checking
Language containment of non-deterministic omega-automata
Alternating Automata and Logics over Infinite Words
On Model-Checking for Fragments of MYAMPERSAND#181;-Calculus
Freedom, Weakness, and Determinism
Progress measures and finite arguments for infinite computations

--CTR
A. Fellah , S. Noureddine, Some succinctness properties of -DTAFA, Proceedings of the 5th WSEAS International Conference on Software Engineering, Parallel and Distributed Systems, p.97-103, February 15-17, 2006, Madrid, Spain
Orna Kupferman , Moshe Y. Vardi, From complementation to certification, Theoretical Computer Science, v.345 n.1, p.83-100, 21 November 2005
Orna Kupferman , Moshe Y. Vardi, From linear time to branching time, ACM Transactions on Computational Logic (TOCL), v.6 n.2, p.273-294, April 2005
Erich Grdel , Wolfgang Thomas , Thomas Wilke, Literature, Automata logics, and infinite games: a guide to current research, Springer-Verlag New York, Inc., New York, NY, 2002
weak alternating automata;complementation