Decidable Problems About Automata

A decision problem is a language $L$ — a set of strings, typically encodings $\langle \cdot \rangle$ of objects like automata, grammars, or pairs of them. The problem is decidable if there is a Turing machine $M$ such that for every input $w$, $M$ halts, and $M$ accepts $w$ if $w \in L$ and rejects $w$ if $w \notin L$. This is strictly stronger than recognizability (a Turing machine that accepts exactly $L$ but may loop forever on strings not in $L$). Decidability demands a decider: total correctness plus guaranteed termination on every input, without exception. The problems studied here all concern automata as data. We encode a DFA $B$ as a string $\langle B \rangle$ listing its states, alphabet, transition function, start state, and accept states — a finite, parseable description, exactly the kind of encoding covered when discussing Encodings and Enumerators. A Turing machine can then take $\langle B, w \rangle$ as input and simulate $B$ running on $w$, because $B$'s entire behavior is captured by a finite table. This is the same simulation idea that underlies the Universal Turing Machine, specialized here to the much tamer setting where the simulated machine is guaranteed to halt after exactly $|w|$ steps. The four central languages are:

Each is proved decidable by a different technique — direct simulation, bounded enumeration, graph reachability, and reduction via a closure-property construction — and together they form the essential proof vocabulary of Computability Theory.

$A_{DFA}$: decidability by direct simulation. A DFA processes one input symbol per transition and has no way to loop — it reads $w$ once, left to right, and after exactly $|w|$ transitions it is in some single state. So a decider for $A_{DFA}$ just tracks that state. ``` Decider M_ADFA(⟨B, w⟩): // B = (Q, Σ, δ, q0, F) if ⟨B, w⟩ is not a syntactically valid DFA-string pair: reject current ← q0 for each symbol a in w (left to right): current ← δ(current, a) if current ∈ F: accept else: reject ``` The loop runs exactly $|w|$ times; there is no recursion, no backtracking, and no possibility of nontermination, because $\delta$ is a total function on $Q \times \Sigma$.

$A_{CFG}$: decidability by bounded enumeration. A CFG can have infinitely many derivations of a string, and can also loop forever (e.g. rules like $S \to SS$), so naive derivation search is not obviously a decider. The fix is to convert $G$ to Chomsky Normal Form (CNF), in which every rule has the form $A \to BC$ or $A \to a$ (with a single rule $S \to \varepsilon$ allowed only if $\varepsilon \in L(G)$). In CNF every non-$\varepsilon$ rule application either keeps the string of variables the same length while adding one terminal, or replaces one variable with two — so any derivation of a string of length $n \ge 1$ takes exactly $2n - 1$ steps. This bounds the search space to something finite and checkable. ``` Decider M_ACFG(⟨G, w⟩): if ⟨G, w⟩ is not a syntactically valid CFG-string pair: reject G' ← convert G to Chomsky Normal Form n ← length(w) if n = 0: if S ⇒ ε is a rule of G': accept else reject for each derivation D of length exactly 2n − 1 in G': if D derives w: accept reject ``` The number of candidate derivations of length $2n-1$ is finite (bounded by $|G'|^{2n-1}$ choices of rule applications), so the `for` loop is a genuinely finite search, and the whole procedure halts.

$E_{DFA}$: decidability by reachability. A DFA's language is empty exactly when no accepting state can ever be reached from the start state — a pure graph-reachability question on the transition diagram, solvable by breadth-first or depth-first marking. ``` Decider M_EDFA(⟨A⟩): // A = (Q, Σ, δ, q0, F) mark q0 repeat until no new state gets marked: for each marked state q, each symbol a: mark δ(q, a) if any state in F is marked: reject // language is nonempty else: accept // language is empty ``` The marking loop terminates because $Q$ is finite: each pass either marks at least one new state or nothing changes, and once nothing changes the process is complete, after at most $|Q|$ passes.

$EQ_{DFA}$: decidability by reduction to $E_{DFA}$. Rather than comparing $A$ and $B$ directly, build the DFA for their symmetric difference:

Regular languages are closed under complement, intersection, and union — each provable by an explicit product-automaton construction — so $C$ is an explicitly constructible DFA. Crucially, $L(A) = L(B)$ iff $L(C) = \emptyset$, which reduces equivalence checking to the emptiness decider already built. ``` Decider M_EQDFA(⟨A, B⟩): construct DFA C such that L(C) = L(A) △ L(B) // C's states are pairs (state of A, state of B) plus one extra // bit for "in a complemented copy"; accept iff exactly one // of A, B accepts along that path run M_EDFA(⟨C⟩) if M_EDFA accepts (L(C) is empty): accept // L(A) = L(B) else: reject // L(A) ≠ L(B) ```

$A_{DFA}$. Time: $O(n)$ transition lookups for $|w| = n$ (each a $O(1)$ table lookup assuming a fixed-size alphabet), so the simulation is linear in $|w|$ plus the cost of parsing $\langle B \rangle$, which is $O(|B|)$. Space: $O(\log |Q|)$ to store the current state, or $O(|B| + |w|)$ if we count the input tape itself. Correctness is an invariant argument: after processing the first $i$ symbols of $w$, `current` equals $\hat\delta(q_0, w_1\cdots w_i)$, the extended transition function's value — this holds by induction on $i$ (base case $i=0$: `current = q0` by definition; inductive step: applying $\delta$ once extends the extended-transition-function computation by exactly one symbol). At $i = |w|$, `current = \hat\delta(q_0, w)`, and by definition $B$ accepts $w$ iff this lies in $F$ — exactly the decider's accept condition.

$A_{CFG}$. Converting to CNF takes polynomial time in $|G|$ (removing $\varepsilon$-rules, unit rules, and useless symbols, each a standard closure-preserving transformation). The dominant cost is enumerating derivations of length $2n - 1$: with $|G'|$ rules, there are at most $|G'|^{2n-1}$ candidate derivation sequences, so the algorithm as stated runs in time exponential in $n$ — it is a decider, not an efficient one. (In practice, one replaces the brute-force search with the CYK Algorithm, a dynamic-programming table of size $O(n^2)$ over $O(|G'|)$ variables, achieving $O(n^3 |G'|)$ time — the same decidability result, dramatically faster.) Correctness rests on the CNF invariant: every application of a binary rule $A \to BC$ increases the number of variables in the sentential form by exactly one (replacing 1 variable with 2), and every terminal rule $A \to a$ converts one variable to one terminal without changing the count. Starting from 1 variable ($S$) and ending at $n$ terminals with 0 variables forces exactly $n - 1$ binary steps and $n$ terminal steps, i.e. $2n - 1$ steps total — so bounding derivation length to $2n-1$ loses no derivations of $w$, and the search is exhaustive within that bound.

$E_{DFA}$. The marking loop is bounded-degree BFS/DFS over a graph with $|Q|$ vertices and $|Q| \cdot |\Sigma|$ edges, so it runs in $O(|Q| \cdot |\Sigma|)$ time and $O(|Q|)$ space (a boolean "marked" array) — linear in the size of the automaton. Correctness: by induction on the number of marking rounds, a state $q$ becomes marked iff there is a path of transitions from $q_0$ to $q$, i.e. iff $q$ is reachable. $L(A) \ne \emptyset$ iff some string drives $q_0$ to some accept state, which happens iff some accept state is reachable — exactly the marked-set test.

$EQ_{DFA}$. The product construction for $C$ has at most $|Q_A| \cdot |Q_B|$ states (times a constant factor for tracking symmetric difference via complement), so $C$ is polynomial in $|A|$ and $|B|$, and the subsequent call to the $E_{DFA}$ decider is linear in $|C|$ — overall polynomial time. Correctness follows from set identities: $L(A) = L(B)$ iff their symmetric difference is empty, a basic fact of set theory, combined with the closure-property guarantee that $C$ as constructed truly recognizes $L(A) \triangle L(B)$ (provable itself by an invariant on the product automaton's states tracking membership in $A$ and $B$ simultaneously). The unifying theme: every decider above is built by composing smaller deciders and constructions that are each individually guaranteed to terminate — simulation of a total function, bounded search over a provably finite space, or graph search over a finite vertex set. There is no step anywhere that risks an unbounded search, which is precisely the property that will fail when Turing machines replace DFAs.

Trace $EQ_{DFA}$ on two small DFAs over $\Sigma = \{0,1\}$.

• $A$: accepts strings with an even number of 1s. States $\{a_0, a_1\}$, start $a_0$, accept $\{a_0\}$.

$\delta_A(a_0,0)=a_0,\ \delta_A(a_0,1)=a_1,\ \delta_A(a_1,0)=a_1,\ \delta_A(a_1,1)=a_0$.

• $B$: accepts strings whose length is even. States $\{b_0,b_1\}$, start $b_0$, accept $\{b_0\}$.

$\delta_B(b_0,0)=b_1,\ \delta_B(b_0,1)=b_1,\ \delta_B(b_1,0)=b_0,\ \delta_B(b_1,1)=b_0$. These are not equivalent (e.g., "00" has zero 1s — even — length 2 — even, both accept; but "01" has one 1 — odd, $A$ rejects — length 2 — even, $B$ accepts). Let's see the decider catch this.

Step 1 — build $C$ with states $(a_i, b_j)$, accepting iff exactly one of $A, B$ accepts (symmetric difference):

Start state of $C$: $(a_0, b_0)$.

Step 2 — transitions of $C$ (component-wise):

Step 3 — run $E_{DFA}$ on $C$ (reachability marking): Round 0: mark $\{(a_0,b_0)\}$. Round 1: from $(a_0,b_0)$ reach $(a_0,b_1)$ [on 0] and $(a_1,b_1)$ [on 1]. Mark both. Marked set: $\{(a_0,b_0), (a_0,b_1), (a_1,b_1)\}$. Round 2: from $(a_0,b_1)$ reach $(a_0,b_0)$ [old] and $(a_1,b_0)$ [new — mark it]. From $(a_1,b_1)$ reach $(a_1,b_0)$ [same, already about to be marked] and $(a_0,b_0)$ [old]. Marked set now: all four states. Round 3: no new states — stop.

Step 4 — check accept states. $(a_0,b_1)$ and $(a_1,b_0)$ are both marked (reachable) and both are accepting states of $C$.

Result: $M_{EDFA}$ rejects $\langle C \rangle$ (nonempty language reachable) $\Rightarrow$ $M_{EQDFA}$ rejects $\langle A, B \rangle$, correctly reporting $L(A) \ne L(B)$. Indeed the string "01" drives $C$ from $(a_0,b_0) \to (a_0,b_1) \to (a_1,b_0)$, landing in an accepting state of $C$ — confirming the witness found earlier by hand.

Compiler front-ends rely on $A_{CFG}$-style parsing every time a source file is checked against a language grammar — parser generators like Yacc and ANTLR are built on exactly the CNF/CYK-style machinery sketched here. Network intrusion detection systems and firewall rule compilers use $EQ_{DFA}$-style equivalence checking to verify that an optimized rule set behaves identically to the original, unoptimized one, catching bugs before deployment. Static analyzers and linters that reason about regular expressions — flagging a regex that can never match anything — are directly running an $E_{DFA}$ emptiness check under the hood after converting the regex to an automaton. Hardware and protocol verification tools (model checkers) that certify a finite-state machine design never enters a forbidden configuration are running reachability analysis identical in spirit to the $E_{DFA}$ marking algorithm, just at industrial scale with millions of states. All of these applications depend on the same guarantee proved here: for finite automata and context-free grammars, the questions we actually want to ask are always answerable by an algorithm that halts — a guarantee that, as the next article on The Halting Problem and A_TM shows, spectacularly fails once the automaton is replaced by a general-purpose Turing machine.

Ask the tutor: If regular languages are closed under complement, union, and intersection, why isn't equivalence of two arbitrary context-free grammars decidable by the same symmetric-difference trick?