Minimizing interacting finite state machines: a compositional approach to language containment

We address the problem of compositional minimization of collections of interacting finite state machines that arise in the context of formal verification of hardware designs by language containment. Typically much of the behavior of the system is redundant with respect to a given property being verified, and so the system can be replaced by substantially simpler representations. We show that these redundancies can be captured by computing states that are input-output equivalent in the presence of fairness. Since computing complete equivalences is computationally expensive, we propose a spectrum of approximations which are efficiently computable. Directly minimizing the entire system requires forming the complete product machine, which can be very large, and hence we describe procedures that hierarchically minimize the system with respect to explicit and BDD representations. We present experimental results on some standard verification examples to show that our algorithms allow the product machine to be represented by very small implicit or explicit representations. We conclude with some further directions