This paper presents the ComBack method for explicit state space exploration. The ComBack method extends the well-known hash compaction method such that full coverage of the state space is guaranteed. Each encountered state is mapped into a compressed state descriptor (hash value) as in hash compaction. The method additionally stores for each state an integer representing the identity of the state and a backedge to a predecessor state. This allows hash collisions to be resolved on-the-fly during state space exploration using backtracking to reconstruct the full state descriptors when required for comparison with newly encountered states. A prototype implementation of the ComBack method is used to evaluate the method on several example systems and compare its performance to related methods. The results show a reduction in memory usage at an acceptable cost in exploration time.
|Title of host publication||Proceedings of the 28th International Conference on Petri Nets and Other Models of Concurrency (ICATPN 2007), 25-29 June 2007, Siedcle, Poland|
|Editors||A. Yakovlev, J. Kleijn|
|Place of Publication||Berlin|
|Publication status||Published - 2007|
|Name||Lecture Notes in Computer Science|