When the automatic controls of a number of small automata are synthesized to
form large automata, the latter are often difficult to manipulate and for the most
part cannot be represented graphically. In order to maintain the applicability
of incremental verification techniques, the larger automata are reduced, in accordance
with the invention. This is done by modeling the automata in a discrete event system
DES and by eliminating from the DES all redundant state transitions, disallowed
states, and unimportant selfloops. The novel method is most prominently applicable
in control programs and distributed control system controllers.