The General Product Machine: a New Model for Symbolic FSM Traversal

Proving the equivalence of two Finite State Machines (FSMs) has many applications to synthesis, verification, testing, and diagnosis. Building their product machine is a theoretical framework for equivalence proof. There are some cases where product machine traversal, a necessary and sufficient check, is mandatory. This is much more complex than traversing just one of the component machines. This paper proposes an equivalence-preserving function that transforms the product machine in the "General Product Machine" (GPM). Using the GPM in symbolic state space traversal reduces the size of the BDDs and makes image computation easier. As a result, GPM traversal is much less expensive than product machine traversal, its cost being close to dealing with a single machine.