This is a joint work w. Loek Cleophas, Eindhoven University.
We present a minimization algorithm for finite state automata that finds and merges bisimulation-equivalent states, identified through partition aggregation. In terms of applicability, the algorithm is a generalisation of an earlier one by Watson and Daciuk for deterministic devices. We show the algorithm to be correct and run in time O(n^2 d^2 k), where n is the number of states of the input automaton M, d is the maximal outdegree in the transition graph for any combination of state and input symbol, and k is the size of the input alphabet. Our algorithm is slower than the fastest algorithms based on partition refinement, but has the advantage that it requires less space, and that intermediate solutions are also language equivalent to M. As a result, implementations in e.g. time-constrained settings can save memory by transforming the input to an equivalent reduced one. Furthermore, the algorithm essentially searches for the maximal model of a characteristic formula for M, so many of the optimisation techniques used to gain efficiency in SAT solvers are likely to apply.