06 Formalizing Finite Automata

A Formal Model of Computation

We’ve spent some time building an intuition for finite automata through state diagrams. Now, it’s time to put this on a solid mathematical foundation. Why? Because if we want to prove things about the limits of what these machines can do, we need a precise, unambiguous definition.

Historically, it’s interesting to note that the more powerful Turing Machine was formalized before the simpler finite automaton. However, starting with automata is a fantastic way to learn the vocabulary and mechanics of formal models. We can zoom in and see exactly what it means to “compute” in a very constrained world.

Definition: Deterministic Finite Automaton (DFA)

A Deterministic Finite Automaton (DFA) is a mathematical object that we can define as a 5-tuple (a quintuple). We’ll call our automaton $A$:

$$A=(Q,\Sigma ,\delta ,q_0,F)$$

Let’s break down these five components.

1. $Q$ : The Set of States This is a finite, non-empty set of states. In our diagrams, these are the circles. The finiteness of $Q$ is the most crucial, and limiting, feature of this model. Unlike a Turing machine with its infinite tape, a DFA can only store a finite amount of information, determined by which of its states it is currently in.

   $$Q=\{q_0,q_1,q_2,\dots ,q_n\}$$

2. $\Sigma$ : The Input Alphabet This is a finite set of symbols that the automaton can read. The input words are strings from ${\Sigma }^{\ast }$.

3. $q_0$ : The Start State This is one special state from $Q$ where every computation begins. In diagrams, we mark it with an incoming arrow.

   $$q_0\in Q$$

4. $F$ : The Set of Accepting States This is a subset of the states. If the automaton finishes reading the input word and is in one of these states, the word is accepted. In diagrams, we mark them with a double circle. Note that $F$ can be empty, though such an automaton wouldn’t be very interesting.

   $$F\subseteq Q$$

5. $\delta$ : The Transition Function This is the “program” of the automaton. It’s a function that takes the current state and the next input symbol and returns the next state.

   $$\delta :Q\times \Sigma \to Q$$

   For example, $\delta (q_2,1)=q_3$ means “if in state $q_2$ and you read a 1, transition to state $q_3$.” The fact that $\delta$ is a function is what makes the automaton deterministic: for any given state and input symbol, there is exactly one, unambiguous next state. This implies two rules for our diagrams:

   • For every state, there must be exactly one outgoing arrow for every symbol in the alphabet $\Sigma$.
   • You cannot have two arrows leaving the same state with the same label.

How an Automaton Computes

Now that we have the static definition, let’s formalize the dynamic process of computation.

Configurations

A configuration is a snapshot of the automaton’s state at any point during a computation. It captures everything we need to know to continue:

1. The current state the automaton is in.
2. The remaining part of the input word that still needs to be read.

A configuration is a pair $(q,w)$ where $q\in Q$ and $w\in {\Sigma }^{\ast }$.

• Start Configuration: For an input word $w$, the computation always begins in the configuration $(q_0,w)$.
• End Configuration: Any configuration where the remaining word is empty is an end configuration. It looks like $(q,\lambda )$ for some state $q$.

Steps and Computations

A step is the process of moving from one configuration to the next. We use the notation $⊢$ to represent a single step.

$$(q,aw)⊢(p,w)$$

This means we transition from configuration $(q,aw)$ to $(p,w)$. This step is valid if and only if:

1. $a$ is a single symbol from $\Sigma$.
2. $w$ is the rest of the input string.
3. The transition function dictates this move: $\delta (q,a)=p$.

A computation is a sequence of steps starting from the start configuration. We use ${⊢}^{\ast }$ for the reflexive, transitive closure of the step relation, meaning “can reach in zero or more steps.”

The Language of an Automaton

We can now formally define the language accepted by a DFA.

The language accepted by an automaton $A$, denoted $L(A)$, is the set of all input words $w$ for which the computation of $A$ on $w$ starts in the initial configuration and ends in a configuration with an accepting state.

$$L(A)=\{w\in {\Sigma }^{\ast }\mid (q_0,w){⊢}^{\ast }(q,\lambda )\text{ for some }q\in F\}$$

The Extended Transition Function $\hat{\delta }$

It’s often cumbersome to talk about sequences of steps. We can extend the transition function $\delta$ to a new function, $\hat{\delta }$, that works on entire words instead of single symbols.

$\hat{\delta }:Q\times {\Sigma }^{\ast }\to Q$ tells us which state we land in after starting at state $q$ and reading the entire word $w$. It’s defined inductively:

1. Base Case: Reading the empty word doesn’t change the state. $$\hat{\delta }(q,\lambda )=q$$
2. Inductive Step: To read a word $wa$ (a word $w$ followed by a symbol $a$), we first see where $w$ takes us, and then apply the original $\delta$ for the final symbol $a$. $$\hat{\delta }(q,wa)=\delta (\hat{\delta }(q,w),a)$$

Using this, we can write a much cleaner definition for the language of an automaton:

$$L(A)=\{w\in {\Sigma }^{\ast }\mid \hat{\delta }(q_0,w)\in F\}$$

The Class of Regular Languages

We can now define a fundamental class of languages.

The class of regular languages, denoted by the calligraphic $\mathcal{L}$, is the set of all languages for which a Deterministic Finite Automaton exists.

$${\mathcal{L}}_{REG}=\{L\mid \exists \text{ a DFA }A\text{ such that }L(A)=L\}$$

The name “regular” is no coincidence. It turns out that this class of languages is precisely the same class that can be described by regular expressions. One can prove that for any regular expression, you can build a DFA that accepts the same language, and for any DFA, you can derive an equivalent regular expression.

Proving an Automaton Correct: The Method of State Classes

How can we be certain that an automaton we’ve designed accepts the correct language? We need a formal proof technique. The most powerful method is to define the class of each state.

The class of a state $q$, denoted $C(q)$, is the set of all words that drive the automaton from the start state $q_0$ to state $q$.

$$C(q)=\{w\in {\Sigma }^{\ast }\mid \hat{\delta }(q_0,w)=q\}$$

These classes have two crucial properties that stem from the deterministic nature of the automaton:

1. They cover all strings: Every word $w\in {\Sigma }^{\ast }$ must end up in exactly one state, so the union of all state classes is ${\Sigma }^{\ast }$. $$\bigcup _{q\in Q}C(q)={\Sigma }^{\ast }$$
2. They are disjoint: A single word cannot end in two different states. $$\forall p\ne q,C(p)\cap C(q)=\varnothing$$

Together, these mean that the state classes form a partition of ${\Sigma }^{\ast }$.

The language of the automaton is then simply the union of the classes of its accepting states:

$$L(A)=\bigcup _{q\in F}C(q)$$

Example: Proving the Parity Checker Correct

Let’s formally prove that our parity automaton accepts all strings of even length.

Claim: The classes of the states are:

• $C(q_0)=\{w\in \{0,1{\}}^{\ast }\mid |w{|}_0\text{ is even and }|w{|}_1\text{ is even}\}$
• $C(q_1)=\{w\in \{0,1{\}}^{\ast }\mid |w{|}_0\text{ is even and }|w{|}_1\text{ is odd}\}$
• $C(q_2)=\{w\in \{0,1{\}}^{\ast }\mid |w{|}_0\text{ is odd and }|w{|}_1\text{ is even}\}$
• $C(q_3)=\{w\in \{0,1{\}}^{\ast }\mid |w{|}_0\text{ is odd and }|w{|}_1\text{ is odd}\}$

Proof by Induction on Word Length $|w|$

• Base Case ($|w|=0$): The only word is $w=\lambda$. It has zero 0s and zero 1s (both even). The automaton starts and ends in $q_0$. So $\lambda \in C(q_0)$. The claim holds.

• Inductive Step: Assume the claim holds for all words of length $i$. Let $w$ be a word of length $i+1$. We can write $w=za$, where $|z|=i$ and $a$ is a single symbol. By the inductive hypothesis, we know $z$ is in the correct class based on its parity counts. We must check all 8 cases (4 states for $z$, 2 choices for $a$). Let’s do one:

  • Suppose $z\in C(q_0)$ (even 0s, even 1s) and $a=0$. The word $w=z0$ has an odd number of 0s and an even number of 1s. Our claim says $w$ should be in $C(q_2)$. Does the automaton agree? From state $q_0$, reading a 0 transitions to $q_2$. Yes, it matches.

By checking all 8 cases, we can confirm the claim is correct.

Conclusion: The accepting states are $F=\{q_0,q_3\}$. The language is $L(A)=C(q_0)\cup C(q_3)$.

• Words in $C(q_0)$ have (even 0s + even 1s) $⟹$ even total length.
• Words in $C(q_3)$ have (odd 0s + odd 1s) $⟹$ even total length. Therefore, $L(A)$ is the language of all binary strings of even length.

Building an Automaton: A Worked Example

Let’s design a DFA for the following language:

$$L=\{w\in \{0,1{\}}^{\ast }\mid (|w{|}_0=3)\wedge (|w{|}_1\ge 2\vee |w{|}_1=0)\}$$

The language consists of words with exactly three 0s AND either at least two 1s OR exactly zero 1s.

The key to tackling such a problem is to realize that the automaton must track the counts of 0s and 1s simultaneously. We can imagine a grid of states, where each state represents a pair of counts seen so far.

• The number of 0s can be 0, 1, 2, 3, or "$>3$" (more than 3). This gives us 5 conditions to track vertically.
• The number of 1s can be 0, 1, or "$\ge 2$". This gives us 3 conditions to track horizontally.

This conceptual grid forms the structure of our automaton. Each state $q_{i,j}$ will represent having seen $i$ zeros and $j$ ones.

Let’s analyze the structure of this state diagram:

• Rows: The rows count the number of 1s.
  • Top row: We have seen zero 1s.
  • Middle row: We have seen exactly one 1.
  • Bottom row: We have seen two or more 1s.
• Columns: The columns count the number of 0s.
  • First column: Zero 0s.
  • Second column: One 0.
  • Third column: Two 0s.
  • Fourth column: Exactly three 0s.
  • Fifth column: More than three 0s (a “trap” column).

Transitions:

• Reading a 0 moves us one step to the right within the same row (increasing the 0 count).
• Reading a 1 moves us one step down within the same column (increasing the 1 count).

Special States:

• Start State: The top-left state, $q_{0,0}$, represents having seen zero 0s and zero 1s.
• Trap States: The rightmost column represents having seen more than three 0s. Once we enter this column, we can never leave, because the condition $|w{|}_0=3$ can no longer be met.
• Loops: The bottom row represents having seen two or more 1s. Since the condition is $|w{|}_1\ge 2$, reading more 1s doesn’t change the satisfaction of this condition, so we loop on 1s in this row. Similarly, we loop on 0s in the rightmost column.

Accepting States: To be accepted, a word must end in a state that satisfies both conditions.

1. The 0s condition: $|w{|}_0=3$. This means we must be in the fourth column.
2. The 1s condition: $|w{|}_1=0$ OR $|w{|}_1\ge 2$. This means we must be in the top row OR the bottom row.

The states that satisfy both are the intersection of these requirements:

• $q_{3,0}$ (top row, fourth column)
• $q_{3,\ge 2}$ (bottom row, fourth column)

These are marked with double circles in the diagram.

State Minimization (A Quick Look)

One might notice that the three states in the rightmost “trap” column are functionally identical: once entered, they are non-accepting and can never be left. We could simplify the automaton by merging these three states into a single “trap” or “garbage” state ($q_{Abfall}$).

(Note: This is a conceptual simplification; the original diagram is also a valid and correct DFA for the language.)

Defining the State Classes

To formally prove this automaton is correct, we would define the class for each state. Let’s name the states $q_{i,j}$ where $i$ is the count of 0s and $j$ is the count of 1s.

• For $i\in \{0,1,2,3\}$ and $j\in \{0,1\}$: $C(q_{i,j})=\{w\mid |w{|}_0=i\text{ and }|w{|}_1=j\}$
• For the “at least” states: $C(q_{i,\ge 2})=\{w\mid |w{|}_0=i\text{ and }|w{|}_1\ge 2\}$
• For the trap states: $C(q_{>3,j})=\{w\mid |w{|}_0>3\text{ and }|w{|}_1=j\}$ (and similarly for $j\ge 2$)

The language of the automaton is the union of the classes of the accepting states:

$$L(A)=C(q_{3,0})\cup C(q_{3,\ge 2})$$

This precisely matches the formal definition of our target language.

Defining State Classes for the Infix Automaton

A typical exam question would be not only to design such an automaton but also to formally define the class of each state, that is, to describe precisely which words land you in which state. Let’s do this for the automaton we just built.

The key is to remember what each state represents: the longest suffix of the word seen so far that is also a prefix of our target pattern, AABA.

• The Accepting State: $C(q_{AABA})$ This one is straightforward. The only way to land in the accepting state is to have successfully found the infix AABA. Once there, we never leave. Therefore, the class of this state is simply the language $L$ itself.

  $$C(q_{AABA})=L=\{w\in \{A,B{\}}^{\ast }\mid w\text{ contains the infix AABA}\}$$

• The “Almost There” State: $C(q_{AAB})$ This is the class of all words that have put us on the brink of success.

  $$C(q_{AAB})=\{w\in \{A,B{\}}^{\ast }\mid w\text{ has suffix AAB, but }w\notin L\}$$

  We must explicitly exclude the words that are already in $L$. For example, the word AABAAB ends in AAB, but it also contains AABA, so it would be in $C(q_{AABA})$, not here.

• The “Two As” State: $C(q_{AA})$ These are words where the longest relevant suffix is AA.

  $$C(q_{AA})=\{w\in \{A,B{\}}^{\ast }\mid w\text{ has suffix AA, but }w\notin L\cup C(q_{AAB})\}$$

  We must exclude words that have an even longer relevant suffix, like AAB.

• The “Single A” State: $C(q_A)$ These are words where the longest relevant suffix is just a single A.

  $$C(q_A)=\{w\in \{A,B{\}}^{\ast }\mid w\text{ has suffix A, but }w\notin L\cup C(q_{AAB})\cup C(q_{AA})\}$$

• The Start State: $C(q_{\lambda })$ This class contains everything else. These are the words that do not contain the AABA infix and do not end in A, AA, or AAB.

  $$C(q_{\lambda })=\{w\in \{A,B{\}}^{\ast }\mid w\notin (L\cup C(q_{AAB})\cup C(q_{AA})\cup C(q_A))\}$$

  This includes words that end in B, like BB or ABAB, and the empty word $\lambda$.

This completes the formal analysis of our automaton. We have not only designed a machine to solve the problem but have also rigorously defined what each component of the machine is “thinking” at every step of the computation.

Continue here: 07 Combining Automata and Proving Non-Regularity