Jun 28, 2011: Alfons Laarman: Parallel Recursive State Compression for Free

June 28, 2011Parallel Recursive State Compression for Free
Room: Zi 5126Alfons Laarman
12:30-13:30

In this work, we focus on reducing memory usage in enumerative model
checking, while maintaining the multi-core scalability obtained in earlier
work. We present a tree-based multi-core compression method, which works by
leveraging sharing among sub-vectors of state vectors.
An algorithmic analysis of both worst-case and optimal compression ratios
shows the potential to compress even large states to a small constant on
average (8 bytes). Our experiments demonstrate that this holds up in
practice: the median compression ratio of 279 measured experiments is within
17% of the optimum for tree compression, and five times better than the
median compression ratio of SPIN's COLLAPSE compression.
Our algorithms are implemented in the LTSmin tool, and our experiments show
that for model checking, multi-core tree compression pays its own way: it
comes virtually without overhead compared to the fastest hash table-based
methods.