In Proc. 28th International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency, ICATPN 2007, volume 4546 of Lecture Notes in Computer Science, pages 445-464. Springer Verlag, Berlin, 2007.
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.
Copyright notice© Springer-Verlag Berlin Heidelberg 2007. All rights reserved.
Online version
icatpn07.pdf (241 Kb)
DOI
BIBTEX entry
@incollection{icatpn07,
author = "Michael Westergaard and Lars Michael Kristensen and Gerth Stølting Brodal and Lars Arge",
booktitle = "Proc. 28th International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency, ICATPN 2007",
doi = "10.1007/978-3-540-73094-1_26",
isbn = "978-3-540-73093-4",
pages = "445-464",
publisher = "Springer {V}erlag, Berlin",
series = "Lecture Notes in Computer Science",
title = "The ComBack Method - Extending Hash Compaction with Backtracking",
volume = "4546",
year = "2007"
}