Internal Report  TCS-96-2

August, 1996

Finite-state Automata on Infinite Inputs^{1}

Madhavan Mukund SPIC Mathematical Institute 92 G N Chetty Rd, Madras 600 017, India E-mail: madhavan@ssf.ernet.in

Abstract

This paper is a self-contained introduction to the theory of finite-state automata on infinite words. The study of automata on infinite inputs was initiated by Büchi in order to settle certain decision problems arising in logic. Subsequently, there has been a lot of fundamental work in this area, resulting in a rich and elegant mathematical theory. In recent years, there has been renewed interest in these automata because of the fundamental role they play in the automatic verification of finite-state systems.

1Tutorial talk, Sixth National Seminar on Theoretical Computer Science, Banasthali Vidyapith, Banasthali, Rajasthan, August 1996

Introduction

Büchi initiated the study of finite-state automata working on infinite inputs in [Bü60]. He was interested in showing that the monadic second order logic of infinite sequences (S1S) was decidable. Büchi discovered a deep and elegant connection between sets of models of formulas in this logic and ω-regular languages, the class of languages over infinite words accepted by finite-state automata.

A few years later, Muller independently proposed an alternative definition of finitestate automata on infinite inputs [Mu63]. His work was motivated by questions in switching theory.

The theory of ω-regular languages and automata on infinite words is substantially more complex than the corresponding theory for finite words. This was evident from Büchi’s initial work, where he showed that non-deterministic automata over infinite inputs are strictly more powerful than deterministic automata. This means that basic constructions like complementation are correspondingly more intricate for this class of automata.

During the 1960’s, fundamental contributions were made to this area. McNaughton proved that with Muller’s definition, deterministic automata suffice for recognizing all ω-regular languages [Mc66]. Later, Rabin extended Büchi’s decidability result for S1S to the monadic second order of the infinite binary tree (S2S) [Ra69]. The logical theory S2S is extremely expressive and Rabin’s theorem can be used to settle a number of decision problems in logic.

Despite this strong connection between automata on infinite inputs and the decidability of logical theories, there was a lull in the area during the 1970’s. One reason for this was Meyer’s negative result about the complexity of the automata-theoretic decision procedure for S1S and S2S [Me75]—he showed that, in the worst case, the automata that one constructs would be hopelessly large and impossible to use in practice.

During the past decade or so, however, there has been renewed interest in applying automata on infinite words to solve problems in logic. To a large extent, this is a consequence of the development of temporal logic as a formalism for specifying and verifying properties of programs [Em90, Pn77]. It turns out that automata on infinite words (and trees) can be directly applied to settle important questions in temporal logic, without invoking S1S and S2S. In conjunction with these new applications, there has been greater emphasis on evaluating the complexity of different constructions on these automata [Sa88, SV89, SVW87, VW94].

In this tutorial, we present a self-contained introduction to the theory of finite-state automata on infinite words. We begin with some preliminaries on the notation we will use in the paper. In Section 1, we introduce Büchi automata and ω-regular languages and prove some basic results. The next section describes in detail the connection between ω-regular languages and formulas of S1S. In Section 3, we look at stronger definitions of automata, proposed by Muller, Rabin and Streett. The last technical section, Section 4, describes in detail a determinization construction for Büchi automata. We conclude with a quick summary of various aspects of the theory which could not discussed in the paper.

For a more detailed introduction to the area, the reader is encouraged to consult the excellent survey by Thomas [Th90]. This tutorial—especially Sections 1 and 2—draws heavily on the material presented in [Th90].

Notation

Throughout this paper, Σ denotes a finite set of symbols called an alphabet. A word is a sequence of symbols from Σ. The set Σ^{∗} denotes the set of finite words over Σ while the set Σ^{ω} is the set of infinite words over Σ. A language is a set of words. Every language we consider either consists exclusively of finite words or exclusively of infinite words.

Typically, elements of Σ will be denoted a, b, c, …, finite words will be denoted u, v, w, …, and infinite words will be denoted α, β, …. We use U, V, … to denote languages of finite words—that is, subsets of Σ^{∗}. L will be reserved for languages consisting exclusively of infinite words.

An infinite word α ∈ Σ^{ω} is an infinite sequence of symbols from Σ. We shall represent α as a function α : ℕ_{0} → Σ, where ℕ_{0} is the set {0, 1, 2, …} of natural numbers. Thus, α(i) denotes the letter occurring at the i^{th} position. For natural numbers m and n, m ≤ n, α[m..n] denotes the finite word α(m)α(m+1) ⋯ α(n−1)α(n) occurring between positions m and n.

In general, if S is a set and σ an infinite sequence of symbols over S—in other words, σ : ℕ_{0} → S—then inf(σ) denotes the set of symbols from S which occur infinitely often in σ. Formally, inf(σ) = {s ∈ S | ∃^{ω}n ∈ ℕ_{0} : σ(n) = s}, where ∃^{ω} denotes the quantifier “there exist infinitely many”.

We shall assume some degree of familiarity with standard results from the theory of regular languages over finite words.

1 Büchi automata

A Büchi automaton is a non-deterministic finite-state automaton which takes infinite words as input. A word is accepted if the automaton goes through some designated “good” states infinitely often while reading it.

Automata An automaton is a triple A = (S, →, S_{in}) where S is a set of states, S_{in} ⊆ S is a set of initial states and → ⊆ S × Σ × S is a transition relation. Normally, we write s ⟶^{a} s′ to denote that (s, a, s′) ∈ →.

The automaton is said to be deterministic if S_{in} is a singleton and → is a function from S × Σ to S.

We could have weakened the condition for deterministic automata by permitting → to be a partial function from S × Σ to S. The present definition demands that at each state there is precisely one outgoing transition for each letter of the input alphabet. The weaker definition would relax this to say that there is at most one outgoing transition per letter. A “weak” deterministic automaton can always be converted to a “strong” deterministic automaton by adding a “dump” or “reject” state to take care of all missing transitions. Since it is often convenient to assume that deterministic automata are “complete” and never get stuck when reading their input, we shall stick to the stronger definition in this paper.

If u is a finite non-empty word, we write s ⟶^{u}^{+} s′ to denote the fact that there is a sequence of transitions labelled by u leading from s to s′. In other words, if u = a_{1}a_{2} ⋯ a_{m},

then s ⟶^{u}^{+} s′ if there exist states s_{0}, s_{1}, …, s_{m} such that s = s_{0} ⟶^{a_{1}} s_{1} ⟶^{a_{2}} ⋯ ⟶^{a_{m}} s_{m} =

s′.

[figure: s; g]

Figure 1: A typical accepting run of a Büchi automaton, with s ∈ S_{in} and g ∈ G.

Runs Let A = (S, →, S_{in}) be an automaton and α : ℕ_{0} → Σ an input word. A run of A on α is a infinite sequence ρ : ℕ_{0} → S such that ρ(0) ∈ S_{in} and for all i ∈ ℕ_{0},

ρ(i) ⟶^{α(i)} ρ(i+1).

A run of A on the finite word w = a_{0}a_{1} … a_{m} is a sequence of states s_{0}s_{1} … s_{m+1} such

that s_{0} ∈ S_{in} and for all i ∈ {0, 1, …, m}, s_{1} ⟶^{α(i)} s_{i+1}.

So, a run is just a “legal” sequence of states that an automaton can pass through while reading the input. In general, an input may admit many runs because of nondeterminism. Since a non-deterministic automaton may have states where there are no outgoing transitions corresponding to certain input letters, it is also possible that an input admits no runs—in this case, every potential run leads to a state from where there is no outgoing transition enabled for the next input letter. If the automaton is deterministic, each input admits precisely one run.

Automata on finite words A finite state automaton on finite words is a structure (A, F) with A = (S, →, S_{in}) and F ⊆ S. The automaton A accepts an input w = a_{0}a_{1} … a_{m} if w admits a run s_{0}s_{1} … s_{m+1} such that s_{m+1} ∈ F. The language recognized by (A, F), L(A, F), is the set of all finite words accepted by (A, F).

Throughout this paper, we shall refer to languages recognized by finite state automata on finite words as regular languages. In other words, a set U ⊆ Σ^{∗} is regular iff there is an automaton (A, F) such that U = L(A, F).

Our goal is to study automata which recognize languages of infinite words. The first definition of such automata was proposed by Büchi [Bü60].

Büchi automata A Büchi automaton is a pair (A, G) where A = (S, →, S_{in}) and G ⊆ S. G denotes a set of good states. The automaton (A, G) accepts an input α : ℕ_{0} → Σ if there is a run ρ of A on α such that inf(ρ) ∩ G ≠ ∅. The language recognized by (A, G), L(A, G), is the set of all infinite words accepted by (A, G). A set L ⊆ Σ^{ω} is said to be Büchi-recognizable if there is a Büchi automaton (A, G) such that L = L(A, G).

According to the definition, a Büchi automaton accepts an input if there is a run along which some subset of G occurs infinitely often. Since G is a finite set, it is easy to see that there must actually be a state g ∈ G which occurs infinitely often along σ. In other words, if we regard the state space of a Büchi automaton as a graph, an accepting run traces an infinite path which starts at some state s in S_{in}, reaches a good state g ∈ G and, thereafter, keeps looping back to g infinitely often (see Figure 1).

[figure: a; b; b; a; s_{1}; s_{2}; ⟹]

Figure 2: A Büchi automaton for L (Example 1.1)

[figure: b; s_{1}; s_{2}; ⟹; a, b; b]

Figure 3: A Büchi automaton for \overline{L} (Example 1.1)

Example 1.1 Consider the alphabet Σ = {a, b}. Let L ⊆ Σ^{ω} consist of all infinite words α such that there are infinitely many occurrences of a in α. Figure 2 shows a Büchi automaton recognizing L. The initial state is marked by a double arrow. There is only one good state, which is indicated with a double circle. In this automaton, all transitions labelled a lead into the good state and, conversely, all transitions coming into the good state are labelled a. From this, it follows that the automaton accepts an infinite word iff it has infinitely many occurrences of a.

The complement of L, which we denote \overline{L}, is the set of all infinite words α such that α has only finitely many occurrences of a. An automaton recognizing \overline{L} is shown in Figure 3. The automaton guesses a point in the input beyond which it will see no more a’s—such a point must exist in any input with only a finite number of a’s. Once it has made this guess, it can process only b’s—there is no transition labelled a from the second state—so if it reads any more a’s it gets stuck.

□

In the example, notice that the automaton recognizing L is deterministic while the automaton for \overline{L} is non-deterministic. We now show that the non-determinism in the second case is unavoidable—that is, there is no deterministic automaton recognizing \overline{L}. This means that Büchi automata are fundamentally different from their counterparts on finite inputs: we know that over finite words, deterministic automata are as powerful as non-deterministic automata.

Limit languages Let U ⊆ Σ^{∗} be a language of finite strings. The limit of U, lim(U) is the set

{α ∈ Σ^{ω} | ∃^{ω}n ∈ ℕ_{0} : α[0..n] ∈ U}.

So, a word belongs to lim(U) iff it has infinitely many prefixes in U. We then have the following characterization of languages recognized by deterministic Büchi automata.

Theorem 1.2 A language L ⊆ Σ^{ω} is recognizable by a deterministic Büchi automaton iff L is of the form lim(U) for some regular language U ⊆ Σ^{∗}.

Proof Let U be a regular language. Then, there exists a deterministic finite state automaton (DFA) of the form (A, F) where A = (S, →, S_{in}) and F ⊆ S such that (A, F) recognizes U. It is easy to see that if we interpret F as a set of good states, the Büchi automaton (A, F) accepts lim(U).

Conversely, let L be recognized by a deterministic Büchi automaton (A, G). Treat G as a set of final states and let U be the language recognized by the DFA (A, G). Once again, it is easy to see that L = lim(U). □

We now show that the language \overline{L} of Example 1.1 is not of the form lim(U) for any language U. Recall that \overline{L} is the set of all infinite words α over the alphabet Σ = \{a, b\} such that α contains only finitely many occurrences of a.

Suppose that \overline{L} = lim(U) for some U ⊆ Σ^{∗}. Since b^{ω} ∈ \overline{L}, there must be some finite prefix b^{n_{1}} ∈ U. Since, b^{n_{1}}ab^{ω} ∈ \overline{L}, we can then find a prefix b^{n_{1}}ab^{n_{2}} ∈ U. From the fact that b^{n_{1}}ab^{n_{2}}ab^{ω} ∈ \overline{L}, we obtain a prefix b^{n_{1}}ab^{n_{2}}ab^{n_{3}} ∈ U. Proceeding in this way, we get an infinite sequence of words {b^{n_{1}}, b^{n_{1}}ab^{n_{2}}, b^{n_{1}}ab^{n_{2}}ab^{n_{3}}, …} ⊆ U. From this it follows that the infinite word β = b^{n_{1}}ab^{n_{2}}ab^{n_{3}}a ⋯ ab^{n_{i}}a ⋯ belongs to lim(U). But β has infinitely many occurrences of a, so it certainly does not belong to \overline{L}, thus contradicting the assumption that \overline{L} = lim(U).

From this observation and Example 1.1, we deduce the following corollary.

Corollary 1.3 Non-deterministic Büchi automata are strictly more powerful than deterministic Büchi automata—there are languages recognized by non-deterministic Büchi automata which cannot be recognized by any deterministic Büchi automaton.

1.1 Characterizing Büchi-recognizable languages

For finite words, we can characterize the class of languages recognized by non-deterministic finite state automata in a number of ways—for instance, in terms of regular expressions, or in terms of syntactic congruences. In the same spirit, we now describe a characterization of Büchi-recognizable languages of infinite words. We first need to define the ω-iteration of a set of finite words. Let U ⊆ Σ^{∗}. Then

U^{ω} = {α ∈ Σ^{ω} | α = u_{0}u_{1}u_{2} ⋯ where u_{i} ∈ U for all i ∈ ℕ_{0}}.

Also, we observe that if U is a language of finite words and L is a language of infinite words, we can define the language UL of infinite words obtained by concatenating each finite word in U with an infinite word from L. Formally, UL = {α | ∃u ∈ U : ∃β ∈ L : α = uβ}. ω-regular languages A language L ⊆ Σ^{ω} is said to be ω-regular if it is of the form ⋃_{i∈{1,2,...,n}} U_{i}V_{i}^{ω}, where each U_{i} and V_{i} is a regular language of finite words.^{2}

Theorem 1.4 A language is Büchi-recognizable iff it is ω-regular.

Proof (⇒): Let L be recognized by a Büchi automaton (A, G), where A = (S, →, S_{in}). We have observed earlier that each infinite word α ∈ L admits an accepting run ρ which begins in an initial state, reaches a good state g, and then loops back through g infinitely often. For s, s′ ∈ S, let V_{ss′} = {w ∈ Σ^{∗} | s ⟶^{w}^{+} s′} denote the set of finite words which can lead from s to s′. It is easy to see that V_{ss′} is regular—to recognize this set, use the non-deterministic automaton (S, →, {s}) with {s′} as the set of final states. From our observation about accepting runs, it follows that we can write L(A, G) as ⋃_{s∈S_{in}, g∈G} V_{sg}V_{gg}^{ω}.

(⇐): It is not difficult to show that the set of Büchi-recognizable languages satisfies the following closure properties:

(i) If U is regular, then U^{ω} is Büchi-recognizable.

(ii) If U is regular and L is Büchi-recognizable then UL is Büchi recognizable.

(iii) If L_{1}, L_{2}, …, L_{n} are Büchi-recognizable, so is ⋃_{i∈{1,2,...,n}} L_{i}.

From this, it follows that every language of the form ⋃_{i∈{1,2,...,n}} U_{i}V_{i}^{ω}, where each U_{i} and V_{i} is regular, is Büchi-recognizable. □

1.2 Constructions on Büchi automata

It turns out that the class of Büchi-recognizable languages is closed under boolean operations and projection. These operations will be crucially used when applying Büchi automata to settle decision problems in logic.

Union To show closure under finite union (which we have already assumed when proving the previous theorem!), let (A_{1}, G_{1}) and (A_{2}, G_{2}) be two Büchi automata. To construct an automaton (A, G) such that L(A, G) = L(A_{1}, G_{1}) ∪ L(A_{2}, G_{2}), we take A to be the disjoint union of A_{1} and A_{2}. Since we are permitted to have a set of initial states in A, we retain the initial states from both copies. If a run of A starts in an initial state contributed by A_{1}, it will never cross over into the state space contributed by A_{2} and vice versa. Thus, we can set the good states of A to be the union of the good states contributed by both components.

2Technically speaking, both regularity and ω-regularity are defined algebraically, in terms of homomorphisms from the given language to a finite monoid. However, we shall ignore this complication and stick to a more simple definition of ω-regularity.

Complementation Showing that Büchi-recognizable languages are closed under complementation is highly non-trivial. One problem is that we cannot determinize Büchi automata, as we have observed in Corollary 1.3. Even if we could work with deterministic automata, the formulation of Büchi acceptance is not symmetric with respect to complementation in the following sense. Suppose (A, G) is a deterministic Büchi automaton and α is an infinite word which does not belong to L(A, G). Then, the (unique) run ρ_{α} of A on α is such that inf(ρ_{α}) ∩ G = ∅. Let \overline{G} denote the complement of G. It follows that inf(ρ_{α}) ∩ \overline{G} ≠ ∅, since some state must occur infinitely often in ρ_{α}. It would be tempting to believe that the automaton (A, \overline{G}) recognizes Σ^{ω} − L(A, G). However, there may be words which admit runs which visit both G and \overline{G} infinitely often. These words will be including both in L(A, \overline{G}) as well as in L(A, G). So, there is no convenient way to express the complement of a Büchi condition again as a Büchi condition.

We shall postpone describing a complementation construction for Büchi automata until Section 4. Till then we shall, however, assume that we can complement these automata.

Intersection Turning to intersection, the natural way to intersect automata A_{1} and A_{2} is to construct an automaton whose state space is the cross product of the state spaces of A_{1} and A_{2} and let both copies process the input simultaneously. For finite words, the input is accepted if each copy can generate a run which reaches a final state at the end of the word.

For infinite inputs, we have to do a more sophisticated product construction. An infinite input α should be accepted by the product system provided both copies generate runs which visit good states infinitely often. Unfortunately, there is no guarantee that these runs will ever visit good states simultaneously—for instance, it could be that the first run goes through a good state after α(0), α(2), … while the second run enters good states after α(1), α(3), … So, the main question is one of identifying the good states of the product system.

The key observation is that to detect that both components of the product visit good states infinitely often, one need not record every point where the copies visit good states; in each copy, it suffices to observe an infinite subsequence of the overall sequence of good states. So, we begin by focusing on the first copy and waiting for its run to enter a good state. When this happens, we switch attention to the other copy and wait for a good state there. Once the second copy reaches a good state, we switch back to the first copy and so on. Clearly, we will switch back and forth infinitely often iff both copies visit their respective good states infinitely often. Thus, we can characterize the good states of the product in terms of the states where one switches back and forth.

Formally, the construction is as follows. Let (A_{1}, G_{1}) and (A_{2}, G_{2}) be two Büchi automata such that A_{i} = (S_{i}, →_{i}, S_{in}^{i}) for i = 1, 2. Define (A, G), where A = (S, →, S_{in}), as follows:

• S = S_{1} × S_{2} × {1, 2}

• The transition relation → is defined as follows:

(s_{1}, s_{2}, 1) ⟶^{a} (s′_{1}, s′_{2}, 1) if s_{1} ⟶^{a}_{1} s′_{1}, s_{2} ⟶^{a}_{2} s′_{2} and s_{1} ∉ G_{1}.

(s_{1}, s_{2}, 1) ⟶^{a} (s′_{1}, s′_{2}, 2) if s_{1} ⟶^{a}_{1} s′_{1}, s_{2} ⟶^{a}_{2} s′_{2} and s_{1} ∈ G_{1}.

(s_{1}, s_{2}, 2) ⟶^{a} (s′_{1}, s′_{2}, 2) if s_{1} ⟶^{a}_{1} s′_{1}, s_{2} ⟶^{a}_{2} s′_{2} and s_{2} ∉ G_{2}.

(s_{1}, s_{2}, 2) ⟶^{a} (s′_{1}, s′_{2}, 1) if s_{1} ⟶^{a}_{1} s′_{1}, s_{2} ⟶^{a}_{2} s′_{2} and s_{2} ∈ G_{2}.

• S_{in} = {(s_{1}, s_{2}, 1) | s_{1} ∈ S_{in}^{1} and s_{2} ∈ S_{in}^{2}}

• G = S_{1} × G_{2} × {2}.

In the automaton A, each product state carries an extra tag indicating whether the automaton is checking for a good state on the first or the second component. The automaton accepts if it switches focus from the second component to the first infinitely often. (Notice that we could equivalently have defined G to be the set G_{1} × S_{2} × {1}.) It is not difficult to verify that L(A, G) = L(A_{1}, G_{1}) ∩ L(A_{2}, G_{2}).

Projection Let Σ_{1} and Σ_{2} be alphabets such that |Σ_{2}| ≤ |Σ_{1}|. A projection function from Σ_{1} to Σ_{2} is a surjective map π : Σ_{1} → Σ_{2}. We can extend π from individual letters to words as usual: if α ∈ Σ_{1}^{ω}, π(α) denotes the word β where β(i) = π(α(i)) for all i in ℕ_{0}.

Let L ⊆ Σ_{1}^{ω}. Then π(L), the projection of L via π, is the language {β ∈ Σ_{2}^{ω} | ∃α ∈ L : β = π(α)}. It is easy to verify that if L is Büchi-recognizable, then so is π(L). Let (A_{1}, G_{1}) be an automaton recognizing L, where A_{1} = (S_{1}, →_{1}, S_{in}^{1}). We construct an automaton A_{2} = (S_{2}, →_{2}, S_{in}^{2}) over Σ_{2} as follows: set S_{2} = S_{1}, S_{in}^{2} = S_{in}^{1} and s ⟶^{b}_{2} s′ iff s ⟶^{a}_{1} s′ for some a ∈ Σ_{1} such that π(a) = b. It is easy to verify that (A_{2}, G_{1}) recognizes π(L).

Emptiness In applications, we will need to be able to check whether the language accepted by a Büchi automaton is empty. To do this, we recall our observation that any accepting run of a Büchi automaton must begin in an initial state, reach a final state g and then cycle back to g infinitely often.

If we ignore the labels on the transitions, we can regard the state space of a Büchi automaton (A, G) as a directed graph G_{A} = (V_{A}, E_{A}) where V_{A} = S and (s, s′) ∈ E_{A} iff for some a ∈ Σ, s ⟶^{a} s′. Recall that a set of vertices X in a directed graph is a strongly connected component iff for every pair of vertices v, v′ ∈ X, there is a path from v to v′. Clearly, L(A, G) is non-empty iff there is a strongly connected component X in G_{A} such that X contains a vertex g from G and X is reachable from one of the initial states. We thus have the following theorem.

Theorem 1.5 The emptiness problem for Büchi automata is decidable.

Notice that it is sufficient to analyze maximal strongly connected components in G_{A} in order to check that L(A, G) ≠ ∅. Computing the maximal strongly connected components of a directed graph can be done in time linear in the size of the graph [AHU74], where the size of a graph G = (V, E) is, as usual, given by |V | + |E|. Checking reachability can also be done in linear time. So, if A has n states, checking that L(A, G) ≠ ∅ can be done in time O(n^{2}).

2 The logic of sequences

Büchi’s original motivation for studying automata on infinite inputs was to solve a decision problem from logic. He discovered a deep and beautiful connection between ω-regular languages and sets of models of formulas in certain logics.

S1S

The logic that Büchi considered was the monadic second-order theory of one successor, abbreviated as S1S. This logic is interpreted over the set ℕ_{0} of natural numbers. In general, second-order logic permits quantification over relations and functions, unlike first-order logic, which permits quantification over just individual variables. However, the fact that we are dealing with a “monadic” second-order logic restricts this extra power to quantification over one-place relations. Since a one-place relation is just a subset, this effectively means that we can quantify over individual elements of ℕ_{0} and subsets of ℕ_{0}. The fact that we are dealing with “one successor” means we are talking about ℕ_{0} with the usual ordering where each element has a unique successor. Permitting two successors, for instance, would produce the infinite binary tree which has countably many nodes but has two successors for each node.

Formally, the logical language S1S is defined as follows.

Terms A term in S1S is built up from the constant 0 and individual variables x, y, … by application of the successor function succ. Thus, the following are terms: 0, succ(x), succ(succ(succ(0))), succ(succ(y)), ….

Atomic formulas Let t, t′, … be terms. An atomic formula is of the form t = t′ or t ∈ X, where X is a set variable.

Formulas A formula is built up from atomic formulas using the boolean connectives ¬ (not) and ∨ (or), together with the existential quantifier ∃. The quantifier ∃ can be applied to both individual and set variables—one can write ∃x and ∃X. In other words, if φ and ψ are inductively assumed to be formulas, so are ¬φ, φ ∨ ψ, (∃x) φ and (∃X) φ.

In addition, we can define the remaining boolean connectives like ∧ (and), ⇒ (if-then), ⇔ (iff) as usual, in terms of ¬ and ∨: for instance, φ ⇒ ψ is defined as (¬φ ∨ ψ). We also have the universal quantifier ∀ which is the dual of ∃: (∀x) φ =^{def} ¬((∃x) ¬φ) and

(∀X) φ =^{def} ¬((∃X) ¬φ).

Assigning truth values to formulas Formulas are interpreted over ℕ_{0}. The constant 0 denotes the number 0. Individual variables x, y, … are interpreted as natural numbers—that is, elements of ℕ_{0}. The function succ corresponds to adding one: succ(x) denotes the number which is one greater than the interpretation of x. Thus, the term succ(succ(succ(0))) represents the number 3. And, if the current interpretation of x is the number 47 then succ(x) denotes 48.

The connective = used in defining atomic formulas denotes equality, as usual. Thus t = t′ is true provided t and t′ denote the same natural number.

Set variables like X, Y, … are interpreted as subsets of ℕ_{0}. The atomic formula t ∈ X is true iff the number denoted by t belongs to the set denoted by X.

Once the interpretation of atomic formulas has been fixed, the meaning of compound formulas involving ¬, ∨ and ∃ is the “natural” one.

Let φ be a formula. A variable is said to occur free in φ if it is not within the scope of a quantifier. For instance, in the formula (∃x)(∀Y) (0 ∈ Y)∨(x = y)∨(x ∈ X), the variables y and X occur free. Variables which do not occur free are said to be bound. In the preceding formula, x and Y are bound. We write φ(x_{1}, x_{2}, …, x_{k}, X_{1}, X_{2}, …, X_{ℓ}) to indicate that all the variables which occur free in φ come from the set {x_{1}, x_{2}, …, x_{k}, X_{1}, X_{2}, …, X_{ℓ}}.

Let \overrightarrow{X} = (x_{1}, x_{2}, …, x_{k}, X_{1}, X_{2}, …, X_{ℓ}). To assign a truth value to the formula φ(\overrightarrow{X}), we

have to first fix an interpretation of the variables in \overrightarrow{X}. In other words, we must map each individual variable x_{i} to a natural number m_{i} ∈ ℕ_{0} and each set variable X_{j} to a subset

M_{j} ⊆ ℕ_{0}. Let \overrightarrow{M} = (m_{1}, m_{2}, …, m_{k}, M_{1}, M_{2}, …, M_{ℓ}). We write \overrightarrow{M} ⊧ φ(\overrightarrow{X}) to denote that φ is true under the interpretation {x_{i} ↦ m_{i}}_{i∈{1,2,...,k}} and {X_{i} ↦ M_{i}}_{i∈{1,2,...,ℓ}}. Rather than go into formal details, we look at some illustrative examples.

Example 2.1

(i) Let Sub(X, Y) = (∀x) x ∈ X ⇒ x ∈ Y.

Then (M, N) ⊧ Sub(X, Y) iff M ⊆ N.

(ii) Let Zero(X) = (∃x) [x ∈ X ∧ ¬(∃y)(y < x)].

This formula asserts that X contains an element which has no predecessors in ℕ_{0}. Thus, M ⊧ Zero(X) iff 0 ∈ M.

(iii) Let Lt(x, y) = (∀Z)[succ(x) ∈ Z ∧ (∀z)(z ∈ Z ⇒ succ(z) ∈ Z)] ⇒ (y ∈ Z).

Then (m, n) ⊧ Lt(x, y) iff m < n. What the formula asserts is that any set Z which contains x+1 and is closed with respect to the successor function must also contain y.

(iv) Let Sing(X) = (∃Y) \begin{matrix}[Sub(Y, X) ∧ (Y ≠ X) ∧ \\ ¬(∃Z) (Sub(Z, Y) ∧ (Z ≠ X) ∧ (Z ≠ Y))]. \end{matrix}

In this formula, X ≠ Y abbreviates ¬(X = Y), where X = Y is itself an abbreviation for Sub(X, Y) ∧ Sub(Y, X). The formula asserts that X has only one proper subset, which is Y. This is true only for singletons, where Y is the empty set. So, M ⊧ Sing(X) iff M is a singleton {m}.

□

A sentence is a formula in which no variables occur free. A sentence φ is either true or false—we do not have to interpret any variables to assign meaning to φ. For instance consider the sentence

(∀X) [0 ∈ X ∧ (∀x) (x ∈ X ⇒ succ(x) ∈ X)] ⇒ (∀x) x ∈ X.

This sentence is true: it expresses the familiar property of mathematical induction for subsets of ℕ_{0}—if a set of natural numbers contains 0 and is closed with respect to the successor function, then the set in fact includes all of ℕ_{0}.

Satisfiability An S1S formula φ(x_{1}, …, x_{k}, X_{1}, …, X_{ℓ}) is said to be satisfiable if we

can choose \overrightarrow{M} = (m_{1}, …, m_{k}, M_{1}, …, M_{ℓ}) such that \overrightarrow{M} ⊧ φ(\overrightarrow{X}).

Büchi showed how to associate an ω-regular language L_{φ} with each S1S formula φ, such that every word in L_{φ} represents an interpretation for the free variables in φ under which the formula φ evaluates to true. Moreover, every interpretation which makes φ true is represented by some word in L_{φ}. Thus, φ is satisfiable iff there is some interpretation which makes it true iff L_{φ} is non-empty. The language L_{φ} is defined over the alphabet {0, 1}^{m}, where m is the number of free variables in φ.

In fact, Büchi showed that the converse is also true. Let us say that a language L ⊆ ({0, 1}^{m})^{ω} is S1S-definable if L = L_{φ} for some S1S formula φ. We can always embed an arbitrary alphabet Σ as a subset of {0, 1}^{m} for some suitable choice of m. In this way, any language L ⊆ Σ^{ω} can be converted into an equivalent language L_{{0,1}} over {0, 1}^{m}. Büchi showed that if L is ω-regular, then L_{{0,1}} is S1S-definable.

Thus, the notions of S1S-definability and ω-regularity are equivalent. The rest of this section will be devoted to formally stating and proving this result.

We begin by defining L_{φ} for an S1S formula φ(x_{1}, x_{2}, …, x_{k}, X_{1}, X_{2}, …, X_{ℓ}). Let

\overrightarrow{M} = (m_{1}, m_{2}, …, m_{k}, M_{1}, M_{2}, …, M_{ℓ}) such that \overrightarrow{M} ⊧ φ(\overrightarrow{X}). We can associate with

\overrightarrow{M} an infinite word α_{M} over \{0, 1\}^{k+ℓ} which represents the characteristic function of \overrightarrow{M}. For i ∈ ℕ_{0}, and j ∈ {1, 2, …, k+ℓ}, let α_{M} (i)(j) denote the j^{th} component of α_{M} (i). Then for i ∈ ℕ_{0} and j ∈ {1, 2, …, k}, α_{M} (i)(j) = 1 iff i = m_{j} and α_{M} (i)(j) = 0 iff i ≠ m_{j}. Similarly, for i ∈ ℕ_{0}, and j ∈ {k+1, k+2, …, k+ℓ}, α_{M} (i)(j) = 1 iff i ∈ M_{j} and α_{M} (i)(j) = 0 iff i ∉ M_{j}. Then

L_{φ} = \{α_{M} | \overrightarrow{M} ⊧ φ(\overrightarrow{X})\}.

Next we define the {0, 1}-image L_{{0,1}} corresponding to a language L over an arbitrary alphabet Σ. Let Σ = {a_{1}, a_{2}, …, a_{m}}. Then, each word α ∈ Σ^{ω} can be represented by a word α_{{0,1}} over {0, 1}^{m}, where for all i ∈ ℕ_{0} and j ∈ {1, 2, …, m}, α_{{0,1}}(i)(j) = 1 if α(i) = a_{j} and α_{{0,1}}(i)(j) = 0 if α(i) ≠ a_{j}. Then

L_{{0,1}} = {α_{{0,1}} | α ∈ L}.

We can now state Büchi’s result more precisely.

Theorem 2.2

(i) Let φ be an S1S formula. Then L_{φ} is an ω-regular language.

(ii) Let L be an ω-regular language. Then L_{{0,1}} is S1S-definable.^{3}

Proof

(i) To show that L_{φ} is ω-regular, we proceed by induction on the structure of φ. To do this, it will be convenient to cut down the language S1S to an equivalent language S1S_{0} which has a simpler syntax.

3We have fixed a apecific embedding of Σ into {0, 1}^{m} which is relatively easy to describe in S1S. In general, we can choose any embedding for defining L_{{0,1}} and the result will still go through.

[figure: s_{1}; s_{2}; ⟹; ⟨1, 0⟩; ⟨0, 0⟩; ⟨0, 1⟩; ⟨1, 1⟩]

Figure 4: Büchi automaton for the atomic formula X ⊆ Y

Formally, in S1S_{0} we do not have individual variables x_{i}—there are only set variables X_{j}. The atomic formulas are of the form X ⊆ Y and succ(X, Y). The first formula is true if X is a subset of Y while the second is true if X and Y are singletons {x} and {y} respectively and y = x+1.

We now argue that every S1S formula φ can be converted to an S1S_{0} formula φ_{0} such that L_{φ} = L_{φ_{0}}.

We begin by eliminating nested applications of the successor function. For instance, if the S1S formula contains the atomic formula succ(succ(x)) ∈ X, we write instead

(∃y)(∃z) y = succ(x) ∧ z = succ(y) ∧ z ∈ X.

We then eliminate formulas of the form 0 ∈ X using the formula Zero(X) defined in Example 2.1.

Finally, we eliminate singleton variables using the formula Sing from Example 2.1. For instance, we rewrite (∀x)(∃y) succ(x) = y ∧ y ∈ Z as

(∀X) (Sing(X) ⇒ [(∃Y) Sing(Y) ∧ succ(X, Y) ∧ Y ⊆ Z]).

Notice that we can uniformly replace Sub(X, Y) by X ⊆ Y in Sing since X ⊆ Y is an atomic formula in SIS_{0}.

We now construct for each S1S_{0} formula φ, a Büchi automaton (A_{φ}, G_{φ}) recognizing L_{φ}.

For the atomic formula X ⊆ Y, the corresponding automaton over {0, 1} × {0, 1} is shown in Figure 4. This automaton accepts any input word which does not contain ⟨1, 0⟩—if α(i) = ⟨1, 0⟩, in the corresponding interpretation, i ∈ X but i ∉ Y, thus violating the requirement that X ⊆ Y.

[figure: ⟹; ⟨0, 0⟩; ⟨0, 0⟩; s_{1}; s_{2}; s_{3}; ⟨1, 0⟩; ⟨0, 1⟩]

Figure 5: Büchi automaton for the atomic formula succ(X, Y)

The other atomic formula is succ(X, Y). The corresponding automaton is shown in Figure 5. This automaton accepts inputs of the form ⟨0, 0⟩^{i}⟨1, 0⟩⟨0, 1⟩⟨0, 0⟩^{ω}, i ∈ ℕ_{0}, corresponding to the interpretation where X = {i} and Y = {i+1}.

For the induction step, we need to consider the connectives ¬, ∨ and ∃X.

Let φ = ¬ψ. Then, L_{φ} is the complement of L_{ψ}. By the induction hypothesis, there exists a Büchi automaton (A_{ψ}, G_{ψ}) which recognizes L_{ψ}. As we mentioned earlier, there is an effective way to construct an automaton (A_{φ}, G_{φ}) recognizing the complement of L_{ψ}. The details will be described in Section 4.

If φ = φ_{1} ∨ φ_{2}, then L_{φ} = L_{φ_{1}} ∪ L_{φ_{2}}. By the induction hypothesis, there exist automata (A_{φ_{1}}, G_{φ_{1}}) and (A_{φ_{2}}, G_{φ_{2}}) such that L(A_{φ_{i}}, G_{φ_{i}}) = L_{φ_{i}} for i = 1, 2. We have seen in Section 1.2 how to construct an automaton (A_{φ}, G_{φ}) such that L(A_{φ}, G_{φ}) = L_{φ_{1}} ∪ L_{φ_{2}}.

Finally, if φ = (∃X_{1}) ψ(X_{1}, X_{2}, … X_{m}), the language L_{φ} corresponds to the projection of L_{ψ} via the function π : {0, 1}^{m} → {0, 1}^{m−1} which erases the first component of each m-tuple in {0, 1}^{m}. A word of (m−1)-tuples belongs to L_{φ} if it can be padded out with an extra component so that the resulting word over m-tuples is in L_{ψ}. This padding operation corresponds to guessing a witness for the set X_{1}. The automaton (A_{φ}, G_{φ}) recognizing L_{φ} can be obtained from (A_{ψ}, G_{ψ}), the automaton recognizing L_{ψ}, as described in Section 1.2.

In this way, we inductively associate with each S1S_{0} formula φ, a Büchi automaton (A_{φ}, G_{φ}) such that L_{φ} = L(A_{φ}, G_{φ}).

There is a slight technicality involved when we deal with sentences. Notice that every time we encounter an existential quantifier, we eliminate one component from the input alphabet of A_{φ}. If φ is a sentence—that is, all variables in φ are bound— we would have erased all components of the input by the time we construct A_{φ}. In other words, A_{φ} will be an input-free automaton whose states and transitions define an unlabelled directed graph. If we were dealing with languages of finite words, we could say that a sentence φ is true iff L_{φ} contains the empty word. Since the empty word is not a member of Σ^{ω}, we would have to slightly modify our definition of L_{φ} to accommodate this case cleanly in our framework. However, we shall not worry too much about this since it is clear that a sentence φ is true iff there is an unlabelled path in the graph corresponding to A_{φ} which begins at some initial state and visits a good state infinitely often.

(ii) Let (A, G) be a Büchi automaton recognizing L ⊆ Σ^{ω}, where Σ = {a_{1}, a_{2}, …, a_{m}} and A = (S, →, S_{in}), with S = {s_{1}, s_{2}, …, s_{k}}. We use free variables A_{1}, A_{2}, …, A_{m} to describe each infinite word over Σ—the variable A_{i} describes the positions in the input where letter a_{i} occurs. We then use existentially quantified variables S_{1}, S_{2}, …, S_{k} to describe runs of the automaton over the input—the variable S_{j} describes the positions in the run where the automaton is in state s_{j}.

The formula φ_{L} can then be written as follows:

(∃S_{1})(∃S_{2}) ⋯ (∃S_{k})
(∀x) ⋁_{i∈{1,2,...,m}} (x ∈ A_{i}) ∧ ⋀_{i∈{1,2,...,m}} (x ∈ A_{i} ⇒ ⋁_{j≠i}x ∉ A_{j})

∧ (∀x) ⋁_{i∈{1,2,...,k}} (x ∈ S_{i}) ∧ ⋀_{i∈{1,2,...,k}} (x ∈ S_{i} ⇒ ⋁_{j≠i}x ∉ S_{j})
∧  ⋁_{s_{i}∈S_{in}} (0 ∈ S_{i})
∧ (∀x) ⋁_{(s_{i},a_{j},s_{k})∈→} (x ∈ S_{i}) ∧ (x ∈ A_{j}) ∧ (succ(x) ∈ S_{k})
∧  ⋁_{s_{i}∈G}  (∀x)(∃y) (x < y) ∧ (y ∈ S_{i})

The first two lines capture the fact that with each position x ∈ ℕ_{0} we associate precisely one input letter and one state from the run. The third line asserts that the position 0 corresponds to an initial state. The fourth line guarantees that the sequence of states represented by S_{1}, S_{2}, …, S_{k} is a run. The last line then says that the run is good—that is, some final state appears infinitely often. It is not difficult to verify that L_{φ_{L}} = L_{{0,1}}.

□

3 Stronger acceptance conditions

As we saw earlier, deterministic Büchi automata cannot recognize all ω-regular languages (Corollary 1.3). It turns out that we can define classes of deterministic automata which recognize ω-regular languages by strengthening the acceptance criterion. We begin with the definition proposed by Muller [Mu63].

Muller automata A Muller automaton is a pair (A, T ) where A = (S, →, S_{in}) is an automaton, as before, and T = ⟨F_{1}, F_{2}, …, F_{k}⟩ is an acceptance table with F_{i} ⊆ S for i ∈ {1, 2, …, k}.

The automaton (A, T ) accepts an input α : ℕ_{0} → Σ if there is a run ρ of A on α such that inf(ρ) ∈ T —that is, inf(ρ) = F_{i} for some i ∈ {1, 2, …, k}.

The acceptance table of a Muller automaton places a much more stringent requirement on runs than a Büchi condition does. The table entry F_{i} makes a positive demand on the states in F_{i}, as well as a negative demand on the states in S −F_{i}—states in F_{i} must all be visited infinitely often while states outside F_{i} must be visited only finitely often. In other words, for a run ρ to satisfy the table entry F_{i}, after some point it must “settle down” in the set F_{i} and visit all the states in this set infinitely often without making transitions to any state outside F_{i}.

Example 3.1 Recall the language L over {a, b} defined in Example 1.1—L contains all words which contain infinitely many occurrences of a. We saw that the deterministic automaton with two states shown in Figure 6 recognizes L with a Büchi condition {s_{1}}.

To accept L using a Muller condition, we retain the same automaton and set the acceptance table to ⟨{s_{1}}, {s_{1}, s_{2}}⟩.

Figure 6: Automaton for L and \overline{L} (Example 3.1)

We also saw that \overline{L}, the complement of L could not be recognized by any deterministic Büchi automaton. However, it is easy to verify that \overline{L} can be recognized with a Muller condition by using the same automaton as for L, but with the acceptance table given by ⟨{s_{2}}⟩. □

Simulations The example shows that deterministic Muller automata are strictly more powerful than deterministic Büchi automata. It is quite straightforward to simulate a Büchi automaton by a Muller automaton—we construct an entry in the Muller table for each subset of states which contains a good state. Formally, let (A, G) be a Büchi automaton, where A = (S, →, S_{in}). The corresponding Muller automaton is given by (A, T_{G}) where T_{G} = {F ⊆ S | F ∩ G ≠ ∅}. It is easy to see that L(A, G) = L(A, T_{G})— any successful run of the Büchi automaton will satisfy one of the entries in the Muller table. Conversely, any run which satisfies an entry in T_{G} must visit a good state infinitely often. Notice that the Muller automaton (A, T_{G}) is deterministic iff the original automaton (A, G) was deterministic: this simulation neither introduces nor removes any non-determinism.

Conversely, any Muller automaton can be simulated by a non-deterministic Büchi automaton. Let (A, T ) be a Muller automaton, where T = ⟨F_{1}, F_{2}, …, F_{k}⟩. For each i ∈ {1, 2, …, k}, we construct a Büchi automaton (A_{i}, G_{i}) such that (A_{i}, G_{i}) accepts an input α iff there is a run ρ of (A, T ) on α with inf(ρ) = F_{i}. It is easy to see that L(A, T ) = ⋃_{i∈{1,2,...,k}} L(A_{i}, G_{i}). As described in Section 1.2, we can then construct a Büchi automaton (A_{T} , G_{T}) which recognizes L(A, T ).

To construct (A_{i}, G_{i}) we proceed as follows. When reading an input α, A_{i} simulates a run of A. At some point, A non-deterministically decides that no more states from S −F_{i} will occur along the run being simulated. After this guess is made, A_{i} will only simulate moves which stay within F_{i}. At the same time, A_{i} repeatedly cycles through F_{i}, checking that all states from F_{i} are seen infinitely often.

Let A = (S, →, S_{in}) and F_{i} = {s_{i_{1}}, s_{i_{2}}, …, s_{i_{m}}}. Then (A_{i}, G_{i}), with A_{i} = (S_{i}, →_{i}, S_{in}^{i}), is defined as follows:

• S_{i} = {(s, finite) | s ∈ S} ∪ {(s, infinite, j) | s ∈ F_{i}, j ∈ {0, 1, …, m−1}}.

• The transition relation →_{i} is given as follows:

(s, finite) ⟶^{a}_{i} (s′, finite) if s ⟶^{a} s′.

(s, finite) ⟶^{a}_{i} (s′, infinite, 0) if s ⟶^{a} s′ and s′ ∈ F_{i}.

(s, infinite, k) ⟶^{a}_{i} (s′, infinite, k) if s ⟶^{a} s′, s′ ∈ F_{i} and s ≠ s_{i_{k+1}}.

(s, infinite, k) ⟶^{a}_{i} (s′, infinite, (k+1) mod m) if s ⟶^{a} s′, s′ ∈ F_{i} and s = s_{i_{k+1}}.

• S_{in}^{i} = {(s, finite) | s ∈ S_{in}}.

• G_{i} = {(s_{i_{m}}, infinite, m−1)}.

These two simulation constructions show that the class of Muller-recognizable languages coincides with the class of Büchi-recognizable languages. In other words, Muller automata also recognize ω-regular languages.

However, Example 3.1 suggests that deterministic Muller automata may suffice for recognizing all ω-regular languages. In fact, this is the case—this non-trivial result was proved by McNaughton [Mc66].

Theorem 3.2 (McNaughton) Every ω-regular language is recognized by a deterministic Muller automaton.

We shall prove McNaughton’s result indirectly in Section 4. Notice that McNaughton’s theorem, combined with the simulation constructions described above, yields a complementation construction for Büchi automata. This is because complementing deterministic Muller automata is easy. Let (A, T ) be a deterministic Muller automaton, where A = (S, →, S_{in}). Let \overline{T} = \{F ⊆ S | F ∉ T \}. It is straightforward to verify that L(A, \overline{T} ) = Σ^{ω} − L(A, T ). So, to complement a Büchi automaton (A, G), we first convert it into an equivalent deterministic Muller automaton (A, T ) using McNaughton’s theorem. We then simulate (A, \overline{T} ) using the construction described earlier to get a Büchi automaton (A\overline{T} , G\overline{T}) which accepts the complement of L(A, G).

Rather than follow this route, we shall describe an alternative determinization construction due to Safra [Sa88]. Safra’s construction converts a Büchi automaton to a deterministic automaton with a pairs table. Acceptance in terms of a pairs table first described by Rabin [Ra69].

Rabin automata A Rabin automaton is a structure (A, PT ) where A = (S, →, S_{in}) is an automaton, as before, and PT = ⟨(G_{1}, R_{1}), (G_{2}, R_{2}), …, (G_{k}, R_{k})⟩ is a pairs table with G_{i}, R_{i} ⊆ S for i ∈ {1, 2, …, k}.

The automaton (A, PT ) accepts an input α : ℕ_{0} → Σ if there is a run ρ of A on α such that for some i ∈ {1, 2, …, k}, inf(ρ) ∩ G_{i} ≠ ∅ and inf(ρ) ∩ R_{i} = ∅.

Thus each pair (G_{i}, R_{i}) in the pairs table of a Rabin automaton specifies a positive and a negative requirement on the run, as in the acceptance table of a Muller automaton. The positive entry G_{i} is just a Büchi condition while the negative entry R_{i} is like the one specified for S − F_{i} by an entry F_{i} in a Muller acceptance table. If we think of G_{i} and R_{i} as “green lights” and “red lights”, a run ρ satisfies (G_{i}, R_{i}) if some green light from G_{i} flashes infinitely often and no red light from R_{i} flashes infinitely often.

Returning to Example 3.1, the language L is accepted by the automaton of Figure 6 with the pairs table ⟨(\{s_{1}\}, ∅)⟩, while \overline{L} is accepted by the same automaton with the pairs table ⟨({s_{2}}, {s_{1}})⟩.

Büchi automata can be trivially simulated by Rabin automata—if (A, G) is a Büchi automaton, the corresponding Rabin automaton is (A, PT_{G}), where PT_{G} = ⟨{G, ∅}⟩.

Conversely, we can simulate Rabin automata by Büchi automata using a construction similar to the one for simulating Muller automata by Büchi automata. As before, it suffices to construct a separate Büchi automaton (A_{i}, G′_{i}) for each entry (G_{i}, R_{i}) in the pairs table of a Rabin automaton (A, PT ). The automaton (A_{i}, G′_{i}) simulates a run of A and guesses when no more states from R_{i} will be seen. It then checks that states from G_{i} occur infinitely often.

Let A = (S, →, S_{in}) and PT = ⟨(G_{1}, R_{1}), (G_{2}, R_{2}), …, (G_{k}, R_{k})⟩. Then (A_{i}, G′_{i}), with A_{i} = (S_{i}, →_{i}, S_{in}^{i}), is defined as follows:

• S_{i} = {(s, finite) | s ∈ S} ∪ {(s, infinite, j) | s ∈ (S − R_{i}), j ∈ {0, 1}}}.

• The transition relation →_{i} is given as follows:

(s, finite) ⟶^{a}_{i} (s′, finite) if s ⟶^{a} s′.

(s, finite) ⟶^{a}_{i} (s′, infinite, 0) if s ⟶^{a} s′ and s′ ∉ R_{i}.

(s, infinite, 0) ⟶^{a}_{i} (s′, infinite, 0) if s ⟶^{a} s′, s′ ∉ R_{i} and s ∉ G_{i}.

(s, infinite, 0) ⟶^{a}_{i} (s′, infinite, 1) if s ⟶^{a} s′, s′ ∉ R_{i} and s ∈ G_{i}.

(s, infinite, 1) ⟶^{a}_{i} (s′, infinite, 0) if s ⟶^{a} s′ and s′ ∉ R_{i}.

• S_{in}^{i} = {(s, finite) | s ∈ S_{in}}.

• G′_{i} = {(s, infinite, 1) | s ∈ (S − R_{i})}.

Notice that a Rabin automaton can also simulated by a Muller automaton in quite a straightforward manner. Let (A, PT ) be a Rabin automaton, where A = (S, →, S_{in}) and PT = ⟨(G_{1}, R_{1}), (G_{2}, R_{2}), …, (G_{k}, R_{k})⟩. Each pair (G_{i}, R_{i}) generates a Muller table T_{i} = {F ⊆ (S − R_{i}) | F ∩ G_{i} ≠ ∅}. Let T = ⋃_{i∈{1,2,...,k}} T_{i}. It is easy to see that (A, T ) recognizes L(A, PT ). Once again, since we have not modified A, the simulating automaton is deterministic iff the original automaton was.

To simulate Muller automata using Rabin automata one has to use a construction which is pretty much the same as the one for simulating Muller automata by Büchi automata. Such a simulation introduces non-determinism: there is no straightforward way to directly simulate a deterministic Muller automaton by a deterministic Rabin automaton even though deterministic Rabin automata do recognize all ω-regular languages, as we shall see in the next section.

The last acceptance condition we look at is obtained by interpreting the pairs table of a Rabin automaton in a complementary fashion.

Streett automata A Streett automaton is a structure (A, PT ) where A = (S, →, S_{in}) and PT = ⟨(G_{1}, R_{1}), (G_{2}, R_{2}), …, (G_{k}, R_{k})⟩ are defined in the same way as for Rabin automata.

The Streett automaton (A, PT ) accepts an input α : ℕ_{0} → Σ if there is a run ρ of A on α such that for every i ∈ {1, 2, …, k}, if inf(ρ) ∩ G_{i} ≠ ∅ it is also the case that inf(ρ) ∩ R_{i} ≠ ∅.

These automata were defined by Streett in [St88]. They are useful for describing fairness conditions in infinite computations—for instance, conditions of the form “if a request for a resource is made infinitely often, then the system grants access to the resource infinitely often”. The following observation is immediate from the close connection between Rabin and Streett automata.

Proposition 3.3 Let (A, PT ) be a deterministic automaton with a pairs table. Let L_{R} be the language accepted by (A, PT ) when PT is interpreted as a Rabin condition and L_{S} be the language accepted by (A, PT ) when PT is interpreted as a Streett condition. Then L_{S} is the complement of L_{R}.

As usual, simulating a Büchi automaton (A, G) by a Streett automaton is easy. Let A = (S, →, S_{in}). Construct an automaton (A, PT_{G}) where PT_{G} = ⟨(S, G)⟩. Since inf(ρ) ∩ S must be non-empty for any run ρ of A, it follows that a run ρ satisfies the pair (S, G) iff inf(ρ) ∩ G ≠ ∅, which is precisely what the Büchi condition demands.

In the converse direction, Safra describes a construction due to Vardi which shows that Streett automata can be efficiently simulated by Büchi automata [Sa88].

Lemma 3.4 Let (A, PT ) be a Street automaton where A = (S, →, S_{in}). Let n = |S| and let k be the number of pairs in PT : that is, PT = ⟨(G_{1}, R_{1}), (G_{2}, R_{2}), …, (G_{k}, R_{k})⟩. Then, we can construct a Büchi automaton (A′, G′) with A′ = (S′, →′, S′_{in}) such that L(A′, G′) = L(A, PT ) and |S′| = n · 2^{O(k)}.

Proof The automaton A′ simulates A. As usual, A′ guesses an initial prefix of the run after which every state which is visited by the run will in fact be visited infinitely often. After making this guess, A checks that the acceptance criterion is met for each pair (G_{i}, R_{i}) ∈ PT . In other words, for every i such that some state from G_{i} appears in the infinite portion of the run, A′ ensures that some state from R_{i} also appears infinitely often. To do this, A′ maintains two sets as part of its state. The first set accumulates the list of indices corresponding to pairs (G_{i}, R_{i}) where some element of G_{i} occurs infinitely often. The second set repeatedly accumulates indices of pairs (G_{i}, R_{i}) for which some element of R_{i} has been visited. Each time the second set becomes as large as the first, it is reset to empty. It is not difficult to see that the acceptance criterion specified by PT is met iff the second set is reset to empty infinitely often during the simulation.

Formally, we construct (A′, G′) as follows:

• S′ = {(s, finite) | s ∈ S} ∪ {(s, X_{1}, X_{2}) | s ∈ S and X_{1}, X_{2} ⊆ {1, 2, …, k}}.

• The transition relation →′ is defined as follows:

(s, finite) ⟶^{a}′ (s′, finite) if s ⟶^{a} s′.

(s, finite) ⟶^{a}′ (s′, ∅, ∅) if s ⟶^{a} s′.

(s, X, Y) ⟶^{a}′ (s′, X ∪ G_{s′}, Y ∪ R_{s′}) if s ⟶^{a} s′ and X ∪ G_{s′} ⊈ Y ∪ R_{s′},

where \begin{matrix}G_{s′} = \{i ∈ \{1, 2, …, k\} | s′ ∈ G_{i}\} and \\ R_{s′} = \{i ∈ \{1, 2, …, k\} | s′ ∈ R_{i}\}. \end{matrix}

(s, X, Y) ⟶^{a}′ (s′, X ∪ G_{s′}, ∅) if s ⟶^{a} s′ and X ∪ G_{s′} ⊆ Y ∪ R_{s′}.

• S_{in}^{i} = {(s, finite) | s ∈ S_{in}}.

• G_{i} = {(s, X, ∅) | s ∈ S, X ⊆ {1, 2, …, k}}.

□

4 Determinizing Büchi automata

We now describe an elegant construction due to Safra for determinizing Büchi automata [Sa88]. Safra’s construction converts a non-deterministic Büchi automaton (A, G) into a deterministic Rabin automaton (A_{G}, PT_{G}) such that L(A_{G}, PT_{G}) = L(A, G). If we regard (A_{G}, PT_{G}) as a Streett automaton, we get a deterministic automaton recognizing the complement of L(A, G). By Lemma 3.4, we can simulate the Streett automaton (A_{G}, PT_{G}) by a Büchi automaton. Thus Safra’s construction also solves the complementation problem for Büchi automata.

Also, recall that it is easy to convert a deterministic Rabin automaton into a deterministic Muller automaton. As a consequence, Safra’s construction gives an indirect proof of McNaughton’s Theorem (Theorem 3.2).

Safra’s determinization construction for Büchi automata is a clever extension to the infinite word case of the classical subset construction for determinizing automata on finite words. In order to motivate the construction, we begin with the subset construction for finite words and enhance it in a graded manner to achieve the final result.

Subset construction For automata on finite words, the subset construction is the standard way to eliminate non-determinism. If the original automaton is (A, F), with A = (S, →, S_{in}), each state of the subset automaton (S_{sub}, →_{sub}, S_{in}^{sub}) is a subset of S. The (single) initial state of the subset automaton is the set S_{in} of initial states of A. The subset automaton’s transition relation →_{sub} is defined as follows:

X ⟶^{a}_{sub} Y iff Y = {y ∈ S | ∃x ∈ X : x ⟶^{a} y}.

Henceforth, we use δ_{sub}(X, a) to denote the set Y such that X ⟶^{a}_{sub} Y.

The subset automaton satisfies the following property: If X ⟶^{w}_{sub}^{+} Y then for each state y in Y, there is an state x ∈ X such that x ⟶^{w}^{+} y in the original automaton.

From this, it follows that if we set the set of final states of the subset automaton to be F_{sub} = {X ⊆ S | S ∩ F ≠ ∅}, then (A_{sub}, F_{sub}) recognizes the same set of words as the original automaton.

Let (A, G) be a non-deterministic Büchi automaton, with A = (S, →, S_{in}). The natural extension of the subset construction to Büchi automata would set the good states of the subset automaton to G_{sub} = {X ⊆ S | X ∩ G ≠ ∅}.

It is easy to see that if (A, G) accepts an input α, so will (A_{sub}, G_{sub}). Unfortunately, the converse is not true—the subset automaton will accept words which are not part of the original language.

Example 4.1 Consider the automaton of Example 1.1 (Figure 3) which recognizes \overline{L} over \{a, b\} given by \overline{L} = \{α | α has only a finite number of occurrences of a\}.

In this example, G_{sub}, the set of good states of the extended subset automaton, is given by {{s_{1}, s_{2}}, {s_{2}}}. On the input (ab)^{ω} = ababab ⋯, the (unique) run of the subset

[figure: ⋯; a; a; b; b; s_{1}; s_{1}; s_{1}; s_{2}; s_{1}; s_{1}; s_{2}]

Figure 7: A run of the extended subset automaton for \overline{L} on input (ab)^{ω} (Example 4.1)

automaton is {s_{1}}({s_{1}}{s_{1}, s_{2}})^{ω} = {s_{1}}{s_{1}}{s_{1}, s_{2}}{s_{1}}{s_{1}, s_{2}}{s_{1}}{s_{1}, s_{2}} · · ·. Since this run visits G_{sub} infinitely often, the automaton (A_{sub}, G_{sub}) accepts the word (ab)^{ω}, even though a occurs infinitely often in this word.

The problem with the subset construction is best brought out by drawing all the “threads” between the individual subsets in this run of the subset automaton—see Figure 7.

As we can see, every finite run of the original automaton which reaches a good state actually dies out at that point. In general, all that this subset construction guarantees is that the original automaton has arbitrarily long finite runs which visit good states. □

Marked subset construction We next try to strengthen the subset construction so that it explicitly keeps track of the threads between subsets. In the marked subset construction, in addition to keeping a subset of states, the subset automaton also has the ability to “mark” each state in the subset. A state in the current subset is marked if it satisfies one of two conditions: either it is a good state, or it has a marked predecessor in the previous subset. However, if all the states in the previous subset are marked, then only good states are marked in the current subset—no marks are inherited from a fully marked state. The good states in the marked subset automaton are those where the entire subset is marked.

Concretely, let (A, G) be the original non-deterministic Büchi automaton with A = (S, →, S_{in}). Then, the marked subset automaton (A_{M}, G_{M}), with A_{M} = (S_{M}, →_{M}, S_{in}^{M}), is given as follows.

• S_{M} = {(X, f) | X ⊆ S, f : X → {marked, unmarked}}.

• The transition function →_{M} is as follows:

(X, f) ⟶^{a}_{M} (Y, g) iff

– Y = δ_{sub}(X, a).

(Recall that Y = δ_{sub}(X, a) iff in the normal subset automaton, X ⟶^{a}_{sub} Y.)

– If f(x) = marked for all x ∈ X then

∀y ∈ Y : g(y) = \{ \begin{matrix}marked & if y ∈ G \\ unmarked & otherwise \end{matrix}

else

∀y ∈ Y : g(y) = \{ \begin{matrix}marked & if y ∈ G or \\ & (∃x ∈ X : f(x) = marked and x ⟶^{a} y) \\ unmarked & otherwise \end{matrix} • S_{in}^{M} = {(S_{in}, f) | ∀s ∈ S_{in} : f(s) = marked}.

• G_{M} = {(X, f) | ∀x ∈ X : f(x) = marked}.

The main property satisfied by this automaton is the following.

Let ρ be a run of (A_{M}, G_{M}) on an input α such that ρ(i) = (X_{i}, f_{i}) for all i ∈ Nat. Suppose that (X_{k}, f_{k}) ∈ G for some k > 0. Let j be the largest natural number less than k such that (X_{j}, f_{j}) ∈ G—such a number j must exist because the initial state of A_{M} belongs to G. Then, for each state y ∈ Y_{k}, there is a state x ∈ X_{j} such that x −^{\underline{α[j..k−1]}} →^{∗} y in the original automaton and, moreover, when going from x to y on reading α[j..k−1], the original automaton goes through some good state.

From this observation, we can deduce that the marked subset construction is sound.

Proposition 4.2 Let (A_{M}, G_{M}) be the marked subset automaton which corresponds to the Büchi automaton (A, G). Then, if (A_{M}, G_{M}) accepts an input α, so does (A, G).

Proof Let ρ_{α} be the (unique) run of A_{M} on an input α with ρ_{α}(i) = (X_{i}, f_{i}) for i ∈ ℕ_{0}. If (A_{M}, G_{M}) accepts α, there must be an infinite sequence of positions {i_{0}, i_{1}, …} ⊆ ℕ_{0} such that 0 = i_{0} < i_{1} < ⋯ and (X_{j}, f_{j}) ∈ G for all j ∈ {i_{0}, i_{1}, …}.

From our previous observation about the marked subset construction, we know that for each index i_{k+1} in the set {i_{0}, i_{1}, …} and for each state x ∈ X_{i_{k+1}}, there is a state y ∈ X_{i_{k}} such that in the original automaton, there is a sequence of transitions leading from y to x on the input α[i_{k}..i_{k+1}−1] which passes through some good state. Let us call such a state y a good predecessor of x.

We construct an infinite tree T_{α} as follows. The root of the tree is the set S_{in} of initial states. At each level k of the tree, k ≥ 1, we have a node n_{(x,i_{k})} corresponding to each state x ∈ X_{i_{k}}. The parent of a node n_{(x,j)} at level j, j > 1, is a node n_{(y,j−1)} at level j−1 such y is a good predecessor of x. (Of course, x may have more than one good predecessor. If this is the case, we arbitrarily select one of them and make the corresponding node the parent of n_{(x,j)} in the tree.)

The tree T_{α} is finitely branching and has an infinite number of nodes. By König’s lemma, it must have an infinite path. Each infinite path in T_{α} corresponds to a run of the original automaton A on α. By construction, such a run must pass through a good state between each level in the tree. Thus, A has at least one run on α which meets G infinitely often. □

Unfortunately, though the marked subset construction is sound, it is not complete—there may be inputs accepted by (A, G) which are not accepted by (A_{M}, G_{M}). Consider the following example.

Example 4.3

In the Büchi automaton shown in Figure 8, the input a^{ω} generates the sequence of subsets {s_{0}}({s_{1}, s_{2}})^{ω}. Since s_{2} is not a final state, the subset {s_{1}, s_{2}} never becomes fully marked. Thus, though the original automaton has an accepting run s_{0}s_{1}^{ω} on this input, the marked subset construction fails to detect this. □

The problem is that the marked subset construction demands too much from the underlying runs. As the example shows, it should be sufficient to identify a portion of the subset which is marked and which can infinitely often regenerate its marks.

[figure: s_{0}; s_{1}; s_{2}; a; a; a; a; ⟹]

Figure 8: The marked subset construction is not complete (Example 4.3)

Hierarchical Marked Subset Construction A first attempt to weaken the marked subset construction would be to have a hierarchy of marks. At the base level, the subset automaton runs the marked subset construction and marks states using a level 1 mark. The states which have level 1 marks then start off a nested copy of the marked subset construction with level 2 marks. Similarly, the states which have level 2 marks start off a marked subset construction with level 3 marks. What we would like to detect is whether some level i can get completely marked. This corresponds to checking if the set of nodes marked at level i is equal to the set of nodes marked at level i+1. If so, we reset all marks at levels greater than i and continue.

Since the number of nodes marked at level i is always strictly greater than the set of nodes marked at level i+1, there can be at most as many levels as there are states in the original automaton.

To specify the acceptance condition, we need to verify that some level i+1 gets set to empty infinitely often and that level i does not get set to empty in between. In other words, level i denotes a permanent thread through the subset construction which gets marked infinitely often. To do this, we have to pass from a Büchi condition to a Rabin condition—for each i, a positive condition for level i+1 has to be qualified by a negative condition for level i.

Here is a formal description of a hierarchical marked subset construction which attempts to achieve this goal. Let (A, G) be a Büchi automaton, with A = (S, →, S_{in}). Define (A_{H}, PT_{H}), with A_{H} = (S_{H}, →_{H}, S_{in}^{H}), as follows:

• Let |S| = n. S_{H} consists of pairs of the form (σ, χ) where:

– σ : {1, 2, …, n} → 2^{S} is a subset list satisfying the condition that σ(i+1) is a proper subset of σ(i) whenever σ(i) is non-empty.

– χ : {1, 2, …, n} → {white, green} is a colour list.

• S_{in}^{H} = (σ_{0}, χ_{0}), where σ_{0}(1) = S_{in}, σ_{0}(i) = ∅ for all i ∈ {2, 3, …, n} and χ(i) = white for all i ∈ {1, 2, …, n}.

• The transition function →_{H} performs the following sequence of actions. Initially, each level runs the subset construction locally. Next, any final states appearing in the new subset at level i are added to the subset at level i+1—this corresponds to generating fresh marks at level i. We now look for the smallest level i whose subset is the same as that at level i+1. If such an i exists, we “clear out” the subset list from level i+1 onwards and set the colour of level i to green.

More formally, on reading an input a, the state (σ, χ) generates a new state (σ′, χ′) as follows:

(i) Let σ_{1} : {1, 2, …, n + 1} → 2^{S} be defined as follows:

– σ_{1}(1) = δ_{sub}(σ(1), a).

– For i ∈ {2, 3, …, n}, σ_{1}(i) = δ_{sub}(σ(i), a) ∪ (δ_{sub}(σ(i−1), a) ∩ G).

– σ_{1}(n+1) = δ_{sub}(σ(n), a) ∩ G.

(ii) If there is no index i ∈ {1, 2, …, n} such that σ_{1}(i) = σ_{1}(i+1), then

– σ′(i) = σ_{1}(i) for all i ∈ {1, 2, …, n}.

– χ′(i) = white for all i ∈ {1, 2, …, n}.

else, let m be the smallest index such that σ_{1}(m) = σ_{1}(m+1). Then,

– σ′(i) = σ_{1}(i) for all i ∈ {1, 2, …, m} and σ′(i) = ∅ for all i > m.

– χ′(m) = green and χ′(i) = white for all i ≠ m.

• The acceptance table PT_{H} consists of n pairs ⟨(G_{1}, R_{1}), (G_{2}, R_{2}), …, (G_{n}, R_{n})⟩ where:

– R_{i} = {(σ, χ) | σ(i) = ∅}

– G_{i} = {(σ, χ) | χ(i) = green}

In this construction, the list σ implicitly records the levels of marks associated with the states in the current subset—a state s belongs to σ(i+1) iff s has a level i mark in the current subset. It is not difficult to show that this construction is complete.

Proposition 4.4 Let (A_{H}, PT_{H}) be the hierarchical marked subset automaton which corresponds to the Büchi automaton (A, G). If (A, G) accepts an input α, so does (A_{H}, PT_{H}).

Proof Suppose (A, G) accepts α. Then, α admits a run ρ which visits G infinitely often. We must show that the unique run ρ_{α} of A_{H} on α satisfies some entry in PT_{H}.

For j ∈ ℕ_{0}, let ρ_{α}(j) = (σ_{j}, χ_{j}). We know that for all j ∈ ℕ_{0}, σ_{j}(1) is the set of states maintained by the subset construction. Since ρ is a valid run of A on α, σ_{j}(1) is always non-empty. So, ρ_{α} satisfies condition R_{1}. If it also satisfies G_{1} then (A_{H}, PT_{H}) accepts α and we are done.

If ρ_{α} does not satisfy G_{1}, let k_{0} be the last position where the colour of the first level is green. We wait for the first position i_{0} > k_{0} where ρ, the accepting run of A on α, next visits a good state. We know that σ_{j}(2) is non-empty for all j ≥ i_{0}—once the good state seen at position i_{0} gets pushed to level 2, the accepting run ρ will be part of the subset construction maintained at level 2, thus guaranteeing that at least one valid state is generated at each point. So, ρ_{α} satisfies R_{2}. If it also satisfies G_{2} we are done.

Otherwise, we repeat the argument above and deduce that ρ_{α} satisfies R_{3}, with the accepting run ρ a part of σ_{j}(3) for all j greater than a finite index i_{1}. We can repeat this

[figure: g_{1}; ⟹; a, b; g_{2}; b; a; a; b; s]

Figure 9: The hierarchical marked subset construction is not sound (Example 4.5)

argument only a finite number of times, till we reach level n. The subset maintained at level n can never be more than a singleton. If the accepting run ρ is part of the subset construction at level n, it must generate the signal green infinitely often in which case ρ_{α} satisfies the pair (G_{n}, R_{n}). □

Unfortunately, the hierarchical subset construction is not sound. Consider this example.

Example 4.5

The automaton shown in Figure 9 does not accept the input (ba)^{ω}. However, the run of the hierarchical marked subset automaton on this input is the following:

1 ({s}, white)
2 (∅, white)
3 (∅, white)

⟶^{b}_{H}

1 ({s, g_{1}}, white)
2 ({g_{1}}, white)
3 (∅, white)

⟶^{a}_{H}

1 ({s, g_{2}}, white)
2 ({g_{2}}, green)
3 (∅, white)

⟶^{b}_{H}

1 ({s, g_{1}, g_{2}}, white)
2 ({g_{1}, g_{2}}, white)
3 ({g_{2}}, white)

⟶^{a}_{H}

1 ({s, g_{2}}, white)
2 ({g_{2}}, green)
3 (∅, white)

⟶^{b}_{H} ⋯

Since level 2 remains populated forever and turns green infinitely often, the hierarchical construction incorrectly accepts this input. □

In the preceding example, the problem is that the good state g_{2} which appears to be permanently part of level 2 is actually a transient state. Each time an a is read, the g_{2} state at level 2 disappears, only to be replaced by a fresh copy of g_{2} which is pushed from level 1.

To rectify this defect, Safra’s construction maintains each level of marks as a disjoint set of nodes. The hierarchy of subsets then becomes a tree, with the set at level 1 as the root.

Safra’s Construction Before presenting Safra’s construction, we review some terminology regarding trees. A tree is a structure T = (V, v_{r}, π) where V is a set of nodes, v_{r} ∈ T is a special node known as the root and for all v ∈ V − {v_{r}}, π(v) ∈ T fixes the parent of the node. If v = π^{i}(v′) for some i > 0, we say that v is an ancestor of v′. The root v_{r} is an ancestor of every other node. If v′ = π(v) then v is said to be a child of v′. We assume that for any node v, all the children of v are ordered so that we can talk of one child being to the left of another. This generates a total order on nodes—if v and v′ are nodes, we say that v < v′ if v is an ancestor of v′ or if there is a common ancestor u of v and v′ such that v is in the subtree rooted at a child u_{1} of v, v′ is in the subtree rooted at a child u_{2} of v and u_{1} is to the left of u_{2}.

Given a Büchi automaton (A, G), with A = (S, →, S_{in}), Safra’s construction produces a Rabin automaton (A_{G}, PT_{G}), with A_{G} = (S_{G}, →_{G}, S_{in}^{G}). The automaton (A_{G}, PT_{G}) is as follows:

• Each state in S_{G} is a structure (T, σ, χ, λ) where

– T = (V, v_{r}, π) is a tree.

– σ : V → 2^{S} associates a set of states of A with each node in V in such a way that:

∗ The union of the sets associated with the children of a node v is a proper subset of σ(v).

∗ If v and v′ are two nodes such that v is not an ancestor of v′ and v′ is not an ancestor of v then σ(v) is disjoint from σ(v′).

∗ If σ(v) = ∅, then v is the root v_{r}.

It is not difficult to verify that the conditions imposed on the function σ ensure that |V | can be no larger than n, where n is the number of states in S.

– χ : V → {white, green} fixes a colour for each node.

– λ : V → L is an injective function which attaches a label from the set L = {ℓ_{1}, ℓ_{2}, …, ℓ_{2n}} to each node. Notice that L has 2n elements.

• On reading an input a, the state (T, σ, χ, λ) is transformed to the state (T′, σ′, χ′, λ′) as follows:

(i) Let T = (V, v_{r}, π). Expand the T to a tree T_{1} = (V_{1}, v_{r}, π_{1}) as follows: For each v ∈ V, if σ(v) ∩ G ≠ ∅, add a node v′ such that π_{1}(v′) = v and v′ is the right-most child of v.

(ii) Extend σ and λ to functions σ_{1} and λ_{1} over T_{1} as follows: For all nodes v in V_{1} ∩ V, let σ_{1}(v) = σ(v). For a new node v ∈ V_{1} − V, σ_{1}(v) = σ(π_{1}(v)) ∩ G. All nodes v in V_{1} ∩ V inherit the label λ(v). For each node in V_{1} − V, choose a new label from L which is not assigned to any other node. Since there 2n labels to choose from, this is always possible—each node in V generates at most one new child in V_{1} and there were not more than n nodes in V.

(iii) For every node v, apply the subset construction locally. In other words, define a new function σ′_{1} : V_{1} → 2^{S} such that σ′_{1}(v) = δ_{sub}(σ_{1}(v), a) for all v ∈ V_{1}.

At this stage, we have to “clean up” T_{1} and σ′_{1} so that the structure once again satisfies the conditions specified for states of A_{G}.

(iv) For every node v ∈ V_{1}, if s ∈ σ′_{1}(v) and s also belongs to σ′_{1}(v′) for some smaller node v′, v′ < v, (recall the total order on all nodes in a tree) remove s from σ′_{1}(v).

(v) Remove all nodes v such that σ′_{1}(v) = ∅ and v is not the root v_{r}.

(vi) For each node v such that σ′_{1}(v) is equal to ⋃{σ′_{1}(v′) | v = π_{1}(v′)}, remove all the children of v and set χ_{1}(v) = green. For all other nodes, set χ_{1}(v) = white.

(vii) Let the set of nodes remaining be V′. For v ∈ V′, σ′(v) is that part of σ′_{1}(v) which remains after discarding states which already appear to the left, as specified in step (iv) above. The label λ′(v) of a node v is retained from T_{1}. Finally, set χ′ = χ_{1}.

• The initial state of A_{G} is the tree ({v_{r}}, v_{r}, ∅) where σ(v_{r}) = S_{in}, χ(v_{r}) = white and λ(v_{r}) = ℓ_{1}.

• The pairs table PT_{G} = ⟨(G_{1}, R_{1}), (G_{2}, R_{2}), …, (G_{2n}, R_{2n})⟩ is defined as follows:

– R_{i} = {(T = (V, v_{r}, π), σ, χ, λ) | ∀v ∈ V : λ(v) ≠ ℓ_{i}}.

– G_{i} = {(T = (V, v_{r}, π), σ, χ, λ) | ∃v ∈ V : λ(v) = ℓ_{i} and χ(v) = green}.

The labelling procedure guarantees that the labels of new nodes added at each stage are disjoint from the labels of the existing nodes. In other words, if a node labelled ℓ_{i} is deleted from the tree during a transition, the label ℓ_{i} temporarily disappears from the tree.

Thus, an entry (G_{i}, R_{i}) in the pairs table specifies the following condition. The condition R_{i} is satisfied if at some stage a node labelled ℓ_{i} is added to the tree and it is never deleted henceforth. The condition G_{i} then says that this node turns green infinitely often.

Figure 10 describes the run generated by Safra’s construction on the input (ba)^{ω} for the automaton shown in Figure 9. In the figure, each node of a tree is denoted by a circle, with the label indicated inside the circle and the associated subset written by its side. Nodes coloured green are drawn as double circles, while white nodes are drawn as single circles. When selecting labels for new nodes added to the tree at each stage, we have followed the policy of using the first “free” label in L.

At the second level of the tree, nodes labelled ℓ_{2} and ℓ_{3} turn green infinitely often, so the run satisfies G_{2} and G_{3}. However, since both these labels also disappear from the tree infinitely often, the run does not satisfy R_{2} or R_{3}, thus ensuring that the automaton rejects this input.

It is not difficult to see that Safra’s construction satisfies a property similar to the only described for the marked subset construction:

Let ρ be a run of (A_{G}, PT_{G}) on an input α such that ρ(i) = (T_{i}, σ_{i}, χ_{i}, λ_{i}) for all i ∈ ℕ_{0}. Let j, k ∈ ℕ_{0} with j < k and ℓ be a label from L such that:

• For all positions i ∈ {j, j+1, …, k}, there is a node v in the tree T_{i} such that λ_{i}(v) = ℓ.

• χ_{j}(v) = χ_{k}(v) = green and for all i such that j < i < k, χ_{i}(v) = white.

[figure: ℓ_{1}; ℓ_{3}; {g_{2}}; ℓ_{1}; ℓ_{3}; {g_{2}}; ℓ_{1}; ℓ_{2}; ℓ_{1}; ℓ_{2}; b; b; a; a; ⋯; ℓ_{1}; {s}; ℓ_{1}; b; {s, g_{1}}; ℓ_{1}; ℓ_{2}; ℓ_{1}; ℓ_{2}; {g_{2}}; a; b; a; {s, g_{2}}; {s, g_{1}, g_{2}}; {s, g_{2}}; {g_{2}}; {g_{2}}; {s, g_{1}, g_{2}}; {g_{2}}; {s, g_{2}}; {s, g_{1}, g_{2}}]

Figure 10: A run generated by Safra’s construction

Then, for each state y ∈ σ_{k}(v), there is a state x ∈ σ_{j}(v) such that x −^{\underline{α[j..k−1]}} →^{∗} y in the original automaton and, moreover, when going from x to y on reading α[j..k−1], the original automaton goes through some good state.

Once we have this property, the soundness of Safra’s construction follows from an argument very similar to the one described for the marked subset construction in Proposition 4.2. In other words, we can show the following.

Proposition 4.6 Let (A_{G}, PT_{G}) be the Rabin automaton generated by Safra’s construction, corresponding to the Büchi automaton (A, G). Then, if (A_{G}, PT_{G}) accepts an input α, so does (A, G).

Proof As in the proof of Proposition 4.2, we construct a finitely branching tree T_{α} with an infinite set of nodes for each input α and argue that each infinite path in T_{α} corresponds to an accepting run of A on α. We omit the details. □

The completeness of Safra’s construction is shown by an argument similar to the one described for the hierarchical marked subset construction.

Proposition 4.7 Let (A_{G}, PT_{G}) be the Rabin automaton generated by Safra’s construction corresponding to the Büchi automaton (A, G). If (A, G) accepts an input α, so does (A_{G}, PT_{G}).

Proof Suppose (A, G) accepts α. Then, α admits a run ρ which visits G infinitely often. We must show that the unique run ρ_{α} of A_{G} on α satisfies some entry in PT_{G}.

For j ∈ ℕ_{0}, let ρ_{α}(j) = (T_{j}, σ_{j}, χ_{j}, λ_{j}). Initially, the root v_{r} is assigned the label ℓ_{1}. Since the root is never removed, the run ρ_{α} satisfies R_{1}. If it also satisfies G_{1} then (A_{G}, PT_{G}) accepts α and we are done.

If ρ_{α} does not satisfy G_{1}, let k_{1} be the last position at which the root is coloured green. Let i_{1} be the first position after k where ρ, the accepting run of A on α, visits G. At this point, a child v_{1} of the root comes into existence.

We know that the accepting run ρ is part of the overall subset construction maintained by the root node. Once v_{1} is created, we know that ρ is also being maintained at the first level. It would appear that the run is maintained by v_{1} itself, but there is a subtle complication to be taken into account. Since we only retain the left-most copy of each state, the run ρ may be passed on by v_{1} to some sibling on the left. In any case, it can only move left a finite number of times. Let us suppose it eventually settles down at some node v′_{1}.

It is not difficult to verify that the node v′_{1} must already have been in the tree when v_{1} was added. Let ℓ_{i_{1}} = λ_{i_{1}}(v′_{1}) be the label of v′_{1}. Since α never dies out, v′_{1} will never be deleted from the tree. In other words, ρ_{α} satisfies the condition R_{i_{1}}. If it satisfies the corresponding condition G_{i_{1}} we are done.

Otherwise, let k_{2} be the last time where v′_{1} turns green. As before, we wait for i_{2}, the next time ρ visits a good state, and look at the child v_{2} of v′_{1} which is created at this point. The run ρ is copied into the subset maintained by v_{2} and passed on left a finite number of times till it settles down at a node v′_{2}. If ℓ_{i_{2}} is the label of v′_{2}, ρ_{α} must satisfy R_{i_{2}}. If ρ_{α} does not also satisfy G_{i_{2}} we push ρ down one more level.

Since there are only n levels in the tree, we cannot do this indefinitely. Thus, we must eventually find a node v′_{m} labelled ℓ_{i_{m}} such that ρ_{α} satisfies the pair (G_{i_{m}}, R_{i_{m}}). □

The complexity of Safra’s construction The automaton A_{G} has 2^{O(n log n)} states, where n is the number of states in A. To see this, we estimate the number of bits required to write down a typical state of A_{G}. We have to specify the structure (T, σ, λ, χ).

Since T has at most n nodes, we can “name” the nodes {1, 2, …, n}, with v_{r} = 1. The structure (V, v_{r}, π) can then be written down as a list of the form {π(i)}_{i∈{1,2,...,n}}. Since π(i) ∈ {1, 2, …, n} requires log n bits to write down, T can be described using n log n bits. Similarly, λ and χ can be written as lists of length n with each entry made up of log n bits and 1 bit, respectively.

The only catch is with σ—if we naïvely represent the function σ : V → 2^{S} as a list of subsets, we will need n bits to represent each entry, resulting in n^{2} bits overall. However, notice that if a state s belongs to σ(v) and σ(v′) for two different nodes v and v′ it must be the case that v is an ancestor of v′ or that v′ is an ancestor of v. Also, if s ∈ σ(v), s must belong to σ(v′) for every ancestor v′ of v, all the way upto the root. Thus, we can characterize the set of nodes where s appears in terms of the lowest node v_{s} such that s ∈ σ(v_{s}): if s ∈ σ(v_{s}) then s ∈ σ(v′) for any other node v′ iff v′ is an ancestor of v_{s}. In this way, σ can also be represented as a list of length n by matching each state s in S to its corresponding node v_{s} in V. Each entry in this list can be written down using log n bits.

Since we can characterize a state of A_{G} using O(n log n) bits, it follows that the number of distinct states is bounded by 2^{O(n log n)}.

The number of pairs in PT_{G} is O(n)—by construction, there is a pair (G_{i}, R_{i}) for each label ℓ_{i} ∈ L and L contains exactly 2n elements.

By Lemma 3.4, we can simulate the Streett automaton (A_{G}, PT_{G}) by a Büchi automaton with 2^{O(n log n)} states. Thus, complementing Büchi automata using Safra’s construction results in the state space blowing up from n to 2^{O(n log n)}. Recall that for automata on finite words, the number of states in the complement (via the subset construction) is 2^{O(n)}. It has been shown that the bound achieved by Safra’s construction is optimal [Mi88].

Why complement Büchi automata? We have seen that if we work with Muller, Rabin or Streett conditions, we can in fact accept all ω-regular languages using deterministic automata. So, why do we bother about complementing non-deterministic Büchi automata?

The reason is that the natural translation of logical questions into automata necessarily introduces non-determinism. For instance, when we constructed the automaton (A_{φ}, G_{φ}) corresponding to an S1S formula φ in Section 2, non-determinism was unavoidable in the inductive step for handling existential quantification. This non-determinism arises regardless of what type of acceptance condition we choose to work with. Surprisingly, determinizing Muller or Rabin automata directly is no easier than first converting them to Büchi automata and then applying Safra’s construction [Sa88].

Arguably, for our purposes it should suffice to complement Büchi automata— determinization is a stronger construction which yields complementation as a corollary. In fact, Klarlund [Kl91] has shown that it is possible to directly complement non-deterministic Büchi automata without determinizing them and without sacrificing the optimal 2^{O(n log n)} bound achieved by Safra’s construction. However, there are applications where determinization is crucial—for instance, in the game-theoretic analysis of automata on infinite trees [GH82].

5 Discussion

Our main focus in this survey has been in describing how Büchi automata can be used to settle decision problems in logic. On the way, we have proved some simple results about ω-regular languages. There has also been a lot of work on the algebraic and topological aspects of ω-regular languages which we have not even touched on. A detailed introduction can be found in the survey [Th90].

As mentioned in the Introduction, Meyer showed in [Me75] that the decision procedure for S1S has a non-elementary complexity. A formula of length n may generate an automaton with 2^{2^{^{···}^{2}}} states, where the tower of exponentials is of height n. In other words, the size of the automaton cannot be bounded by a function of constant exponential height. This result appears to make it impossible to use this elegant theory in a practical setting for verifying properties of programs.

However, for temporal logics, it turns out that there are direct ways to construct a Büchi automaton (A_{φ}, G_{φ}) recognizing L_{φ} for a temporal logic formula φ, such that the size of A_{φ} is exponential in the length of the formula [VW86]. As shown in [VW86], Büchi automata also provide a clean solution to the model-checking problem for finite state systems. The model checking problem is the following—given a finite-state program P and a temporal logic formula φ, do all the computations of P satisfy φ?

Rabin showed that Büchi’s decidability result for S1S could be extended to the logic S2S, the monadic second order theory of the infinite binary tree [Ra69]. The logic S2S is very powerful—for instance, it is powerful enough to embed the logic SωS, the monadic second order theory of the infinite countably branching tree.

Rabin’s results are proved by extending the techniques developed for automata on infinite words to automata operating on infinite trees. These extensions are highly nontrivial—especially the result that automata on infinite trees are closed under complementation. A number of attempts have been made to simplify Rabin’s difficult proof. A novel and fruitful approach has been to analyze these automata in terms of infinite games [GH82].

Recently, there has been a lot of work on lifting the theory of Büchi automata and ωregular languages to the setting of concurrent programs [GP92, EM93]. When dealing with concurrent programs, it is often advantageous to regard the runs of the system as partial orders rather than as sequences. Two actions in such a run are unordered if they occur independently. A sequential description of a concurrent program will generate a number of equivalent interleavings for each partially ordered run. To verify properties of a concurrent program in terms of such a sequential description, we have to check all these equivalent interleavings when, in principle, it should suffice to check one representative interleaving for each partially ordered computation. By directly working with infinite labelled partial orders rather than infinite sequences, we can avoid some of this duplication of effort. A challenging open problem is to extend the work of [GP92, EM93] to branching structures with concurrency, corresponding to the case of infinite trees for sequential systems.

Acknowledgments I thank Deepak D’Souza, P. Madhusudan, Samik Sengupta and Barbara Sprick for patiently listening to me when I lectured on this material. Their questions and observations in class have greatly influenced the manner in which I have organized the material in this tutorial. In particular, Example 4.5 is due to Madhu and Barbara.

References

[AHU74] A.V. Aho, J.E. Hopcroft and J.D. Ullman: The Design and Analysis of Algorithms, Addison-Wesley, Reading (1974).

[Bü60] J.R. Büchi: On a decision method in restricted second order arithmetic, Z. Math. Logik Grundlag. Math, 6 (1960) 66–92

[EM93] W. Ebinger and A. Muscholl: Logical Definability on Infinite Traces, Proc. ICALP ’93, LNCS 700 (1993) 335–346.

[Em90] E.A. Emerson: Temporal and modal logic, in: J. van Leeuwen ed., Handbook of Theoretical Computer Science: Volume B, North-Holland, Amsterdam (1990) 995–1072.

[GP92] P. Gastin and A. Petit: Asynchronous Cellular Automata for Infinite Traces, Proc. ICALP ’92, LNCS 623 (1992) 583–594.

[GH82] Y. Gurevich and L. Harrington: Trees, automata and games, Proc 14th ACM STOC, (1982) 60–65.

[Kl91] N. Klarlund: Progress measures for complementation of ω-automata with applications to temporal logic, Proc. 32nd IEEE FOCS (1991) 358–367.

[Mc66] R. McNaughton: Testing and generating infinite sequences by a finite automaton, Inform. Control, 9 (1966) 521–530.

[Me75] A. Meyer: Weak monadic second order theory of successor is not elementary recursive, Proc. Logic Colloquium, Lecture Notes in Mathematics 453 (1975) 132–154.

[Mi88] M. Michel: Complementation is more difficult with automata on infinite words, Manuscript (1988).

[Mu63] D.E. Muller: Infinite sequences an finite machines, Proc. 4th IEEE Symp. on Switching Circuit Theory and Logical Design, (1963) 3–16.

[Pn77] A. Pnueli: The temporal logic of programs, Proc. 18th IEEE FOCS (1977) 46–57.

[Ra69] M.O. Rabin: Decidability of second order theories and automata on infinite trees, Trans. AMS, 141(1969) 1–37.

[Sa88] S. Safra: On the complexity of ω-automata, Proc. 29th IEEE FOCS, (1988) 319–327.

[SV89] S. Safra and M. Vardi: On ω-automata and temporal logic, Proc. 21st ACM STOC, (1989) 127–137.

[SVW87] A.P. Sistla, M. Vardi and P. Wolper: The complementation problem for ω-automata with applications to temporal logic, Theoret. Comput. Sci., 49 (1987) 217–237.

[St88] R. Streett: Propositional dynamic logic of looping and converse is elementarily decidable, Inform. Control, 48 (1981) 261–283.

[Th90] W. Thomas: Automata on infinite objects, in J. van Leeuwen (ed.), Handbook of Theoretical Computer Science, Volume B, North-Holland, Amsterdam (1990) 133–191.

[VW86] M. Vardi and P. Wolper: An automata theoretic approach to automatic program verification, Proc. 1st IEEE LICS, (1986) 332–345.

[VW94] M. Vardi and P. Wolper: Reasoning about infinite computations, Inform. Comput., 115(1) (1994) 1–37.