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

The reason why an implicit BDD-based representation is used for the transition
predicates is that

• BDDs are efficient for functions with small support.

• BDDs allow for sharing identical or related functions and reusing the computed

results.

• BDDs are canonical, which allows for the use of BDD node pointers as unique

keys in a hash table.

These advantages are not available when SOPs are used to represent the predicates.
The proposed hybrid representation was tested on a number of practical
problems. It was found useful for problems with up to 100,000 states and 25
inputs/outputs. The number of states and transitions can be increased at the cost
of linear increase in memory and computation time. Increasing the number of
variables above 25 is also possible. However, in this case, the non-robustness
of BDD representation limits the scalability because they can blow up in size
unpredictably.

6.2 Implementation of Particular Commands

In this subsection, we present implementation details of the procedures performing
finite automata manipulations, which are used during language equations solving.

6.2.1 STG Extraction

In many practical applications, an FSM is given as a binary or multi-valued
sequential network, for which the initial state is known. The FSMs STG implied
by this network can be extracted by an algorithm presented below. The resulting
STG is used in a variety of computations.
The extracted STG consists of a set of nodes which represent the set of states of
the FSM reachable from the initial state. Each state is associated with a set of arcs
originating in this state. Each arc has the next state, the output produced, and an
input/output predicate, which enables this transition. In the application dealing with
finite automata, inputs and outputs are treated uniformly. Therefore, in the STG
extraction procedure, we do not distinguish inputs and outputs and simply record
transitions as relations depending on both.
A self-explanatory pseudo-code of the STG extraction algorithm is shown in
Fig. 6.1 . The input to the algorithm is a sequential network with initial states and a
limit on the number of states extracted. The output is the hybrid representation of
the resulting STG. The computation terminates if the limit on the number of states
has been reached.