Implementation of Automata Manipulations - The Unknown Component Problem: Theory and Applications - page 109

6.2.6 Product

Product of two finite automata, A and B, is a new automaton whose states are pairs
of states from A and B, respectively, reachable from the initial states of A and B
under some input sequences.
It is assumed that both A and B are complete when forming the product. This can
be achieved by applying the operation Completion to an automaton that is not yet
complete: in this way it is completed by adding the non-accepting don't care state,
and all missing transitions from any state are directed to this non-accepting don't
care state.
It is assumed that both A and B have the same support when forming the product.
This can be achieved by forcing them to have the same support, if it is not already
the case, by the operation Support , which resets the support of an automaton to
be equal to a given ordered list of variables. For instance suppose that the support
of automaton A is .x; z / and the support of B is .y; z /, then the user must set the
supports of both A and B to be x; y; z .
If A and B share a variable in their supports, it is identified as the same variable
and they must agree in value. Suppose that A is in state s a and B is in state s b ,and
that A transits to accepting state s a on input .˛; ;/ and B transits to accepting
state s b on input . ;ˇ;/ (the input to 0 0 means don't care as an effect of lifting
a variable to get a common support), then the product automaton transits from
product state .s a ;s b / to product state ..s a ; s b / under input .˛;ˇ;/. A product state
is accepting if and only if both of the component states are accepting.
A self-explanatory pseudo-code of the algorithm computing the product of two
automata is presented in Fig. 6.4 . The input to the procedure are the automata and
the limit on the number of states of the product automaton. The output is the product
automaton. The computation will exit if the limit on the number of states is reached.

6.2.7 Prefix-Closed

Prefix-closed is an operation applied to a finite automaton, which transforms it as
follows. The non-accepting states are removed together with all the transitions into
them and from them. Only the states reachable under this new automaton from the
given initial state are kept. This operation returns the empty automaton if the initial
state is not accepting.

6.2.8 Input-Progressive

Input-progressive is an operation, applied to a finite automaton, which transforms it
as follows. First, operation prefix-closed is applied. If the resulting automaton is not