The ComBack Method - Extending Hash Compaction with Backtracking

Michael Westergaard, Lars Michael Kristensen, Gerth Stølting Brodal, and Lars Arge

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.

Abstract

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

10.1007/978-3-540-73094-1_26

BIBTEX entry

@incollection{icatpn07,
  author = "Michael Westergaard and Lars Michael Kristensen and Gerth St{\o}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"
}