= Solution
From the decoded <deterministic finite automaton>, retain only productive states: those reachable from the initial state and from which an accepting state is reachable. Both <sets> are computable by finite <graph search>. Its <regular language> is infinite precisely when this productive directed graph contains a directed cycle.
Indeed, a cycle on a route from the start to acceptance can be repeated arbitrarily often, giving accepted words of different lengths. Conversely an accepted path of length at least the number of productive states repeats one such state and gives a productive cycle. Therefore absence of cycles bounds every accepted length strictly below that number. Cycle detection is a finite algorithm, proving that \b[finiteness of the accepted language is decidable].
When it is finite, enumerate every word of length less than the number of states and simulate acceptance, then count the accepted words. This includes the empty word. Alternatively use dynamic programming in the productive acyclic graph:
$$
N(q)=\mathbf1_{\{q\text{ accepting}\}}+
\sum_{a:\delta(q,a)\text{ productive}}N(\delta(q,a)).
$$
Distinct alphabet symbols count distinct words even when their transitions share a destination. The result is $N(q_0)$, or zero if the start state is not productive. Validity of the encoding is checked first, so the <set> of valid finite-language codes is <recursive set>.
Back to article page
