Parallel Recursive State Compression for Free

Alfons Laarman, Jan Cornelis van de Pol, M. Weber

Research output: Book/ReportReport

  • 20 Citations

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.
LanguageUndefined
Place of PublicationIthaca, NY
PublisherArXiv
Number of pages19
StatePublished - 15 Apr 2011

Publication series

Name
No.arXiv:1104.3119

Keywords

  • Multi-Core
  • Model Checking
  • CR-D.2.4
  • METIS-277631
  • EWI-20160
  • state space compression
  • Parallel
  • incremental algorithm
  • tree-based algorithm

Cite this

Laarman, A., van de Pol, J. C., & Weber, M. (2011). Parallel Recursive State Compression for Free. Ithaca, NY: ArXiv.
Laarman, Alfons ; van de Pol, Jan Cornelis ; Weber, M./ Parallel Recursive State Compression for Free. Ithaca, NY : ArXiv, 2011. 19 p.
@book{20b069da552b4e2bb28511f3511c07be,
title = "Parallel Recursive State Compression for Free",
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.",
keywords = "Multi-Core, Model Checking, CR-D.2.4, METIS-277631, EWI-20160, state space compression, Parallel, incremental algorithm, tree-based algorithm",
author = "Alfons Laarman and {van de Pol}, {Jan Cornelis} and M. Weber",
note = "Proceedings of the 18th International SPIN Workshop, SPIN 2011, Snow Bird, Utah",
year = "2011",
month = "4",
day = "15",
language = "Undefined",
publisher = "ArXiv",
number = "arXiv:1104.3119",

}

Laarman, A, van de Pol, JC & Weber, M 2011, Parallel Recursive State Compression for Free. ArXiv, Ithaca, NY.

Parallel Recursive State Compression for Free. / Laarman, Alfons; van de Pol, Jan Cornelis; Weber, M.

Ithaca, NY : ArXiv, 2011. 19 p.

Research output: Book/ReportReport

TY - BOOK

T1 - Parallel Recursive State Compression for Free

AU - Laarman,Alfons

AU - van de Pol,Jan Cornelis

AU - Weber,M.

N1 - Proceedings of the 18th International SPIN Workshop, SPIN 2011, Snow Bird, Utah

PY - 2011/4/15

Y1 - 2011/4/15

N2 - 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.

AB - 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.

KW - Multi-Core

KW - Model Checking

KW - CR-D.2.4

KW - METIS-277631

KW - EWI-20160

KW - state space compression

KW - Parallel

KW - incremental algorithm

KW - tree-based algorithm

M3 - Report

BT - Parallel Recursive State Compression for Free

PB - ArXiv

CY - Ithaca, NY

ER -

Laarman A, van de Pol JC, Weber M. Parallel Recursive State Compression for Free. Ithaca, NY: ArXiv, 2011. 19 p.