A minimized automaton representation of reachable states

被引：12

作者：

Holzmann G.J. ^{[1
]}

Puri A. ^{[1
]}

机构：

[1] Bell Laboratories, Murray Hill

来源：

International Journal on Software Tools for Technology Transfer | 1999年 / 2卷 / 3期

关键词：

Data compression; Finite automata; Model checking; OBDDs; Sharing trees; Spin; Verification;

D O I：

10.1007/s100090050034

中图分类号：

学科分类号：

摘要：

We consider the problem of storing a set S⊂Σk as a deterministic finite automaton (DFA). We show that inserting a new string σ∈Σk or deleting a string from the set S represented as a minimized DFA can be done in expected time O(k{pipe}Σ{pipe}), 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. © 1999 Springer-Verlag.

引用

页码：270 / 278

页数：8

共 10 条

[1]

Bryant, R.E., Graph based algorithms for boolean function manipulation (1986) IEEE Transansactions on Computers, C-35, pp. 677-691

[2]

Bryant, R.E., Symbolic boolean manipulation with ordered binary decision diagrams (1992) Computing Surveys, 24 (3), pp. 293-318

[3]

Grégoire, J.C., State space compression in Spin with GETSs (1996) Proc Second Spin Workshop, , Rutgers University, New Brunswick, NJ, AmericanMathematical Society, DIMACS-32

[4]

Holzmann, G.J., (1991) Design and Validation of Computer Protocols, , Englewood Cliffs, NJ: Prentice Hall

[5]

Holzmann, G.J., State compression in Spin (1997) Proc Third Spin Workshop, , Twente University, The Netherlands, April

[6]

Holzmann, G.J., The model checker Spin (1997) IEEE Transactions on Software Engineering, 23 (5), pp. 279-295

[7]

Holzmann, G.J., Peled, D., Yannakakis, M., On nested depth first search (1996) Proc Second Spin Workshop, , Rutgers University, New Brunswick, NJ, American Mathematical Society, DIMACS/32

[8]

Kimura, S., Clarke, E.M., A parallel algorithm for constructing binary decision diagrams (1990) IEEE International Conference on Computer Design, , In:, September

[9]

Sleator, D., Tarjan, R., Self-adjusting binary search trees (1985) JACM, 32 (3), pp. 652-686

[10]

Visser, W., Memory efficient storage in Spin (1996) Proc Second Spin Workshop, , Rutgers University, New Brunswick, NJ, American Mathematical Society, DIMACS-32

← 1 →