= Deterministic finite automaton
{wiki}
= DFA
{c}
{synonym}
= FDA
{c}
{synonym}
A <deterministic finite automaton> has exactly one <automaton transition> for every <automaton state> and input symbol. Formally, a <DFA> is a <tuple> $(Q,\Sigma,\delta,q_0,F)$: $Q$ is a nonempty <finite set> of <automaton states>, $\Sigma$ a finite <alphabet>, $\delta:Q\times\Sigma\to Q$ a <function>, $q_0$ the initial <automaton state>, and $F\subseteq Q$ the accepting <automaton states>. Its unique path on a <word> accepts if it ends in $F$ after consuming the entire input. Visiting $F$ earlier does not suffice.
For a concrete <binary divisibility automaton>, recognize the <words> whose values in the <binary numeral system> are divisible by three. Choose $Q=\{0,1,2\}$, $\Sigma=\{0,1\}$, $q_0=0$, and $F=\{0\}$. Each <automaton state> names the <congruence class> of the <integer> read so far. Appending a <binary digit> $b$ changes its value $n$ to $2n+b$, so the <automaton transition> is
$$
\delta(r,b)=(2r+b)\bmod 3.
$$
The <modular arithmetic> therefore needs only three <automaton states>, whatever the input length. The full <function> is $\delta(0,0)=0$, $\delta(0,1)=1$, $\delta(1,0)=2$, $\delta(1,1)=0$, $\delta(2,0)=1$, and $\delta(2,1)=2$.
\Image[/binary-remainder-automaton.png]
{title=A three-state <DFA> for <binary digits> representing <integers> divisible by three, with accepted and rejected traces}
For $110_2=6$, the successive <automaton states> are $0\to1\to0\to0$, so the <word> is accepted. For $101_2=5$, they are $0\to1\to2\to2$, so it is rejected. Leading zeros are allowed: they leave the initial <automaton state> unchanged. We explicitly assign value zero to the <empty word>, which is accepted because the initial <automaton state> is accepting. This is a convention for a <formal language>, rather than a claim that ordinary written numerals include a blank numeral.
The generator checks every <word> of up to eight <binary digits>, comparing the final <automaton state> with the <integer> value modulo three. Each length $n$ includes all $2^n$ <words>, preserving leading zeros as distinct inputs:
|| Length $n$
|| <Words> checked
|| Accepted by the <DFA>
|| Values divisible by three
| 0
| 1
| 1
| 1
| 1
| 2
| 1
| 1
| 2
| 4
| 2
| 2
| 3
| 8
| 3
| 3
| 4
| 16
| 6
| 6
| 5
| 32
| 11
| 11
| 6
| 64
| 22
| 22
| 7
| 128
| 43
| 43
| 8
| 256
| 86
| 86
All 511 checks agree. They are useful for catching a reversed arrow or mistaken label, but the reason the <DFA> works at every length is its invariant: after reading any <word> of value $n$, its <automaton state> is $n\bmod3$. The update $n\mapsto2n+b$ preserves that statement by <mathematical induction>. Through the <extended transition function of a deterministic finite automaton>, this becomes $\widehat\delta(0,w)=\operatorname{value}(w)\bmod3$.
Back to article page
