A minimized automaton representation of reachable states
type: Item
instance of: scholarly article
title: A minimized automaton representation of reachable states
zbMATH Open document ID: 1065.68579
author: Gerard J. Holzmann
author: Anuj Puri
published in: International Journal on Software Tools for Technology Transfer. STTT
publication date: 1999-01-01T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 68Q45
Mathematics Subject Classification ID: 68P30
zbMATH DE Number: 1862284
zbMATH Keywords: finite automata
zbMATH Keywords: model checking
zbMATH Keywords: verification
zbMATH Keywords: OBDDs
zbMATH Keywords: sharing trees
zbMATH Keywords: data compression
zbMATH Keywords: SPIN
describes a project that uses: SPIN
MaRDI profile type: Publication
full work available at URL: s100090050034
OpenAlex ID: W2044309072
DOI: 10.1007/S100090050034
description: scientific article; zbMATH DE number 1862284