Method of verification of a finite state sequential machine and resulting information support and verification tool

Abstract From the Canadian patent

The method of computing the reverse image of the transition function .DELTA.(.delta..delta.') of a product finite state machine (PFSM) : .DELTA.-1(E n-1) from the set of n-1 equivalent states comprises the steps of (a) constructing in a canonical way from the BDD of the graph of the equivalence relation E n-1 the BDD of the graph of a total function from S into S named cross-section and denoted C(E n-1) (b) constructing from the cross-section and vector .delta. a new vector .delta.n-1= C(E n-1) o .delta. and (c) computing the equivalent pairs of states with respect to the vector .delta.n-1 to have the pairs of (~x.DELTA.-1(E n-1)).