Generalized finite automaton

A finite directed automaton whose edge labels are regular expressions rather than individual letters. A path accepts concatenations of words in its successive labels, with choices over all accepting paths combined by union.

To remove an internal state $k$, replace each surviving label by $R_{ij}\cup R_{ik}(R_{kk}{)}^{\ast }{R}_{kj}$. The added term accounts for entering $k$, traversing its loop any number of times, and leaving it. Fresh initial and final states allow all old states to be eliminated, producing a regular expression for the same language.

For numbered states of a finite-state automaton, $R_{ij}^{(k)}$ is a regular expression describing paths from $i$ to $j$ whose internal states have numbers at most $k$. Splitting a path at its visits to state $k$ gives $R_{ij}^{(k)}=R_{ij}^{(k-1)}+R_{ik}^{(k-1)}(R_{kk}^{(k-1)}{)}^{\ast }{R}_{kj}^{(k-1)}$. At stage zero use individual edge labels and an empty-word option when the endpoints coincide. This proves the automaton-to-expression direction of Kleene theorem.