×

A minimized automaton representation of reachable states. (English) Zbl 1065.68579

Int. J. Softw. Tools Technol. Transf. 2, No. 3, 270-278 (1999).
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.

MSC:

68Q45 Formal languages and automata
68P30 Coding and information theory (compaction, compression, models of communication, encoding schemes, etc.) (aspects in computer science)

Software:

SPIN
Full Text: DOI