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

• Explicit methods represent STGs in such a way that every state, transition, and

predicate is stored in the computer memory as a separate object.

• Implicit methods represent STGs as transition relations in a monolithic or

partitioned form. A monolithic form uses one relation in contrast to a partitioned
form which has many relations, where it is implied that they are to be conjoined to
form a single relation. Transition relations are expressed and manipulated using
Binary Decision Diagrams (BDDs). The choice of BDDs is motivated by the fact
that they lead to efficient quantification of variables while other representation
often have problems with quantification.

• Hybrid methods use a combination of explicit and implicit representations.

When implicit methods are used, states and transitions are not represented as
specific objects. Instead the BDD is treated as a single object encoding all states
and transitions. For many practical problems, the implicit representation is smaller
than the explicit one. Implicit representations are often preferred in computations,
such as reachability analysis. However, for several important classes of applications,
and for most large practical functions, the size of implicit representations can exceed
the amount of available memory, which makes implicit representations impractical.
While implementing the proposed methods, we experimented with several types
of STG representations. For example, we implemented determinization by subset
construction using three methods, explicit, implicit, and hybrid, and compared their
performance. The hybrid method was the winner in the majority of cases. The
performance of this method scaled well with the problem size.
The above observation motivated the use of a hybrid representation in our
software implementation of language solving. In the subsections below, we focus
on the hybrid representation, in which, states and transitions are stored explicitly
while the predicates are stored implicitly as BDDs. A similar conclusion about the
applicability of a hybrid representation to manipulating automata and FSMs was
reached in the previous work [139].

6.1 Hybrid Representation of Finite Automata

In this subsection, we describe the hybrid representation of finite automata. When
this representation is used, the STG is represented as a graph with explicitly listed
transition predicates. This is similar to the explicit representation. The difference is
that the predicate enabling a transition from one state to another is represented using
a BDD rather than a sum-of-product (SOP).
The reason why the STG is represented explicitly (as a list of nodes and
predicates) is that, in most practical problems, the STG is given in this form as
an input to the program, or it is derived by enumerating states reachable from an
initial state. In both cases, each state is visited at least once during file reading or
during STG extraction from network form. As a result, there is no need to develop
an implicit representation; the states can just as well be stored explicitly and visited
in some order.