A Database Approach to Distributed State-Space Generation

Stefan Blom, I. Cerna (Editor), Boudewijn R.H.M. Haverkort (Editor), Bert Lisser, Jan Cornelis van de Pol, M. Weber

Research output: Contribution to journalArticleAcademicpeer-review

5 Citations (Scopus)
47 Downloads (Pure)

Abstract

We study distributed state-space generation on a cluster of workstations. It is explained why state-space partitioning by a global hash function is problematic when states contain variables from unbounded domains, such as lists or other recursive data types. Our solution is to introduce a database which maintains a global numbering of state values. We also describe tree compression, a technique of recursive state folding, and show that it is superior to manipulating plain state vectors. This solution is implemented and linked to the muCRL toolset, where state values are implemented as maximally shared terms (ATerms). However, it is applicable to other models as well, e.g. PROMELA or LOTOS models. Our experiments show the trade-offs between keeping the database global, replicated or local, depending on the available network bandwidth and latency.
Original languageUndefined
Article number10.1093/logcom/exp004
Pages (from-to)45-62
Number of pages18
JournalJournal of logic and computation
VolumeAdvance Ac
Issue number1
DOIs
Publication statusPublished - 5 Mar 2009

Keywords

  • parallel algorithms
  • latency hiding
  • EC Grant Agreement nr.: FP6/043235
  • EWI-15980
  • Distributed model checking
  • FMT-MC: MODEL CHECKING
  • METIS-263982
  • IR-67856
  • CR-I.1.2

Cite this

Blom, Stefan ; Cerna, I. (Editor) ; Haverkort, Boudewijn R.H.M. (Editor) ; Lisser, Bert ; van de Pol, Jan Cornelis ; Weber, M. / A Database Approach to Distributed State-Space Generation. In: Journal of logic and computation. 2009 ; Vol. Advance Ac, No. 1. pp. 45-62.
@article{41b658b2cf2047fa9b3f86697d8c6c5b,
title = "A Database Approach to Distributed State-Space Generation",
abstract = "We study distributed state-space generation on a cluster of workstations. It is explained why state-space partitioning by a global hash function is problematic when states contain variables from unbounded domains, such as lists or other recursive data types. Our solution is to introduce a database which maintains a global numbering of state values. We also describe tree compression, a technique of recursive state folding, and show that it is superior to manipulating plain state vectors. This solution is implemented and linked to the muCRL toolset, where state values are implemented as maximally shared terms (ATerms). However, it is applicable to other models as well, e.g. PROMELA or LOTOS models. Our experiments show the trade-offs between keeping the database global, replicated or local, depending on the available network bandwidth and latency.",
keywords = "parallel algorithms, latency hiding, EC Grant Agreement nr.: FP6/043235, EWI-15980, Distributed model checking, FMT-MC: MODEL CHECKING, METIS-263982, IR-67856, CR-I.1.2",
author = "Stefan Blom and I. Cerna and Haverkort, {Boudewijn R.H.M.} and Bert Lisser and {van de Pol}, {Jan Cornelis} and M. Weber",
note = "Advance Access since February 2009",
year = "2009",
month = "3",
day = "5",
doi = "10.1093/logcom/exp004",
language = "Undefined",
volume = "Advance Ac",
pages = "45--62",
journal = "Journal of logic and computation",
issn = "0955-792X",
publisher = "Oxford University Press",
number = "1",

}

Blom, S, Cerna, I (ed.), Haverkort, BRHM (ed.), Lisser, B, van de Pol, JC & Weber, M 2009, 'A Database Approach to Distributed State-Space Generation' Journal of logic and computation, vol. Advance Ac, no. 1, 10.1093/logcom/exp004, pp. 45-62. https://doi.org/10.1093/logcom/exp004

A Database Approach to Distributed State-Space Generation. / Blom, Stefan; Cerna, I. (Editor); Haverkort, Boudewijn R.H.M. (Editor); Lisser, Bert; van de Pol, Jan Cornelis; Weber, M.

In: Journal of logic and computation, Vol. Advance Ac, No. 1, 10.1093/logcom/exp004, 05.03.2009, p. 45-62.

Research output: Contribution to journalArticleAcademicpeer-review

TY - JOUR

T1 - A Database Approach to Distributed State-Space Generation

AU - Blom, Stefan

AU - Lisser, Bert

AU - van de Pol, Jan Cornelis

AU - Weber, M.

A2 - Cerna, I.

A2 - Haverkort, Boudewijn R.H.M.

N1 - Advance Access since February 2009

PY - 2009/3/5

Y1 - 2009/3/5

N2 - We study distributed state-space generation on a cluster of workstations. It is explained why state-space partitioning by a global hash function is problematic when states contain variables from unbounded domains, such as lists or other recursive data types. Our solution is to introduce a database which maintains a global numbering of state values. We also describe tree compression, a technique of recursive state folding, and show that it is superior to manipulating plain state vectors. This solution is implemented and linked to the muCRL toolset, where state values are implemented as maximally shared terms (ATerms). However, it is applicable to other models as well, e.g. PROMELA or LOTOS models. Our experiments show the trade-offs between keeping the database global, replicated or local, depending on the available network bandwidth and latency.

AB - We study distributed state-space generation on a cluster of workstations. It is explained why state-space partitioning by a global hash function is problematic when states contain variables from unbounded domains, such as lists or other recursive data types. Our solution is to introduce a database which maintains a global numbering of state values. We also describe tree compression, a technique of recursive state folding, and show that it is superior to manipulating plain state vectors. This solution is implemented and linked to the muCRL toolset, where state values are implemented as maximally shared terms (ATerms). However, it is applicable to other models as well, e.g. PROMELA or LOTOS models. Our experiments show the trade-offs between keeping the database global, replicated or local, depending on the available network bandwidth and latency.

KW - parallel algorithms

KW - latency hiding

KW - EC Grant Agreement nr.: FP6/043235

KW - EWI-15980

KW - Distributed model checking

KW - FMT-MC: MODEL CHECKING

KW - METIS-263982

KW - IR-67856

KW - CR-I.1.2

U2 - 10.1093/logcom/exp004

DO - 10.1093/logcom/exp004

M3 - Article

VL - Advance Ac

SP - 45

EP - 62

JO - Journal of logic and computation

JF - Journal of logic and computation

SN - 0955-792X

IS - 1

M1 - 10.1093/logcom/exp004

ER -