LAUSR

We present a minimization algorithm for non-deterministic finite state automata that finds and merges bisimulation-equivalent states. The bisimulation relation is computed through partition aggregation, in contrast to existing algorithms that use partition refinement. The algorithm simultaneously generalises and simplifies an earlier one by Watson and Daciuk for deterministic devices. We show the algorithm to be correct and run in time $$ O \left( n^2 r^2 \left| \varSigma \right| \right) $$ O n 2 r 2 Σ , where n is the number of states of the input automaton $$M$$ M , r is the maximal out-degree in the transition graph for any combination of state and input symbol, and $$\left| \varSigma \right| $$ Σ is the size of the input alphabet. The algorithm has a higher time complexity than derivatives of Hopcroft’s partition-refinement algorithm, but represents a promising new solution approach that preserves language equivalence throughout the computation process. Furthermore, since the algorithm essentially computes the maximal model of a logical formula derived from  $$M$$ M , optimisation techniques from the field of model checking become applicable.