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

The algorithm returns without changing the automaton if it is complete. Other-
wise, it creates a new non-accepting state na. Next, the algorithm iterates through
the states of the automaton. For each state, the algorithm computes its domain, i.e.
the union of all transitions enabled from this state. If it is incomplete, a transition
from this state to the non-accepting state is added with the associated transition
being the complement of the domain.

6.2.3 Determinization

Determinization is a crucial step in solving language equations and in many other
algorithms working with finite automata. Determinization of a finite automaton is
required before it is complemented. It derives a deterministic automaton accepting
the same language of the original non-deterministic automaton. If the automaton is
already deterministic, determinization is not performed.
A self-explanatory pseudo-code of determinization by subset construction (see
Sect. 2.3.1) is presented in Fig. 6.3 . The input to the procedure is a finite automaton
and a limit on the number of states of the determinized automaton. The output is a
deterministic automaton that is equivalent to the initial one. The computation will
terminate if the limit on the number of states has been reached.
The procedures called from the determinization algorithm are the following:
newAutomaton : Creates a new finite automaton.
getInitialState : Queries the automaton for its initial state.
getOneState : Extracts one subset state from the set.
deriveStateRelation : Iterates through the subset s of states of automaton A,then
over the transitions from these states, and derives the transition relation of s as a
BDD in terms of inputs, i , and next state variables, x.
getOneCombination : Extracts one arc from the BDD.
stateIsNew : Checks if the end state is already present in the automaton.
addTransition : Adds one transition to the automaton.
getNumStates : Queries automaton for the number of states in it.
A non-trivial part of the above determinization procedure is deriving the subsets
of next states, n.x/, reachable from the subset s. To this end, a single predicate in
terms of variables i and x, minterm(i, x) , is found in R.i; x/, which is the transition
relation of the subset of states, s. Next, the minterm, input(i) , in terms of input
variables, i , is computed from this minterm, by quantifying state variables, x.The
subset of next states, n.x/, reachable under minterm input(i) is found by computing
the image of input(i) using the relation R.i; x/. The full predicate, pred(i) ,ofthe
transition from subset s into subset n is computed by universally quantifying next
state variables, x, from the expression stating equality of R.i; x/ and n.x/;we
want all those i which precisely go to the subset n andnomoreorlessstates.To
understand the reason for computing pred.i/ D8 x ŒR.i; x/ n.x/, suppose as
an example that getOneCombination selects minterm .i 1 ;n 1 /,thenitis input .i 1 /