Introduction

Time for another DFA classic: the Inclusion Problem. Given two DFAs $D_1$ and $D_2$, we ask: is every string accepted by $D_1$ also accepted by $D_2$? In formal terms, do we have

$$ L(D_1) \subseteq L(D_2)? $$

Great news: this is decidable, and it uses a slick reduction to emptiness.

Formal Setup

Let

$$ D_i = (Q_i, Σ, δ_i, q_{0,i}, F_i) \quad\text{for } i=1,2. $$

We want to check whether

$$ L(D_1) \subseteq L(D_2) \quad\Longleftrightarrow\quad L(D_1) \cap \overline{L(D_2)} = ∅. $$

So we just need to test emptiness of the intersection with the complement.

Example DFAs

# DFA I1:
# accepts any string with an even number of '0's.

# DFA I2:
# accepts any string with an even number of '0's or an even number of '1's.
  • Question: Is L(I1) ⊆ L(I2)? Answer: No, consider the string “00” (two zeros, even, so in I1; but it has zero ones which is even, so actually “00” is in I2 as well). Need a better example: “0” (one zero)? That’s odd zeros so not in I1; pick “0011”? Actually both even… Let’s switch: I1 even zeros; I2 only even ones. Then “00”: in I1, but in I2? zeros don’t matter so yes. Hmm. Instead, I2 even zeros and even ones: then I1 ⊆ I2 holds. Bad example.

Let’s pick:

# DFA I1: accepts strings over {a,b} with no 'b'.
# DFA I2: accepts strings with length ≤ 5.
  • Question: Is L(I1) ⊆ L(I2)? Answer: No, strings like “aaaaaaa” are in I1 (only ‘a’s) but not in I2 (length >5).

Algorithm (Complement + Intersection Emptiness)

  1. Complement $D_2$ to get $D_2^c$ by flipping accepting vs. non-accepting states.
  2. Product Automaton: build the product of $D_1$ and $D_2^c$ as in DFA equivalence, with accepting states where $D_1$ accepts and $D_2^c$ accepts (i.e., $D_1$ accepts and $D_2$ rejects).
  3. Check emptiness: if that product has no reachable accepting state, then $L(D_1) \subseteq L(D_2)$; otherwise, it doesn’t.

Runs in $O(|Q_1|\cdot|Q_2|\cdot|Σ|)$ time.

Why It Matters

  • Type Checking: Ensuring outputs of one module conform to another’s expected inputs.
  • Protocol Verification: Guaranteeing one protocol’s message set is within the allowed set of another.

Wrap-Up

That wraps up DFA inclusion! Next: Minimization, how to shrink a DFA to its smallest equivalent form.