Parallel Recursive State Compression for Free

TL;DR

This paper introduces a multi-core tree-based compression method for enumerative model checking that significantly reduces memory usage while maintaining scalability, achieving near-optimal compression ratios in practice.

Contribution

It presents a novel parallel recursive state compression algorithm leveraging sharing among sub-vectors, improving memory efficiency without sacrificing multi-core scalability.

Findings

Median compression ratio within 17% of optimal

Five times better than SPIN's COLLAPSE compression

No significant overhead compared to hash table methods

Abstract

This paper focuses 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.