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

Proving the equivalenceof two Finite State Machines (FSMs) has many applications to synthesis, verication, 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 sucient check, is mandatory. This is muchmore complexthan traversingjust one of the componentmachines. This paperproposes an equivalence-preservingfunctionthat transformsthe productmachinein the General Product Machine (GPM). Using the GPM in symbolicstate 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.

• Type: Journal
• Year: 1998
• Where: FMSD
• Authors: Gianpiero Cabodi, Paolo Camurati, Fulvio Corno, Paolo Prinetto, Matteo Sonza Reorda
• Keywords: FMSD 1998, Machine, Product Machine, Product Machine Traversal