Automata Products, Composition & Decomposition

A proof-driven guide to combining and factoring finite-state systems: synchronous products and Boolean languages, output-machine products, cascade and FST composition, reachable-state growth, behavioral preservation targets, projection-based factorization, and the Krohn–Rhodes horizon.

“Combine these machines” is not a complete instruction. Two automata may read the same input in parallel, one transducer may feed another in a cascade, or paths may be composed by matching hidden intermediate labels. Each wiring has a different transition rule and a different invariant.

Decomposition is the inverse design problem: replace one machine by smaller interacting components while preserving a declared observation. Language equivalence, input/output trace equivalence, simulation, and graph isomorphism are different preservation targets. This chapter starts with constructions that can be proved from one-step transitions, then marks the much deeper Krohn–Rhodes theory as an advanced horizon.

Name the wiring and observation contract #

Before forming a combined state, answer four questions:

  1. Which external event reaches each component?
  2. Does one component's output become another's input?
  3. Which component state and buffering information must the composite remember?
  4. What does the environment observe: acceptance, an output tuple, an aggregated output, or the full internal graph?

The answers distinguish the core operations:

Construction External input flow Composite memory Compatibility requirement
synchronous parallel product the same symbol reaches both components pair of current states common input alphabet or an explicit fan-out adapter
cascade input enters the first; its output drives the second both states, plus interface buffering if needed first output convention matches second input convention
general FST composition paths are paired when their intermediate labels agree paired states and, with epsilon labels, filter/alignment state a shared intermediate alphabet and exact epsilon semantics

No informal connection label determines any row. Without ports, timing, transition rules, and observables, there is no formal operation to analyze.

Synchronous products track two summaries of one prefix #

Let

Ai=(Qi,Σ,δi,q0i,Fi)A_i=(Q_i,\Sigma,\delta_i,q_{0i},F_i)

be complete DFAs over the same input alphabet. Their synchronous product has state set Q1×Q2Q_1\times Q_2, initial state (q01,q02)(q_{01},q_{02}), and transition

δ((p,q),a)=(δ1(p,a),δ2(q,a)).\delta((p,q),a)=(\delta_1(p,a),\delta_2(q,a)).

The central invariant is

δ∗((q01,q02),w)=(δ1∗(q01,w),δ2∗(q02,w)).\delta^*((q_{01},q_{02}),w) = (\delta_1^*(q_{01},w),\delta_2^*(q_{02},w)).

It holds for ε\varepsilon by the initial-state definition. If it holds for ww, the componentwise transition makes it hold for wawa. Every use of the product follows from this induction: after one shared prefix, the pair contains exactly both component summaries.

Boolean language operations differ only at the observation #

Once the product transition graph is built, choose an accepting predicate on pairs:

Required language Product pair (p,q)(p,q) accepts when…
L(A1)∩L(A2)L(A_1)\cap L(A_2) p∈F1p\in F_1 and q∈F2q\in F_2
L(A1)∪L(A2)L(A_1)\cup L(A_2) p∈F1p\in F_1 or q∈F2q\in F_2
L(A1)∖L(A2)L(A_1)\setminus L(A_2) p∈F1p\in F_1 and q∉F2q\notin F_2
L(A1)△L(A2)L(A_1)\triangle L(A_2) exactly one of p,qp,q is accepting

The transition invariant proves every row. For intersection, for example, the final pair is accepting exactly when the common word places both components in their accepting sets.

Complement does not require a two-machine product: flip acceptance in a complete deterministic automaton. If a diagram omits transitions, first add a rejecting sink and route every missing case to it. Merely toggling the drawn states of a partial machine leaves some words with no run rather than turning rejection into acceptance.

Equivalence and inclusion produce witnesses #

Two complete DFAs are language-equivalent iff their symmetric-difference product has no reachable accepting pair. Inclusion L(A1)⊆L(A2)L(A_1)\subseteq L(A_2) holds iff the difference product L(A1)∖L(A2)L(A_1)\setminus L(A_2) is empty.

Use breadth-first search from the initial pair. For each newly discovered pair, retain its predecessor and the symbol used. If a violating pair is reached, follow predecessors backward to reconstruct a shortest counterexample word. The product is therefore both a decision construction and a diagnostic explanation.

Worked product: parity crossed with length modulo three #

Over {0,1}\{0,1\}, let P2P_2 track whether the count of 1 symbols is even (EE) or odd (OO). Let L3L_3 track input length modulo three with states R0,R1,R2R_0,R_1,R_2.

  • Every input symbol advances RiR_i to Ri+1 mod 3R_{i+1\bmod 3}.
  • Input 0 preserves parity; input 1 toggles it.

The product recognizes “even number of 1 symbols and length divisible by three” by accepting only (E,R0)(E,R_0).

Product state on 0 on 1 Accepting?
(E,R0)(E,R_0) (E,R1)(E,R_1) (O,R1)(O,R_1) yes
(E,R1)(E,R_1) (E,R2)(E,R_2) (O,R2)(O,R_2) no
(E,R2)(E,R_2) (E,R0)(E,R_0) (O,R0)(O,R_0) no
(O,R0)(O,R_0) (O,R1)(O,R_1) (E,R1)(E,R_1) no
(O,R1)(O,R_1) (O,R2)(O,R_2) (E,R2)(E,R_2) no
(O,R2)(O,R_2) (O,R0)(O,R_0) (E,R0)(E,R_0) no

For 101:

(E,R0)→1(O,R1)→0(O,R2)→1(E,R0),(E,R_0)\xrightarrow{1}(O,R_1) \xrightarrow{0}(O,R_2) \xrightarrow{1}(E,R_0),

so the word is accepted. All six pairs are reachable: ε\varepsilon, 0, and 00 reach the three even-row states, while 1, 10, and 100 reach the three odd-row states in cyclic order.

The empty word ε\varepsilon reaches (E,R0)(E,R_0), which is correct because zero ones is even and length zero is divisible by three.

Nominal state count is not reachable state count #

The Cartesian carrier has ∣Q1∣∣Q2∣|Q_1||Q_2| pairs, an upper bound on the explicit product representation. A particular initial state and transition structure may reach far fewer.

Generate the product on demand:

  1. Insert only the initial pair into a work queue.
  2. For each dequeued pair, compute one successor per alphabet symbol.
  3. Add unseen successors.
  4. Stop when the queue is empty.

The result contains exactly the reachable subautomaton. This distinction matters twice:

  • performance depends on generated reachable pairs, not on a blindly materialized Cartesian table;
  • minimization should run after unreachable pairs are removed, because unreachable structure cannot affect external behavior.

The worst case can still reach every pair, as the six-state example does. “Usually smaller” is not a proof about a particular product.

Products of output machines need an output rule #

For two Mealy machines reading the same external symbol, a shared-input product can emit the pair

(λ1(p,a),λ2(q,a)).(\lambda_1(p,a),\lambda_2(q,a)).

It could instead emit h(λ1(p,a),λ2(q,a))h(\lambda_1(p,a),\lambda_2(q,a)) for a declared combining function hh. Pairing, selecting, voting, adding, and suppressing outputs are different observable machines even when their state transition graph is identical.

Moore products similarly need a state-output function such as

ω(p,q)=(ω1(p),ω2(q)).\omega(p,q)=(\omega_1(p),\omega_2(q)).

When Mealy and Moore components are mixed, their observations do not automatically share a clock: a Moore initial output exists before the first consumed input under the classical convention. The adapter must declare whether that value is exposed, buffered, delayed, or omitted. Finite-state transducers develops the timing contract.

Parallel product and cascade are different machines #

Suppose T1T_1 maps external a,b to intermediate x,y, and T2T_2 maps x,y to external 0,1.

Parallel — shared input

Cascade — output becomes input

In the parallel diagram, both components need a compatible external-input interface. In the cascade, T2T_2 need not understand a,b; it consumes only the output of T1T_1. Swapping the boxes changes the required alphabets and generally changes or invalidates the behavior. Cascade is directional and not commutative.

For synchronous one-symbol transducers, the cascade state is a pair. On external input aa, compute

b=λ1(p,a),p′=δ1(p,a),b=\lambda_1(p,a),\quad p'=\delta_1(p,a),

then

c=λ2(q,b),q′=δ2(q,b).c=\lambda_2(q,b),\quad q'=\delta_2(q,b).

Emit cc and enter (p′,q′)(p',q'). The invariant says the downstream state has consumed exactly the complete intermediate output produced so far.

For string-output transducers, one upstream transition may emit several intermediate symbols and trigger several downstream transitions. With epsilon labels, compatible paths may advance one side without the other. General FST composition therefore requires exact label-matching and epsilon-alignment machinery; naive lockstep pair stepping is only the synchronous special case. Mohri's construction establishes closure for sequential and pp-subsequential functions while tracking the paired component state needed by the interface.

Minimization, quotienting, and factorization answer different questions #

Minimization merges states that no future observation can distinguish. Formally, it forms a quotient by behavioral equivalence. The goal is one smaller machine with the same external behavior.

Product factorization seeks components and wiring whose composite behavior reconstructs the original. A factor may preserve a particular coordinate of behavior rather than merge indistinguishable states.

Cascade decomposition may let later components depend on outputs/state summaries from earlier components; it is more general than recognizing a visible Cartesian grid.

These operations can interact, but they are not synonyms. A minimal automaton may still decompose; a visibly product-shaped automaton may contain equivalent states; a quotient can destroy the coordinate labels that made an engineering decomposition obvious while preserving the language.

Elementary direct-product decomposition through projections #

The six-state example was built from pair states, so its coordinate projections are

π1(p,r)=p,π2(p,r)=r.\pi_1(p,r)=p, \qquad \pi_2(p,r)=r.

They commute with transitions:

πi(δ((p,r),a))=δi(πi(p,r),a).\pi_i(\delta((p,r),a)) = \delta_i(\pi_i(p,r),a).

Together with aligned initial states, this one-step square lifts by induction to every word. Each projection of the product run is exactly the corresponding component run.

This gives a verification procedure for a proposed exact direct-product factorization:

  1. Define component state sets, transitions, and projection maps.
  2. Check that the original initial state maps to the tuple of component initial states.
  3. Check transition commutation for every original state and input symbol.
  4. Check that acceptance or output is recovered by a declared predicate/function on component observations.
  5. Determine whether the original states correspond bijectively to the full product, only to its reachable subautomaton, or many-to-one to component tuples.

Renaming the six states A through F and drawing them irregularly does not destroy the factorization: the projection maps still witness it. Conversely, arranging arbitrary states in a rectangle does not prove anything if no commuting projections exist.

State the preservation target before accepting a decomposition #

Several targets form different contracts:

Target Must preserve May change
graph isomorphism every labeled transition and structural incidence up to renaming only state names
input/output trace equivalence every external output trace for every input under one timing convention internal states and wiring
accepted-language equivalence accepted versus rejected words output timing and internal traces not represented by acceptance
simulation/refinement the observations required by the chosen directional relation behavior outside that relation's guarantee

Moore distinguished isomorphism from external indistinguishability precisely because experiments can fail to reveal internal structural differences. A decomposition intended as an implementation replacement usually needs trace equivalence; one used only for a language decision may require less. Claiming “equivalent decomposition” without naming the row leaves the central obligation undefined.

For a deterministic finite machine, a robust proof pattern is:

  • relate each original state to its proposed composite state;
  • prove initial states are related;
  • prove one related transition yields another related pair and preserves the immediate observation;
  • conclude by induction that all finite input traces agree.

If the proof fails, search for a shortest distinguishing input. It is more useful than a large diagram because it shows the first externally visible divergence.

Decomposition is rarely unique #

Even when two components reconstruct behavior, other factorizations or quotients may do so as well. Reasons include:

  • inaccessible product tuples that can be represented or omitted;
  • behaviorally equivalent states that may be merged before or after factoring;
  • different choices of what each component exposes at its interface;
  • a preservation target weaker than graph isomorphism;
  • cascade structures that encode state information differently from a direct product.

A useful engineering decomposition therefore optimizes an explicit concern—separation of responsibilities, verifiability, implementation cost, or interface locality—not an assumed unique “prime” drawing.

Advanced horizon: Krohn–Rhodes theory #

At a high level, the theory identifies finite simple groups as the prime reversible components and includes elementary non-group units for irreversible behavior inside the relevant composition closure. This is deeper than Cartesian product factorization and cannot be compressed into a component-count slogan. The theorem does not make a visible, unique, automatically computed block diagram fall out of an arbitrary state table.

To state the result rigorously, a future chapter must first develop:

  • the transition semigroup/monoid generated by input actions;
  • subsemigroups, quotients, and the exact division relation;
  • finite simple groups;
  • cascade or wreath-product constructions and their action on state sets;
  • the elementary unit/reset components used by the theorem;
  • what equivalence of machines is preserved.

The conceptual lesson is legitimate: reversible permutation-like behavior and irreversible state-collapsing behavior play distinct algebraic roles. The constructive details, complexity, non-uniqueness, and theorem proof belong in that advanced prerequisite chain.

Diagnostic checklist #

  • Do all parallel components consume the same external event, or is an adapter missing?
  • Is a cascade's intermediate alphabet exactly the downstream input alphabet?
  • Is composition order written in the same order that the data flows?
  • Does the pair-state transition preserve the stated prefix invariant?
  • Is the accepting or output predicate part of the construction rather than implied by the graph?
  • Before complement or a Boolean product, are both DFAs deterministic and complete?
  • Is ∣Q1∣∣Q2∣|Q_1||Q_2| being reported as a nominal bound rather than an observed reachable count?
  • Were unreachable pairs removed before minimization?
  • Is minimization being confused with decomposition?
  • Do proposed projections commute with every transition and preserve the selected observation?
  • Is “equivalent” qualified as graph, language, trace, or simulation equivalence?
  • Is a Krohn–Rhodes claim backed by its semigroup/division prerequisites rather than an unsupported slogan?

The common proof pattern is simple even when the systems grow: define the composite state, state what it means after a prefix, prove the one-step transition preserves that meaning, and tie the final observation to the requirement. Decomposition reverses the direction but keeps the obligation—components are valid only when their wiring reconstructs the declared observable behavior.

Sources

  1. paperRabin and Scott — Finite Automata and Their Decision Problems
  2. paperMoore — Gedanken-Experiments on Sequential Machines
  3. paperMohri — Finite-State Transducers in Language and Speech Processing
  4. paperKrohn and Rhodes — Algebraic Theory of Machines I

Searches titles, aliases, headings, summaries, and full text.↑↓ move ↵ open esc close