Loading...

Summer Research Fellowship Programme of India's Science Academies

An introduction to finite automata theory

Nabarun Deka

Indian Institute of Science, CV Raman Road, Bengaluru 560012

Abstract

In this report, we begin by familiarising ourselves with the theory of finite automata. We study a formal definition of finite automata and the notion of languages being recognized by them. We then look at the concept of 'Nondeterminism', formalise a 'Nondeterministic' finite automata and prove the equivalence of 'Deterministic' and 'Nondeterministic' finite automaton. We then study the problem of trying to describe the languages recognized by finite automata leading to defining 'Regular expressions' and then prove the equivalence of regular expressions and finite Automata. We also look at the problem of constructing minimal finite automata for a given language and study the 'Myhill-Nerode Relations' and the 'Myhill-Nerode' Theorem. We then look at a necessary condition for a language to be recognizable by a finite automaton through the 'Pumping Lemma'. With a familiarity of Finite Automata, we look at a specific problem. We look at the question of defining finite automata that accepts infinite strings as input. We study Büchi's construction of automata on infinite words. Through an example, we study the non-equivalence of 'deterministic' and 'non-deterministic' Büchi automata. We study the characterisation of languages recognized by Büchi automata. We then look at the 'monadic second order logic of one successor', abbreviated as S1S and look at some examples of formulas in S1S. Finally, we study the satisfiability problem in S1S, and Büchi's solution using Büchi automata

Keywords: deterministic finite automata, non-deterministic finite automata, regular expressions, Myhill-Nerode theorem, pumping lemma, Büchi automata

Abbreviations

The following abbreviations will be used in this report

Abbreviations
DFADeterministic Finite Automata
NFANon-Deterministic Finite Automata
 S1S Monadic second order logic of one successor
 MNMyhill-Nerode 

Notation

Small letters a,b,c will be used to denote letters of an alphabet.

Small letters u,v,w will be used to denote finite length words.

Greek letters α,β,γ will be used to denote infinite length words.

Capital letters A,B,C will be used to denote Languages

The following report is written by Nabarun Deka, Registration Number: MATS384 as part of the IAS Summer Fellowship Program 2019, under the guidance of Dr. Aiswarya Cyriac, CMI.

FINITE AUTOMATA: A FORMAL DEFINITION

A Finite Automata is defined as a quintuple (Q,Σ,δ,q0,F)(Q, \Sigma, \delta, q_{0}, F)where :

1. QQ is a finite set called the set of states

2. Σ\Sigma is a finite set called the Alphabet

3. δ:Q×ΣQ\delta : Q \times \Sigma \rightarrow Qis a function called the Transition Function

4. q0Qq_{0} \in Q is a state called the Initial State

5. FQF \subseteq Qis called the set of Accept States

The input to a Finite Automaton (Q,Σ,δ,q0,F)(Q, \Sigma, \delta, q_{0}, F) are words from the alphabet Σ\Sigma. A Finite Automaton always begins in the initial state. As it reads a word (call it ww), it moves from one state to another as given by the transition function. The state of the automaton after reading the entire input is called the final state. If the final state is an accept state, we say that the automaton accepts the word ww. The set of all words accepted by an automaton is said to be the Language recognized by the automaton. We formalise this notion of acceptance of a word as follows: Let M=(Q,Σ,δ,q0,F)M = (Q, \Sigma, \delta, q_{0}, F) be a finite automaton, and let w=a1a2anw = a_1a_2\dots a_n be a word where each aia_ibelongs to the alphabet Σ\Sigma. Then, MM accepts ww if there exist a sequence of states r0,r1,,rnr_0,r_1,\dots,r_n in QQ (such a sequence of states is called an accepting run of the word ww on the automaton MM) such that:

1. r0=q0r_0 = q_0

2. ri+1=δ(ri,ai+1)r_{i+1} = \delta(r_i,a_{i+1}) for i=0,1,,n1i = 0,1,\dots,n-1

3. rnFr_n \in F

It is easier to represent Finite Automata pictorially than as a quintuple. We shall look at this through a few examples.

Example 1: Consider the language, L1L_1, of all even numbers expressed in the binary number system. We will build a finite state automaton that will recognize this language (It reads the string from most significant digit to least significant one). We observe that all even numbers end with the digit 0 in the binary number system, while all odd numbers end with the digit 1. Thus, we can build an automaton that recognizes this language by using two states to keep track of the last digit read by the automaton. As a convention, we will take the empty string to be an even number. The automaton is shown in the figure below.

fig1.JPG
    Automaton that recognizes  L1L_1

    Example 2: Consider the language, L2L_2, over the alphabet {0,1}\{0,1\} that contains all strings that contain the substring 001001. The idea behind this construction is to check for the substring 001001 while reading the string, and then accepting if we find it. The automaton that accepts this language is shown below.

    fig2.JPG
      Automaton that recognizes  L2L_2

      A language, LL, is said to be a Regular Language if it is recognized by some finite automaton.

      NON-DETERMINISM

      Observe that, given a word ww, the automaton given in Section 1 follows a unique run while reading the word. An automaton that has a unique run on a word is called a deterministic automaton. We can also have automatons that have multiple runs on a given word. Such automata can be constructed by giving multiple transitions from a state on a given input. In addition to this, nondeterministic finite automata also have empty transitions (denoted by ϵ\epsilon). An empty transition is one where the automaton can make a transition from one state to another without reading any input. Formally, a nondeteministic finite automaton is defined as a quintuple (Q,Σ,Δ,q0,F)(Q,\Sigma,\Delta,q_0,F) where

      1. QQ is the set of states

      2. Σ\Sigma is the Alphabet

      3. ΔQ×Σ{ϵ}×Q\Delta \subseteq Q \times \Sigma \cup \{\epsilon\} \times Qis a relation called the Transition Relation

      4. q0Qq_{0} \in Q is a state called the Initial State

      5. FQF \subseteq Qis called the set of Accept States

      Observe that a NFA has a transition relation instead of a function i.e given a state qq and input letter aa, the machine can go to state qq' iff (q,a,q)Δ(q,a,q') \in \Delta. This relation introduces the non-determinism in the machine. Similar to a DFA, we define an accepting run of a word w=a1a2anw = a_1a_2\dots a_n on a NFA as a sequence of states r0,r1,,rmr_0,r_1,\dots,r_m where mnm \geq n (the run can be much larger than the length of the input because of empty transitions) such that

      1. r0=q0r_0 = q_0

      2. (ri,bi+1,ri+1)Δ(r_i,b_{i+1},r_{i+1}) \in \Delta for i=0,1,,m1i = 0,1,\dots,m-1

      3. b1b2bm=a1a2an=wb_1 b_2 \cdots b_m = a_1 a_2 \cdots a_n = w

      4. rmFr_m \in F

      We say that a NFA accepts a word ww if there exists atleast one accepting run of ww i.e. atleast one run ends on an accept state. Note that, if at any point a run encounters a state-letter pair that has no defined transition, the run ends there and becomes invalid (because it hasnt read the complete input).

      Example 3: Consider the language L3L_3 of all strings over {0,1}\{0,1\} that have a 11 at the third position from the end of the string. We can construct a NFA to accept this language by guessing that each 11 we encounter is the third one from the end, and then checking whether this is true. The automaton that recognizes this language is given below

      fig3.JPG
        Automaton that accepts  L3L_3

        Equivalence of Deterministic and Non-deterministic Automata

        Since Non-deterministic automata are able to simulate multiple runs simultaneously, one might expect them to be more powerful than Deterministic Automata, i.e. NFA can recognize languages that cannot be recognized by DFA. Surprisingly, this turns out to be false. We have the following theorem:

        Theorem: Every NFA has an equivalent DFA

        Proof: Let N=(Q,Σ,Δ,q0,F)N = (Q,\Sigma,\Delta, q_0,F) be a NFA. We construct a DFA, MM, that is equivalent to NNas follows :

        M=(Q,Σ,δ,q0,F) M = (Q',\Sigma,\delta,q_0',F')  where

        ​1. Q=P(Q)Q' = P(Q) , the set of all subsets of QQ

        2. To define the transition function, we first define δ(q,a)\delta'(q,a) as the set of all states reachable from qq on the letter aa in the NFA i.e δ(q,a)={qQ(q,a,q)Δ} \delta'(q,a) = \{q' \in Q \mid (q,a,q') \in \Delta\} . Now we define the transition function for MM as

        δ(R,a)=qR δ(q,a)\delta(R,a) = \bigcup_{q \in R}  \delta'(q,a)

        3. The start state is the state corresponding to the singleton set {q0}\{q_0\}

        4. The set of final states consists of all the subsets of QQthat contain atleast one final state from FF i.e F={RP(Q)RFϕ}F' = \{R \in P(Q) \mid R \cap F \neq \phi \}

        ​The machine MM keeps track of all the states the NFA is in after reading the input. Hence, if after reading the input MM is in a state from FF', then there was some run in NN that ended in a final state, and hence, the input is accepted by NN. It is easy to see that these two automata are equivalent.

        REGULAR EXPRESSIONS

        We now try to give a characterisation of the regular languages. For this purpose, we define three operations on languages. Let AA and BB be two languages. We define :

        1. Union : AB={xxA or xB}A \cup B = \{x \mid x \in A  or  x \in B \}

        2. Concatenation : AB={xyxA and yB}AB = \{xy \mid x \in A  and  y\in B \}

        3. Iteration : A={x1x2xkk0;xiA  1ik}A^* = \{ x_1x_2\dots x_k \mid k \geq 0; x_i \in A  \forall  1 \leq i \leq k \} (Note that this also contains the empty string)

        Now, we define regular expressions inductively as follows:

        1. The expression aa is a regular expression ( aa is a letter of some alphabet Σ\Sigma)

        2. ϵ\epsilon which denotes the empty string, is a regular expression

        3. \emptysetwhich denotes the empty language, is a regular expression

        4. If L1L_1 and L2L_2 are regular expressions, then

        4.1 L1L2L_1 \cup L_2 is a regular expression

        4.2 L1L2L_1L_2 is a regular expression

        4.2 L1 L_1^*  is a regular expression

        Examples :

        1. (01)(0 \cup 1)^* is a regular expression that describes the language of all strings over the alphabet {0,1}\{0,1\}

        2. a(ab)ba(a \cup b)^*b is a regular expression that describes all strings starting with an aa and ending with a bb

        Now, we will prove that regular languages can be characterised using regular expressions. This includes two parts.

        Regular Expressions describe Regular Languages

        Theorem : If RR is a regular expression, then, it describes a Regular Language

        Proof : We prove this by induction on the structure of Regular Expressions. The base cases are the singleton letter, the empty string, and the null language.

        1. Singleton letter : The expression R=aR = a describes the language consisting of the sinlge letter string aa i.e L(R)={a}L(R) = \{a\}. This language is regular because it can be recognized by the following two state automaton

        2. Empty String : The expression R=ϵR= \epsilon describes the language consisting of only the empty string i.e L(R)={ϵ}L(R) = \{\epsilon\}. This is also a regular language as it can be recognized by the following one state automaton

        3. Null language: The expression R=R = \emptysetdescribes the empty language, i.e the language that has no strings. This language is also regular as it can be recognized by the following single state automaton

        This proves the base cases. Now, for the inductive step, we show that regular languages are closed under the regular operations, i.e. union, concatenation and iteration of regular languages are also regular.

        Let R1R_1 and R2R_2 be regular expressions and let their corresponding regular languages be L1L_1 and L2L_2respectively (this is true from the induction hypothesis). Let the automata recognizing L1L_1 and L2L_2 be M1=(Q1,Σ1,δ1,q1,F1)M_1 = (Q_1, \Sigma_1, \delta_1, q_1, F_1) and M2=(Q2,Σ2,δ2,q2,F2)M_2 = (Q_2, \Sigma_2, \delta_2, q_2, F_2) respectively.

        1. Union: We construct a NFA that recognizes the union of these two languages by creating a new start state that has empty transitions to the start states of both M1M_1 and M2M_2. We keep M1M_1 and M2M_2 as they are, and make the set of final states the union of their final states. This NFA runs the word on both M1M_1 and M2M_2 simultaneously, and accepts it if it reaches an accept state on any one of them. Hence, it accepts the union of the two languages. Thus, we proved that regular languages are closed under union.

        2. Concatenation: We construct a NFA that recognizes L1L2L_1L_2 by taking M1M_1 and putting empty transitions from the final states of M1M_1 to the start states of M2M_2. The start state of this new NFA is the start state of M1M_1 and the final states are the final states of M2M_2. It is easy to see that this NFA accepts the concatenation of the two languages.

        3. Iteration: We construct a NFA that recognizes L1L_1^*by taking M1M_1 and putting empty transitions from its final states to its start state. However, this construction has one problem, it does not accept the empty string unless the start state of M1M_1is also a final state, while L1L_1^* includes the empty string. To correct this, we create a new start state, put empty transitions from all the final states to this state, and empty transitions from this state to the start state. It is easy to see that this NFA accepts L1L_1^*. Thus, given any regular expression, we can construct an automaton to accept the language described by it.

        Regular Languages are described by Regular Expressions

        Theorem: If LL is a regular language, then it is described by a regular expression

        Proof: Let M=(Q,Σ,Δ,q0,F)M = (Q,\Sigma,\Delta,q_0,F)be the automaton that recognizes LL. Given a subset XQX \subseteq Qand states u,vQu,v \in Q, we show how to construct a regular expression RuvXR_{uv}^X representing the set of all strings wwsuch that there is a path from uuto vv in MM of the string ww and all the states in that path lie in XX(with the possible exception of uuand vv). We construct this by induction on the size of XX. qq

        Base Case : X=X = \emptyset

        Let a1,a2,aka_1,a_2,\dots a_kbe the letters in Σ{ϵ}\Sigma \cup \{\epsilon \}such that vΔ(u,ai)v \in \Delta(u,a_i) for all ii. Then, define

        RuvX:={a1a2akk1k=0R_{uv}^X :=\begin{cases}a_1\cup a_2 \cup \dots \cup a_k & k\geq 1 \\\emptyset & k=0\end{cases}

        Induction Step: For non-empty XX, choose any state qXq \in X. We construct RuvXR_{uv}^X as

        RuvX:=RuvX{q}RuqX{q}(RqqX{q})RqvX{q}R_{uv}^X := R_{uv}^{X - \{q\}} \cup R_{uq}^{X-\{q\}}(R_{qq}^{X-\{q\}})^*R_{qv}^{X-\{q\}}

        By the induction hypothesis, each of RuvX{q}R_{uv}^{X-\{q\}}, RuqX{q}R_{uq}^{X-\{q\}}, RqqX{q}R_{qq}^{X-\{q\}} and RqvX{q}R_{qv}^{X-\{q\}} exist. To justify this expression, note that any path from uu to vv lying in XX will either never visit qq, and hence the expression RuvX{q}R_{uv}^{X-\{q\}}, or it visits qq for the first time, hence the expression RuqX{q}R_{uq}^{X-\{q\}}, and then loops from qqback to itself, hence the expression RqqX{q}R_{qq}^{X-\{q\}} and then reaches vv from qq and hence the expression RqvX{q}R_{qv}^{X-\{q\}}

        The regular expression for LL is

        R=fFRq0fQR = \bigcup_{f \in F} R_{q_0f}^Q

        Thus, we have proved that Regular expressions characterise all the regular languages.

        MYHILL - NERODE THEOREM

        Myhill - Nerode Relation: Let LΣL \subseteq \Sigma^* be any language. An equivalence realtion, \equiv on Σ\Sigma^*is said to be a Myhill - Nerode relation induced by LL if it satisfies the following properties:

        1. Right congruence: xy     (wΣ)(xwyw)x \equiv y \implies \forall  (w \in \Sigma^*) (xw \equiv yw)

        2. Refinement: xy    (xL    yL)x \equiv y \implies (x \in L \iff y \in L)

        Theorem: Every regular language LL induces a Myhill-Nerode relation (MN relation) on Σ\Sigma^*that has finitely many equivalence classes.​

        Proof: Let M=(Q,Σ,δ,q0,F)M = (Q,\Sigma,\delta,q_0,F) be the automaton recognizing LL. For any state qq and word ww define δ^(q,w)\hat{\delta}(q,w) inductively on the length of ww as

        δ^(q,ϵ)=q\hat{\delta}(q,\epsilon) = q

        δ^(q,wa)=δ(δ^(q,w),a)\hat{\delta}(q,wa) = \delta(\hat{\delta}(q,w),a)

        This denotes the state of the automaton starting at state qq and reading the word ww.

        Now, define L\equiv_Lon Σ\Sigma^* as

        xLy    δ^(q0,x)=δ^(q0,y)x \equiv_L y \iff \hat{\delta}(q_0,x) = \hat{\delta}(q_0,y)

        It is easy to see that this is an equivalence relation. Also, for any wΣw \in \Sigma^*, if xLyx \equiv_L y, then

        δ^(q0,xw)=δ^(δ^(q0,x),w)= δ^(δ^(q0,y),w)= δ^(q0,yw)    xwLyw\hat{\delta}(q_0,xw) = \hat{\delta}(\hat{\delta}(q_0,x),w) = \hat{\delta}(\hat{\delta}(q_0,y),w) = \hat{\delta}(q_0,yw) \implies xw \equiv_L yw

        Hence, it is right congruent. Also,

        xLy    δ^(q0,x)= δ^(q0,y)    (δ^(q0,x)F     δ^(q0,y)F)    (xL    yL)x \equiv_L y \implies \hat{\delta}(q_0,x) = \hat{\delta}(q_0,y) \implies (\hat{\delta}(q_0,x) \in F \iff \hat{\delta}(q_0,y) \in F) \implies (x \in L \iff y \in L)

        Hence, it is a MN relation. Also, it is clear from the definition that the number of equivalence classes is equal to the number of states of MM which is finite.

        Theorem: Let L\equiv_L be a MN relation for any language LΣL \subseteq \Sigma^*. If L\equiv_L is of finite index, i.e. it has finitely many equivalence classes, then LLis regular.

        Proof: We construct an automaton M=(Q,Σ,δ,q0,F)M = (Q,\Sigma,\delta,q_0,F) for LL as follows:

        Q={[x]xΣ}Q = \{ [x] \mid x \in \Sigma^*\} where [x][x] is the equivalence class of xx. Since there are finitely many equivalence classes, this set is finite.

        δ([x],a)=[xa]\delta([x],a) = [xa]. This is well defined because of the right congruence of MN relations.

        q0=[ϵ]q_0 = [\epsilon]

        F={[x] xL}F = \{[x] \mid  x\in L\}

        Claim: δ^([x],w)=[xw]\hat{\delta}([x],w) = [xw]

        We prove this by induction on length of ww.

        ​Base case: δ^([x],ϵ)=[xϵ]=[x]\hat{\delta}([x],\epsilon) = [x\epsilon] = [x] (By definition)​

        Induction step: δ^([x],wa)=δ(δ^([x],w),a)=δ([xw],a)=[xwa]\hat{\delta}([x],wa) = \delta(\hat{\delta}([x],w),a) = \delta([xw],a) = [xwa] (follows from definitions of δ\delta and δ^\hat{\delta}.

        Hence, wL(M)    δ^([ϵ],w)F    [w]F    wLw \in L(M) \iff \hat{\delta}([\epsilon],w) \in F \iff [w] \in F \iff w \in L

        Hence, MM is a DFA for LL

        Now, with these two results, we are ready to state the Myhill Nerode Theorem.

        For any language LΣL \subseteq \Sigma^*, define the canonical MN relation, L\approx_L on Σ\Sigma^* as

        xLy    (w)(xwL    ywL)x \approx_L y \iff (\forall w) (xw \in L \iff yw \in L)

        It is easy to see that this is a MN relation. Further more, this is the coarsest MN relation for LL, i.e any other MN relation for LL refines this.

        Lemma: Let L\equiv_L be a MN relation for LL. Then, L\equiv_Lrefines L\approx_L.

        Proof: Pick any x,yx,ysuch that xLyx \equiv_L y. Now, assume that x̸Lyx \not\approx_L y. This means that there exists some ww such that xwLxw \in L but ywLyw \notin L. This implies that xw̸Lywxw \not\equiv_L yw(since L\equiv_Lsatisfies the refinement property). But this contradits the right congruence of L\equiv_L. Hence, our assumption was wrong.

        Thus, xLy    xLyx \equiv_L y \implies x \approx_L y.

        Thus, any MN relation refines the canonical MN relation.

        Myhill - Nerode Theorem: A language LLis regular iff ​ L\approx_L is of finite index.

        Proof: If L\approx_L is of finite index, since L\approx_L is a MN relation, by our previous theorem, LLis regular.

        If LL is regular, it has some MN relation of finite index. By our previos result, this refines L\approx_L. Hence, index of L\approx_Lis also finite. ​

        PUMPING LEMMA FOR REGULAR LANGUAGES

        The pumping lemma gives a necessary condition for a language to be regular. The lemma is given below

        Pumping Lemma: If LLis a regular language, then there exists a natural number, p>0p \gt 0 called the pumping length such that for any word wLw \in Lof length greater than pp, wwcan be written as xyzwxyzw'such that

        1. xyz=p|xyz| = p

        2. y>0|y| \gt 0

        3. xyizwL  i0xy^izw' \in L  \forall  i \geq 0

        This means that there is some segment of the word that can be pumped to get more words in the language.

        Proof: Since LLis regular, there is a deterministic finite automaton that recognizees it. Let the number of states in this automaton be nn. The pumping length p=np = n. Now, consider any word wwof length greater than pp. Let xyzxyz be the first pp letters of the word. Consider the run of this word on the automaton. After the first ppletters of the word are read, the run consists of n+1n+1states. Since there are only nnstates in the machine, by the pigeon hole principle, a state must repeat in the run. Let the segement of the run that starts and ends at the same state be yy. Then wwis of the form xyzwxyzw'and since the automaton is at the same state before starting to read yyand after finishing reading it, it is at the same state after reading yiy^i for all i0i \geq 0. Hence, xyizwLxy^izw' \in L for all i0i \geq 0.​

        Example: The language L={anbnn0}L = \{ a^nb^n \mid n \geq 0\} is not a regular language.

        Proof: Assume LL was a regular language. Then by the pumping lemma, there exists a pumping length pp for LL. Consider the string apbpLa^pb^p \in L. If we write it as xyzw xyzw' such that xyzp|xyz| \leq p, then xyz=apxyz = a^p and y=am y = a^m for some 0<mp0 \lt m \leq p. Taking i=2i = 2, we see that xy2zw=ap+mbpLxy^2zw' = a^{p+m}b^p \notin L. This contradicts the pumping lemma. Hence, our assumption was wrong, and LL is not regular.

        BÜCHI AUTOMATA

        Now that we are familiar with finite state automata, we study a particular type of automata that was developed to solve decidability problems in Second Order Logic. A Büchi automaton is an automaton that runs on strings of infinite length. Since it runs on infnite strings, we cannot use the standard definition of acceptance that we use for automaton over finite strings. We now formally define a Büchi automaton.

        Infinite String: An infinite string over an alphabet Σ\Sigma is a function α:NΣ\alpha : \mathbb{N} \rightarrow \Sigma where α[i]\alpha[i] denotes the letter at the iith position.

        A Büchi automaton is a Finite state automaton A=(Q,Σ,δ,q0,F)A = (Q,\Sigma, \delta, q_0, F) that runs on infinite strings. To define acceptance condition for a Büchi automaton, we first look at the run of an infinite word on an automaton. Let ρ\rhobe the run of some word α\alpha on the automaton. Since it is an infinite word, and the automaton has finitely many states, some states must repeat infinitely often on the run ρ\rho. We denote this set by inf(ρ)inf(\rho). Now, the automaton is said to accept α\alpha if the run of α\alpha on AA goes to some final state infinitely often i.e inf(ρ)Fϕinf(\rho) \cap F \neq \phi.

        We will denote a language of finite words over an alphabet Σ\Sigma by LΣL \subseteq \Sigma^* and a language of infinite words by LΣωL \subseteq \Sigma^\omega.

        Example: Let LL be the language of all infinite strings over {a,b}\{a,b\} that have infinitely many aa's. The Büchi automaton recognizing this lagnuage is given below.

        fig4.JPG
          Büchi automaton that recognizes  LL

          Example: Let LL'be the complement of the above language, that is language containing infinite strings that have only finitely many occurences of aa. The Büchi automaton recognizing this language is given below. Note that it is a non-deterministic automaton.

          fig5.JPG
            Büchi automaton that recognizes  LL'

            NON - DETERMINISTIC AND DETERMINISTIC BÜCHI AUTOMATA ARE NOT EQUIVALENT

            Unlike automata over finite words, non-deterministic Büchi automata are more powerful than deterministic ones. To prove this, we will first characterise the languages recognized by deterministic Büchi automata.

            Limit Language: Let UΣU \subseteq \Sigma^*be any langugae of finite strings. The limit language of UUis a language over infinite strings defined as

            lim(U)={αΣωωnN,  α[0n]U}lim(U) = \{\alpha \in \Sigma^\omega \mid \exists^\omega n \in \mathbb{N},   \alpha[0\dots n] \in U\}

            So, a word belongs to lim(U)lim(U) iff it has infinitely many prefixes in UU.

            Theorem: A language LΣω L \subseteq \Sigma^\omega is recognized by a deterministic Büchi automaton iff LLis of the form lim(U)lim(U)for some regular language UΣU \subseteq \Sigma^*.

            Proof: Let UU be a regular language of finite length words. Then, it is recognized by a deterministic automaton A=(Q,Σ,δ,q0,F)A = (Q,\Sigma,\delta,q_0,F). If we interpret this automaton as a Büchi automaton, it is clear that it will accept lim(U)lim(U).

            Conversely, if LΣωL\subseteq \Sigma^\omegais recognized by a deterministic Büchi automaton ​ A=(Q,Σ,δ,q0,F)A = (Q,\Sigma,\delta,q_0,F), treating this as a DFA over finite words, it accepts some regular language UU. It is easy to see that L=lim(U)L = lim(U).

            Using this theorem, we will show that LL'in our example above, cannot be recognized by a deterministic Büchi automaton. Assume otherwise. Then, by our theorem, L=lim(U)L' = lim(U) for some regular language UΣU \subseteq \Sigma^*. Now, bωLb^\omega \in L'. Thus, bn0Ub^{n_0} \in U for some n0n_0. Now, bn0abωLb^{n_0}ab^\omega \in L'. Thus, bn0abn1Ub^{n_0}ab^{n_1} \in Ufor some n1n_1. Continuing this process, we get an infinite set {bn0,bn0abn1,bn0abn1abn2,}\{b^{n_0},b^{n_0}ab^{n_1},b^{n_0}ab^{n_1}ab^{n_2}, \dots\} such that each of the strings in it lie in UU. Then, the infinite string bn0abn1abn2abn3b^{n_0}ab^{n_1}ab^{n_2}ab^{n_3}\dots lies in L(=lim(U))L' (= lim(U)). However, the string has infintely many aa's. Contradiction. Hence, LL cannot be recognized by a deterministic Büchi automaton.

            CLOSURE PROPERTIES OF BÜCHI RECOGNIZABLE LANGUAGES

            A language recognized by a Büchi automata is called a Büchi recognizable language or a ω-regular language. We now study the closure of Büchi automata under the operations of union, intersection, projection and complementation.

            1. Union: Let L1,L2L_1,L_2be two Büchi recognizable languages. Then, L1L2L_1\cup L_2is also Büchi recognizable. Let A1,A2A_1,A_2be the Büchi automata recognizing L1,L2L_1,L_2respectively. We create a non deterministic Büchi automaton AA whose start states are the start states of A1 A_1 and A2A_2, and accept states are the union of accept states of A1 A_1 and A2A_2. This automaton runs the word on both A1 A_1 and A2A_2 and accepts if it is accepted by either of them. Hence, it accepts the union of the two languages.

            2. Intersection: Let A1=(Q1,Σ,Δ1,S1,F1) A_1 = (Q_1,\Sigma, \Delta_1, S_1,F_1)  and A2=(Q2,Σ,Δ2,S2,F2)A_2 = (Q_2,\Sigma, \Delta_2, S_2,F_2) be the (possibly non-deterministic) automata recognizing L1,L2L_1,L_2 respectively. We construct an automaton that recognizes their intersection as follows, A=(Q,Σ,Δ,S,F)A = (Q,\Sigma,\Delta,S,F), where

            Q=Q1×Q2×{1,2}Q = Q_1\times Q_2\times \{1,2\}

            Δ\Deltais defined as:

            ((q1,q2,1),a,(q1,q2,1))Δ((q_1,q_2,1),a,(q_1',q_2',1))\in \Delta if (q1,a,q1)Δ1,(q2,a,q2)Δ,q1F1(q_1,a,q_1') \in \Delta_1, (q_2,a,q_2')\in \Delta, q_1 \notin F_1

            ((q1,q2,1),a,(q1,q2,2))Δ((q_1,q_2,1),a,(q_1',q_2',2))\in \Delta if ​ (q1,a,q1)Δ1,(q2,a,q2)Δ,q1F1(q_1,a,q_1') \in \Delta_1, (q_2,a,q_2')\in \Delta, q_1 \in F_1

            ((q1,q2,2),a,(q1,q2,2))Δ((q_1,q_2,2),a,(q_1',q_2',2))\in \Delta if ​ (q1,a,q1)Δ1,(q2,a,q2)Δ,q2F2(q_1,a,q_1') \in \Delta_1, (q_2,a,q_2')\in \Delta, q_2 \notin F_2

            ((q1,q2,2),a,(q1,q2,1))Δ((q_1,q_2,2),a,(q_1',q_2',1))\in \Delta if ​ (q1,a,q1)Δ1,(q2,a,q2)Δ,q2F2(q_1,a,q_1') \in \Delta_1, (q_2,a,q_2')\in \Delta, q_2 \in F_2

            S={(q1,q2,1)q1S1,q2S2}S = \{(q_1,q_2,1) \mid q_1 \in S_1, q_2 \in S_2 \}

            F=Q1×F2×{2}F = Q_1 \times F_2 \times \{2\}

            It is easy to verify that this automaton recognizes the intersection of the two languages.

            3. Projection: Let Σ1,Σ2\Sigma_1, \Sigma_2be two alphabets such that Σ2Σ1|\Sigma_2| \leq |\Sigma_1|. A projection map from Σ1\Sigma_1 to Σ2\Sigma_2is a surjective map​ π:Σ1Σ2\pi : \Sigma_1 \rightarrow \Sigma_2. We can extend this map to words as usual : if αΣ1ω\alpha \in \Sigma_1^\omega​, π(α)\pi(\alpha) is the word β\beta such that β(i)=π(α(i))  iN\beta(i) = \pi(\alpha(i))  \forall  i \in \mathbb{N}. Let LΣ1ωL \subseteq \Sigma^\omega_1be recognized by the Büchi automaton A=(Q,Σ1,Δ,S,F)A = (Q,\Sigma_1,\Delta,S,F), we construct an automaton A=(Q,Σ2,Δ,S,F)A' = (Q',\Sigma_2,\Delta',S',F')that recognizes π(L)\pi(L)as follows:

            Q=QQ' = Q

            (q,b,q)Δ if  aΣ1 s.t.(q,a,q)Δ;π(a)=b(q,b,q') \in \Delta'  if  \exists  a\in\Sigma_1  s.t. (q,a,q') \in \Delta; \pi(a) = b

            S=SS' = S

            F=FF' = F

            It is easy to verify that this automaton accepts the language π(L)\pi(L).

            4. Complementation: Showing that Büchi automata are closed under complementation is non-trivial, and we will devote an entire separate section for it.

            COMPLEMENTING BÜCHI AUTOMATA

            Let A=(Q,Σ,Δ,S,F)A = (Q,\Sigma,\Delta,S,F)be a non-deterministic Büchi automaton that recognizes LΣωL \subseteq \Sigma^\omega. We define the run DAG of AAon a word αΣω\alpha \in \Sigma^\omegato be the directed acyclic graph G=(V,E)G = (V,E)where

            1. V=l0(Ql×{l}) where Q0=S and Ql+1=qQl,(q,α(l),q)Δ{q} V = \bigcup_{l\geq0}(Q_l\times \{l\})  where  Q_0 = S  and  Q_{l+1} = \bigcup_{q\in Q_l,(q,\alpha(l),q')\in\Delta}\{q'\} 

            2. E={(q,l,q,l+1)(q,α(l),q)Δ;l0}E = \{ (\langle q,l\rangle,\langle q',l+1\rangle) \mid (q,\alpha(l),q')\in \Delta;l\geq0\}

            A path in a run DAG is accepting iff it visits FFinfinitely often. The automaton AA accepts α\alphaif some path in the run DAG is accepting.

            Now, we define a ranking for the run DAG as follows:

            A ranking for GGis a function f:V{0,1,2,,2.Q}f : V \rightarrow \{0,1,2,\dots,2.|Q|\} such that

            1. for all s,lV\langle s,l \rangle \in V, if f(s,l)f(\langle s,l \rangle) is odd, then sFs \notin F

            2. for all (s,l,s,l)E,f(s,l)f(s,l)( \langle s,l \rangle , \langle s',l' \rangle ) \in E, f(\langle s',l' \rangle) \leq f(\langle s,l \rangle)

            A ranking is called odd iff for all paths s0,l0,s1,l1, \langle s_0,l_0 \rangle,\langle s_1,l_1 \rangle,\dots in GG, there is a i0i \geq 0 such that f(si,li)f(\langle s_i,l_i \rangle) is odd and for all j>i,  f(sj,lj)=f(si,li)j \gt i,   f(\langle s_j,l_j \rangle) = f(\langle s_i,l_i \rangle)

            Lemma 1: If there exists an odd ranking for GG, then AA does not accept α\alpha

            Proof: In an odd ranking, every path eventually gets trapped in an odd rank. If some vertex s,l\langle s,l \rangleis odd, then sFs \notin F. Hence, all paths visit FF only finitely many times.

            Let GG' be a subgraph of GG. We call a vertex s,l\langle s,l \rangle

            1. Safe in GG'if for all vertices s,l\langle s',l' \ranglereachable from s,l\langle s,l \rangle, sFs' \notin F

            2. Endangered in GG' if only finitely many vertices are reachable from it.

            We define a sequence of DAG's G0G1G2G_0 \supseteq G_1 \supseteq G_2 \supseteq \dotsinductively as follows

            1. G0=GG_0 = G

            2. G2i+1=G2i{s,ls,l is endangered in G2i}G_{2i + 1} = G_{2i} \setminus \{\langle s,l \rangle \mid \langle s,l \rangle  is  endangered  in  G_{2i}\}

            3. G2i+2=G2i+1{s,ls,l is safe in G2i} G_{2i + 2} = G_{2i + 1} \setminus \{\langle s,l \rangle \mid \langle s,l \rangle  is  safe  in  G_{2i} \} 

            Lemma 2: If AA does not accept α\alpha, then the following holds: for every i0i \geq 0, there exists an lil_i such that for all jlij \geq l_i, at most Qi|Q| - i vertices of the form _,j\langle \_,j \rangle are in G2iG_{2i}

            Proof: We prove by induction on ii.

            Base case : i=0i = 0 is trivial.

            Inductive case: Assume truth for 0,1,2,,i0,1,2,\dots ,i.

            Case G2iG_{2i}is finite: then G2(i+1)G_{2(i+1)} is empty.

            Case G2iG_{2i} is infinite:

            - There must exist a safe vertex s,l\langle s,l \rangle in G2i+1G_{2i+1}

            - ​We choose li+1=ll_{i+1} = l

            - We prove that for all jlj \geq l, there are atmost Q(i+1)|Q| - (i+1)vertices of the form _,j\langle \_,j \rangle in G2i+2G_{2i + 2}:

            1. s,lG2i+1\langle s,l \rangle \in G_{2i+1}, thus, it is not endangered in G2iG_{2i}. Hence, there are infintely many verties reachable from s,l\langle s,l \rangle in G2iG_{2i}.

            2. By König's lemma, there exists an infinte path p=s,l,s1,l+1,p = \langle s,l \rangle, \langle s_1,l+1 \rangle,\dots in G2iG_{2i} and no vertex in this path is endangered in G2iG_{2i}. Thus, ppis in G2i+1G_{2i + 1}

            3. All vertices in pp are safe in G2i+1G_{2i+1}. Hence, none of the vertices of pp are in G2i+2G_{2i+2}.

            Hence Proved.

            Lemma 3: If AA does not accept α\alpha, then there exists an odd ranking for GG.

            Proof: We define f(s,l)=2if(\langle s,l \rangle) = 2iif (s,l) (\langle s,l \rangle) is endangered in G2iG_{2i} and ​ f(s,l)=2i+1f(\langle s,l \rangle) = 2i+1if (s,l) (\langle s,l \rangle) is safe in G2iG_{2i}.

            ff is a ranking

            By Lemma 2, GjG_jis empty for j>2.Qj \gt 2.|Q|. Hence, f:V{0,1,2,,2.Q}f : V \rightarrow \{0,1,2,\dots,2.|Q|\}

            If s,l\langle s',l' \rangleis a succesor of s,l\langle s,l \rangle​, then f(s,l)f(s,l)f(\langle s',l' \rangle) \leq f(\langle s,l \rangle):

            Let j=f(s,l)j = f(\langle s,l \rangle). If jjis even, s,l\langle s,l \rangle​is endangerd in GjG_j and hence, either s,l\langle s',l' \rangleis not in GjG_jand hence f(s,l)<jf(\langle s',l' \rangle) \lt j; or s,l\langle s',l' \rangle is in GjG_jand safe; and hence, f(s,l)=jf(\langle s',l' \rangle) = j

            ffis an odd ranking: It is clear that for every path, there is an i0i \geq 0 such that for all jij\geq i f(sj,lj)= f(si,li)f(\langle s_j,l_j \rangle) = f(\langle s_i,l_i \rangle). Now, suppose k=f(si,li)k = f(\langle s_i,l_i \rangle)is even. Then, ​ si,li\langle s_i,l_i \rangleis endangered in GkG_k. But, since f(sj,lj)= f(si,li)f(\langle s_j,l_j \rangle) = f(\langle s_i,l_i \rangle) for all jij\geq i, all sj,lj\langle s_j,l_j \rangle are in GkG_k. This contradicts that ​ si,li\langle s_i,l_i \rangleis endangered in GkG_k. Hence, proved.

            Theorem: For every Büchi automaton AA, there exists a Büchi automaton AA' such that L(A)L(A')is the complement of L(A)L(A)

            Proof: We first define some helpful structures:

            1. A level ranking is a function g:Q{0,1,,2.Q}{}g : Q \rightarrow \{0,1,\dots,2.|Q|\} \cup \{\bot\} such that if g(q)g(q)is odd, then qFq \notin F.

            2. Let RR be the set of all level rankings

            3. A level ranking gg' covers a level ranking gg if, for all q,qQq,q' \in Q, if g(q)0g(q) \geq 0and (q,a,q)Δ(q,a,q') \in \Delta, then 0g(q)g(q)0 \leq g'(q') \leq g(q)​.

            We now construct A=(Q,Σ,Δ,S,F)A' = (Q',\Sigma,\Delta',S',F') as follows:

            Q=R×2QQ' = R \times 2^Q

            S={g0,, where g0(q)=2.Q if qS and g0(q)= if qS}S' = \{ \langle g_0,\emptyset \rangle,  where  g_0(q) = 2.|Q|  if  q\in S  and  g_0(q) = \bot  if  q\notin S\}

            Δ={(g,,a,g,Pg \Delta' = \{(\langle g,\emptyset \rangle,a,\langle g',P' \rangle \mid g' covers g,g,and P={qQg(q) P' = \{q' \in Q \mid g'(q') is even }}\}\}

            {(g,P,a,g,P)P,g\cup \{ (\langle g,P \rangle,a,\langle g',P' \rangle) \mid P \neq \emptyset , g'covers gg, and

            P={qQ(q,a,q)Δ,qP,g(q) P' = \{q'\in Q \mid (q,a,q') \in \Delta, q\in P, g'(q') is even }}\}\}

            F=R×{}F' = R \times \{\emptyset\}

            It is not very difficult to see that this automaton accepts the complement language

            MONADIC SECOND - ORDER THEORY OF ONE SUCCESSOR

            The logic that Büchi considered was the monadic second order logic of one succesor, abbreviated as S1S. This language is defined formally as follows:

            Terms: A term in S1S is built up from the constant 0 and individual variables x,y,x,y,\dots and by the application of the successor function, succsucc. Examples : 0,succ(x),succ(succ(y