Symbolic Optimization of FSM Networks Based on Redundancies Identification and Removal

This paper presents a binary decision diagram (BDD)-based algorithm for the optimization of the driven machine, 2, of a finite-state machine (FSM) network with cascade connection, 1 2. The technique we propose relies on redundant faults identification and removal. A fault, , located into machine 2, is redundant with respect to the overall network if the driving machine 1 is not able to generate any test sequence for such a fault. When the state transition graph (STG) specifications of the network components are available, the standard way for checking the redundancy condition for the considered fault requires to first construct the product machine 2 2 , where 2 is the faulty FSM, then to connect it to the driving machine, and finally to perform reachability analysis on the composed machine 1 2 2 . Clearly, the size of such machine limits the applicability of the approach above to systems whose components have a few tens of states at most, even when symbolic traversal algorithms are used. Since we are interested in dealing with networks of larger FSM’s (i.e., machines whose STG’s can not be represented explicitly), we propose to use the product automaton = 1 , where 1 is the finite automaton (FA) accepting all the output sequences of 1, and is the FA accepting all the test sequences for fault , instead of machine 1 2 2 . This simplifies sensibly the task of the reachability analysis program, since has considerably less states and less edges than the product machine 2 2 and, thus, the size of the BDD representation of its transition relation is much more easily manageable. In addition, differently from other approaches, automaton 1 is not required to be deterministic and state minimal. This allows us to avoid the application of determinization and state minimization procedures whose complexity is exponential. We present experimental results for examples (i.e., network of interacting controllers) on which existing optimization methods are not applicable, due to the size of the component FSM’s. We also provide a comparison to the data produced by state-of-the-art FSM network optimizers on small benchmarks in order to show the effectiveness of our approach.