Module Fix.Minimize

This module offers a minimization algorithm for deterministic finite automata (DFAs).

The algorithm is based on Antti Valmari's 2012 paper, "Fast brief practical DFA minimization". Our implementation differs from Valmari's in the use of an abstraction barrier between the partition refinement data structure and the refinement algorithm.

module type DFA = sig ... end

The signature DFA describes a deterministic finite-state automaton.

module Minimize (Label : sig ... end) (A : sig ... end) : sig ... end

The functor application Minimize(Label)(A) applies a partition refinement algorithm to minimize the deterministic finite automaton A. The time complexity of this operation is O(n + m.log m), where n is the number of states of the automaton A and m is the number of its transitions. This bound is independent of the size of the alphabet of the transition labels.