deterministischer endlicher AutomatA = (Z, X, {0, 1}, s, δ, λ), der über zwei anderen deterministischen endlichen Automaten A₁ = (Z₁, X, Y, s₁, δ₁, λ₁) und A₂ = (Z₂, X, Y, s₂, δ₂, λ₂) definiert ist durch

(1) Z = Z₁ × Z₂,

(2) s = (s₁, s₂),

(3) δ : Z × X → Z definiert durch \begin{eqnarray}\delta (({z}_{1},{z}_{2}),x)=({\delta }_{1}({z}_{1},x),{\delta }_{2}({z}_{2},x))\end{eqnarray}

für alle (z₁, z₂) ∈ Z und x ∈ X, und

(4) λ : Z × X → {0, 1} definiert durch \begin{eqnarray}\lambda (({z}_{1},{z}_{2}),x)=1\iff {\lambda }_{1}({z}_{1},x)={\lambda }_{2}({z}_{2},x)\end{eqnarray}

für alle (z₁, z₂) ∈ Z und x ∈ X.

Die übliche Schreibweise ist A = A₁ × A₂.

Produktautomaten werden im Rahmen der sequentiellen Schaltkreisverifikation eingesetzt, um die Äquivalenz von zwei endlichen Automaten nachzuweisen. Die endlichen Automaten A₁ und A₂ zeigen genau dann das gleiche Ein-/Ausgabeverhalten, wenn vom Anfangszustand (s₁, s₂) des Produktautomaten A₁ × A₂ aus kein Zustand erreicht werden kann, an dem der Wert 0 durch die Ausgabefunktion λ ausgegeben wird.