Deterministic Finite Automata: States, Transitions, and Accepted Languages

Intuition Beginner

Imagine a turnstile at a subway station. It has two positions: locked and unlocked. You push a coin in, and it unlocks. You walk through, and it locks again. No matter how many times you push a coin without walking through, the turnstile stays unlocked. It has no memory beyond its current position.

A deterministic finite automaton (DFA) is exactly this kind of device. It is a machine with a fixed collection of positions called states. At every moment it is in exactly one state. It reads an input string one symbol at a time, and each symbol causes a single, predetermined move to a new state. There is no choice, no randomness, and no memory of the past beyond which state you happen to be in right now.

After reading the entire input, the DFA either accepts or rejects the string. Acceptance depends only on whether the final state belongs to a designated set of accept states. The language of the DFA is the collection of all strings it accepts.

The remarkable fact about DFAs is that, despite their extreme simplicity, they capture a large and useful class of languages called the regular languages. Every language you can describe with a regular expression, every language you can search for with a text editor's find command, every pattern that does not require counting or nesting — all of these are the languages of some DFA.

Visual Beginner

A DFA drawn as a directed graph. Each state is a circle. Arrows between states are labelled with input symbols. The start state has an incoming arrow from nowhere. Accept states have double circles.

    0        1        0        1
→ [q0] ──→ [q1] ──→ [q2] ──→ [q0]
   │ ↑                │
   └── 1 ─────────────┘ (self-loop omitted for clarity)

This DFA accepts strings over {0, 1} that end in "01". State q0 is the start. After reading a 0, move to q1 (the "maybe we just saw a 0" state). After reading a 1 from q1, move to q2 (accept). From q2, reading a 0 restarts the cycle at q1.

Input string	State sequence	Accepted?
01	q0 → q1 → q2	Yes
001	q0 → q1 → q1 → q2	Yes
010	q0 → q1 → q2 → q1	No
1101	q0 → q0 → q0 → q1 → q2	Yes
10	q0 → q0 → q1	No

The pattern: only strings whose last two symbols are 0 then 1 land in the double-circled accept state q2.

Worked example Beginner

We build a DFA for the language of all strings over the alphabet {0, 1} that end in "01". Call the states $q_0$, $q_1$, $q_2$.

State meanings. State $q_0$ means "I have not just read a 0 that could start the suffix 01." State $q_1$ means "I just read a 0, so the next symbol could complete 01." State $q_2$ means "I just completed 01."

Transitions. From $q_0$, reading a 0 moves to $q_1$ (a potential start of the suffix). Reading a 1 stays in $q_0$ (a 1 cannot start 01).

From $q_1$, reading a 1 completes the suffix, so move to $q_2$ (accept). Reading a 0 stays in $q_1$ (we just saw a 0, which could still be the start of a new suffix).

From $q_2$, reading a 0 moves to $q_1$ (the new 0 could start another suffix). Reading a 1 moves to $q_0$ (a 1 after a completed 01 resets us — we have not just seen a 0).

Accept states. Only $q_2$. The start state is $q_0$.

Trace the string "1101". Start at $q_0$. Read 1: stay $q_0$. Read 1: stay $q_0$. Read 0: go to $q_1$. Read 1: go to $q_2$. Accept. The string ends in 01, so the DFA correctly accepts it.

Trace the string "10". Start at $q_0$. Read 1: stay $q_0$. Read 0: go to $q_1$. End in $q_1$, which is not an accept state. Reject. The string does not end in 01, so the DFA correctly rejects it.

Check your understanding Beginner

Formal definition Intermediate+

Definition (DFA). A deterministic finite automaton is a 5-tuple $M=(Q,\Sigma ,\delta ,q_0,F)$ where:

• $Q$ is a finite set of states,
• $\Sigma$ is a finite input alphabet,
• $\delta :Q\times \Sigma \to Q$ is the transition function,
• $q_0\in Q$ is the start state (also called the initial state),
• $F\subseteq Q$ is the set of accept states (also called final states).

The transition function $\delta$ is total: for every state $q\in Q$ and every symbol $a\in \Sigma$, the value $\delta (q,a)$ is a unique state in $Q$. This totality and uniqueness are what make the automaton deterministic.

Definition (extended transition function). The function $\hat{\delta }:Q\times {\Sigma }^{\ast }\to Q$ extends $\delta$ from single symbols to entire strings by recursion:

$$\hat{\delta }(q,\epsilon )=q,\hat{\delta }(q,wa)=\delta (\hat{\delta }(q,w),a),$$

where $\epsilon$ is the empty string, $w\in {\Sigma }^{\ast }$, and $a\in \Sigma$.

Definition (accepted language). The DFA $M$ accepts a string $w\in {\Sigma }^{\ast }$ if $\hat{\delta }(q_0,w)\in F$. The language recognised (or accepted) by $M$ is

$$L(M)=\{w\in {\Sigma }^{\ast }:\hat{\delta }(q_0,w)\in F\}.$$

A language $L\subseteq {\Sigma }^{\ast }$ is regular if there exists a DFA $M$ with $L(M)=L$. The class of regular languages over $\Sigma$ is denoted $\mathcal{R}(\Sigma )$.

Definition (product construction). Given two DFAs $M_1=(Q_1,\Sigma ,{\delta }_1,q_{01},F_1)$ and $M_2=(Q_2,\Sigma ,{\delta }_2,q_{02},F_2)$ over the same alphabet, the product DFA is

$$M_1\times M_2=(Q_1\times Q_2,\Sigma ,\delta ,(q_{01},q_{02}),F),$$

where $\delta ((q_1,q_2),a)=({\delta }_1(q_1,a),{\delta }_2(q_2,a))$ and $F$ is chosen according to the desired operation:

• For intersection: $F=F_1\times F_2$.
• For union: $F=(F_1\times Q_2)\cup (Q_1\times F_2)$.
• For complement of $M_1$: flip accept and non-accept states, $F=Q_1\setminus F_1$.

Counterexamples to common slips

• "A DFA with more states accepts more strings." The number of states constrains memory, not the size of the language. A single-state DFA with an accept state and self-loops on all symbols accepts ${\Sigma }^{\ast }$, an infinite language, while a 100-state DFA can accept the empty language.

• "The transition function can be undefined on some inputs." By definition $\delta$ is a total function from $Q\times \Sigma$ to $Q$. If you want some transitions to be "missing," you are thinking of a nondeterministic automaton (see 47.01.02).

• "Accepting a string means the DFA prints yes." Acceptance is defined by the final state being in $F$. There is no output beyond the classification into accept or reject.

Key theorem with proof Intermediate+

Theorem (closure under Boolean operations). The class of regular languages is closed under union, intersection, and complement. That is, if $L_1$ and $L_2$ are regular, then so are $L_1\cup L_2$, $L_1\cap L_2$, and $\overline{L_1}={\Sigma }^{\ast }\setminus L_1$.

Proof (complement). Let $M=(Q,\Sigma ,\delta ,q_0,F)$ recognise $L_1$. Define $\overline{M}=(Q,\Sigma ,\delta ,q_0,Q\setminus F)$. For any string $w$:

$${\hat{\delta }}_{\overline{M}}(q_0,w)={\hat{\delta }}_M(q_0,w),$$

since the transition function is unchanged. The string $w$ is accepted by $\overline{M}$ iff ${\hat{\delta }}_M(q_0,w)\in Q\setminus F$, which holds iff $w\notin L_1$. So $L(\overline{M})={\Sigma }^{\ast }\setminus L_1$.

Proof (intersection via product). Let $M_1$ recognise $L_1$ and $M_2$ recognise $L_2$. Construct $M=M_1\times M_2$ with $F=F_1\times F_2$. By induction on $|w|$:

$$\hat{\delta }((q_{01},q_{02}),w)=({\hat{\delta }}_1(q_{01},w),{\hat{\delta }}_2(q_{02},w)).$$

The base case $w=\epsilon$ is immediate. The inductive step: $\hat{\delta }((q_1,q_2),wa)=\delta (\hat{\delta }((q_1,q_2),w),a)=\delta (({\hat{\delta }}_1(q_1,w),{\hat{\delta }}_2(q_2,w)),a)=({\delta }_1({\hat{\delta }}_1(q_1,w),a),{\delta }_2({\hat{\delta }}_2(q_2,w),a))=({\hat{\delta }}_1(q_1,wa),{\hat{\delta }}_2(q_2,wa))$.

Therefore $w\in L(M)$ iff ${\hat{\delta }}_1(q_{01},w)\in F_1$ and ${\hat{\delta }}_2(q_{02},w)\in F_2$, i.e. $w\in L_1\cap L_2$. $\square$

Bridge. The product construction is the foundational reason regular languages form a Boolean algebra: any two regular languages can be combined by intersection, union, or complement without leaving the class. This builds toward the Myhill-Nerode theorem in 47.01.04, where the product construction reappears as the canonical way to compute the minimal DFA, and it appears again in 47.01.02 where the subset construction converts an NFA into a DFA by taking the power set of the NFA's states — a generalised product. The central insight is that DFAs compose: running two machines in parallel is itself a machine, and this is exactly what makes the regular languages algebraically well-behaved.

Exercises Intermediate+

Lean formalization Intermediate+

Mathlib has a DFA structure in Computability.DFA with fields δ, evalFrom, and accepts, but it does not provide the product construction for intersection or union as a named construction, nor the proof that the product DFA accepts the intersection of the two component languages. The Myhill-Nerode theorem and the minimisation algorithm are also absent. A Codex.Automata.DFA.Product module defining DFA.product and proving DFA.accepts (M₁.prod M₂) = DFA.accepts M₁ ∩ DFA.accepts M₂ would be the load-bearing first step; this unit ships without it.

Advanced results Master

The product construction gives regular languages the structure of a Boolean algebra. Three further results sharpen our understanding of what DFAs can and cannot do.

Theorem 1 (Myhill-Nerode). Let $L\subseteq {\Sigma }^{\ast }$. Define the equivalence relation ${\equiv }_L$ on ${\Sigma }^{\ast }$ by $x{\equiv }_{L}y$ iff $\forall z\in {\Sigma }^{\ast }$, $xz\in L\iff yz\in L$. Then $L$ is regular iff ${\equiv }_L$ has finitely many equivalence classes. Moreover, the number of classes equals the number of states in the minimal DFA for $L$ ^{[Hopcroft, Motwani & Ullman §2.4]}.

The proof constructs the minimal DFA directly: each state corresponds to an equivalence class, and the transition function sends the class of $x$ under symbol $a$ to the class of $xa$. This DFA is unique up to isomorphism, and any other DFA for $L$ can be collapsed onto it by merging states that are ${\equiv }_L$-equivalent. The Myhill-Nerode theorem is the structural reason why some languages need many states and others need few.

Theorem 2 (closure under reversal). If $L$ is regular, then $L^R=\{w^R:w\in L\}$ (where $w^R$ is $w$ written backwards) is also regular.

The proof uses an NFA construction: reverse all arrows, swap the start state with the accept states, and convert back to a DFA via the subset construction of 47.01.02. The resulting DFA may have exponentially more states, but it is still finite.

Theorem 3 (closure under homomorphism and inverse homomorphism). Let $h:{\Sigma }^{\ast }\to {\Gamma }^{\ast }$ be a homomorphism (a function satisfying $h(uv)=h(u)h(v)$). If $L\subseteq {\Gamma }^{\ast }$ is regular, then $h^{-1}(L)=\{w\in {\Sigma }^{\ast }:h(w)\in L\}$ is regular. If $L\subseteq {\Sigma }^{\ast }$ is regular, then $h(L)$ need not be regular, but $h(L)$ is regular when $h$ is a letter homomorphism (each symbol maps to a single symbol or the empty string).

The inverse homomorphism closure is proved by feeding each symbol $a\in \Sigma$ into the DFA for $L$ by running the DFA on $h(a)$ from the current state. The extended transition function handles multi-symbol images naturally. This result is fundamental in the theory of regular substitutions and is used in the proof of the pumping lemma 47.01.04.

Synthesis. The DFA model is the foundational reason the regular languages are algebraically well-behaved: the product construction gives Boolean closure, the Myhill-Nerode theorem gives a canonical minimal representative for each regular language, and homomorphism closure connects regularity over one alphabet to regularity over another. The central insight is that finiteness of the state set constrains memory but not expressiveness within the regular class, and putting these together with the subset construction of 47.01.02 and Kleene's theorem of 47.01.03 yields the equivalence of three characterisations of regularity: DFAs, NFAs, and regular expressions. This equivalence is the structural backbone of formal language theory, and it appears again in the Chomsky hierarchy where each level (regular, context-free, context-sensitive, recursively enumerable) is defined by the type of automaton that recognises it.

Full proof set Master

Proposition 1 (closure under complement). If $L$ is regular, then $\overline{L}={\Sigma }^{\ast }\setminus L$ is regular.

Proof. Let $M=(Q,\Sigma ,\delta ,q_0,F)$ recognise $L$. Define $\overline{M}=(Q,\Sigma ,\delta ,q_0,Q\setminus F)$. Since the transition function $\delta$ is unchanged, ${\hat{\delta }}_{\overline{M}}(q_0,w)={\hat{\delta }}_M(q_0,w)$ for all $w$. Then $w\in L(\overline{M})$ iff ${\hat{\delta }}_M(q_0,w)\in Q\setminus F$ iff ${\hat{\delta }}_M(q_0,w)\notin F$ iff $w\notin L$. So $L(\overline{M})={\Sigma }^{\ast }\setminus L$. $\square$

Proposition 2 (product construction correctness for intersection). Let $M_1$ and $M_2$ be DFAs over $\Sigma$. Then $L(M_1\times M_2)=L(M_1)\cap L(M_2)$ when $F=F_1\times F_2$.

Proof. Let $M=(Q_1\times Q_2,\Sigma ,\delta ,(q_{01},q_{02}),F_1\times F_2)$ where $\delta ((q_1,q_2),a)=({\delta }_1(q_1,a),{\delta }_2(q_2,a))$. Claim: for all $w\in {\Sigma }^{\ast }$,

$$\hat{\delta }((q_{01},q_{02}),w)=({\hat{\delta }}_1(q_{01},w),{\hat{\delta }}_2(q_{02},w)).$$

By induction on $|w|$. Base: $w=\epsilon$, both sides equal $(q_{01},q_{02})$. Step: $w=ua$. By induction, $\hat{\delta }((q_{01},q_{02}),u)=({\hat{\delta }}_1(q_{01},u),{\hat{\delta }}_2(q_{02},u))$. Then:

$$\hat{\delta }((q_{01},q_{02}),ua)=\delta (\hat{\delta }((q_{01},q_{02}),u),a)=\delta (({\hat{\delta }}_1(q_{01},u),{\hat{\delta }}_2(q_{02},u)),a)=({\delta }_1({\hat{\delta }}_1(q_{01},u),a),{\delta }_2({\hat{\delta }}_2(q_{02},u),a))=({\hat{\delta }}_1(q_{01},ua),{\hat{\delta }}_2(q_{02},ua)).$$

Therefore $w\in L(M)$ iff $\hat{\delta }((q_{01},q_{02}),w)\in F_1\times F_2$ iff ${\hat{\delta }}_1(q_{01},w)\in F_1$ and ${\hat{\delta }}_2(q_{02},w)\in F_2$ iff $w\in L(M_1)\cap L(M_2)$. $\square$

Proposition 3 (Myhill-Nerode theorem, forward direction). If $L$ is regular, then ${\equiv }_L$ has finitely many equivalence classes.

Proof. Let $M=(Q,\Sigma ,\delta ,q_0,F)$ recognise $L$. Define $\phi :{\Sigma }^{\ast }\to Q$ by $\phi (w)=\hat{\delta }(q_0,w)$. If $\phi (x)=\phi (y)$ then for all $z$, $\hat{\delta }(q_0,xz)=\hat{\delta }(\hat{\delta }(q_0,x),z)=\hat{\delta }(\hat{\delta }(q_0,y),z)=\hat{\delta }(q_0,yz)$, so $xz\in L\iff yz\in L$, i.e., $x{\equiv }_{L}y$. The function $\phi$ partitions ${\Sigma }^{\ast }$ into at most $|Q|$ classes, so ${\equiv }_L$ has at most $|Q|$ equivalence classes. $\square$

Connections Master

• 50.03.01 — Big-O and complexity analysis provide the framework for analysing the time and space efficiency of DFA simulation, where processing a string of length $n$ takes $O(n)$ time and $O(1)$ space (the current state).

• 37.01.01 — Probability spaces and distributions underpin the theory of probabilistic automata, a generalisation of DFAs where transitions are stochastic and acceptance is defined by a threshold on the probability of reaching an accept state.

• 47.01.02 — NFAs generalise DFAs by allowing multiple transitions per state-symbol pair; the subset construction converts any NFA to a DFA, proving both models recognise exactly the regular languages.

• 47.01.03 — Regular expressions provide an algebraic description of the same class of languages; Kleene's theorem proves the equivalence of DFA-recognisable and regex-describable languages.

• 47.01.04 — The pumping lemma for regular languages proves that certain languages are not regular by exploiting the finiteness of the DFA state set, formalising the pigeonhole argument that a DFA with $n$ states reading a string of length $>n$ must revisit a state.

Historical & philosophical context Master

The concept of finite automata emerged from the study of nerve nets by Warren McCulloch and Walter Pitts in 1943, who modelled neurons as threshold logic devices. Stephen Kleene formalised their behaviour in 1956 with the representation theorem for regular events, proving that the languages recognised by these finite-state devices are exactly those described by regular expressions ^{[Sipser §1.1]}.

Michael Rabin and Dana Scott's 1959 paper "Finite Automata and Their Decision Problems" introduced the formal DFA model as a 5-tuple, proved closure under Boolean operations via the product construction, and established the equivalence between deterministic and nondeterministic finite automata. This work earned them the Turing Award in 1976. The product construction itself is a natural instance of the Cartesian product of monoid actions: the state sets of two DFAs carry actions of the free monoid ${\Sigma }^{\ast }$, and the product DFA carries the diagonal action.

Anil Nerode (1958) and John Myhill (1957) independently proved the theorem that now bears their names, characterising regularity by the finiteness of a right-invariant equivalence relation. The Myhill-Nerode theorem provides a canonical minimal DFA for each regular language and is the theoretical basis for DFA minimisation algorithms used in compiler design and pattern matching.

Bibliography Master

@book{sipser2013,
  author    = {Sipser, Michael},
  title     = {Introduction to the Theory of Computation},
  edition   = {3rd},
  publisher = {Cengage Learning},
  year      = {2013},
}
@book{hopcroft2006,
  author    = {Hopcroft, John E. and Motwani, Rajeev and Ullman, Jeffrey D.},
  title     = {Introduction to Automata Theory, Languages, and Computation},
  edition   = {3rd},
  publisher = {Pearson},
  year      = {2006},
}
@article{rabin1959finite,
  author  = {Rabin, Michael O. and Scott, Dana},
  title   = {Finite Automata and Their Decision Problems},
  journal = {IBM Journal of Research and Development},
  volume  = {3},
  number  = {2},
  pages   = {114--125},
  year    = {1959},
}
@article{nerode1958linear,
  author  = {Nerode, Anil},
  title   = {Linear Automaton Transformations},
  journal = {Proceedings of the American Mathematical Society},
  volume  = {9},
  number  = {4},
  pages   = {541--544},
  year    = {1958},
}
@article{kleene1956representation,
  author  = {Kleene, Stephen C.},
  title   = {Representation of Events in Nerve Nets and Finite Automata},
  journal = {Automata Studies},
  pages   = {3--41},
  year    = {1956},
  publisher = {Princeton University Press},
}