A minimized automaton representation of reachable states (Q1856175)

We consider the problem of storing a set \(S \subseteq \Sigma ^k\) as a Deterministic Finite Automaton (DFA). We show that inserting a new string \(\sigma \in \Sigma ^k\) or deleting a string from the set \(S\) represented as a minimized DFA can be done in expected time \(O(k | \Sigma | )\), while preserving the minimality of the DFA. The method can be applied to reduce the memory requirements of model checkers that are based on explicit state enumeration. As an example, we discuss an implementation of the method for the model checker SPIN.