Symbolic Optimization of Interacting Controllers Based on Redundancy Identification and Removal

This paper presents a binary decision diagram (BDD)-based algorithm for the optimization of the driven machine, M2, of a finite-state machine (FSM) network with cascade connection, M1 →M2. The technique we propose relies on redundant faults identification and removal. A fault, f, located into machine M 2, is redundant with respect to the overall network if the driving machine M1 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 one to first construct the product machine M2×M2F , where M2F is the faulty FSM, then to connect it to the driving machine, and finally to perform reachability analysis on the composed machine M1→M2×M2F. 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 STGs can not be represented explicitly), we propose to use the product automaton P'=A1×Af, where A1 ' is the finite automaton (FA) accepting all the output sequences of M1, and Af is the FA accepting all the test sequences for fault f, instead of machine M1→M2 ×M2F. This simplifies sensibly the task of the reachability analysis program, since Af has considerably less states and less edges than the product machine M2 ×M2F and, thus, the size of the BDD representation of its transition relation is much more easily manageable. In addition, differently from other approaches, automaton A 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 approac