A minimized automaton representation of reachable states (Q1856175)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | A minimized automaton representation of reachable states |
scientific article |
Statements
A minimized automaton representation of reachable states (English)
0 references
1999
0 references
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.
0 references
finite automata
0 references
model checking
0 references
verification
0 references
OBDDs
0 references
sharing trees
0 references
data compression
0 references
SPIN
0 references