We present a minimization algorithm for finite state automata that finds and merges bisimulation-equivalent states, identified through partition aggregation. We show the algorithm to be correct and have a time complexity of a low polynomial. The algorithm is slower than those based on partition refinement, but has the advantage that intermediate solutions are also language equivalent to $\machine$. As a result, the algorithm can be run as a maintenance task in the background, and put on hold when needed. Furthermore, the algorithm essentially searches for the maximal model of a characteristic formula for the input automaton, so many of the optimisation techniques used to gain efficiency in SAT solvers are likely to apply.