A Database Approach to Distributed State Space Generation

Stefan Blom, Bert Lisser, Jaco van de Pol, Michael Weber

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

9 Citations (Scopus)
3 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 datatypes. 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 μCRL toolset, where state values are implemented as maximally shared terms (ATerms). However, it is applicable to other models as well, e.g., PROMELA models via the NIPS virtual machine. Our experiments show the trade-offs between keeping the database global, replicated, or local, depending on the available network bandwidth and latency.
Original languageEnglish
Title of host publicationProceedings of the 6th International Workshop on Parallel and Distributed Methods in verifiCation
Subtitle of host publicationPDMC 2007, 8 July 2007, Berlin, Germany
EditorsI. Černá, B.R. Haverkort
Place of PublicationAmsterdam
PublisherElsevier
Pages17-32
Number of pages16
DOIs
Publication statusPublished - 4 Mar 2008
Event6th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2007 - Berlin, Germany
Duration: 8 Jul 20078 Jul 2007
Conference number: 6
http://anna.fi.muni.cz/PDMC/PDMC07/

Publication series

NameElectronic Notes in Theoretical Computer Science
PublisherElsevier
Number1
Volume198
ISSN (Print)1571-0661
ISSN (Electronic)1571-0661

Workshop

Workshop6th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2007
Abbreviated titlePDMC
CountryGermany
CityBerlin
Period8/07/078/07/07
Internet address

Fingerprint

Hash functions
Bandwidth
Experiments
Virtual machine

Keywords

  • FMT-TOOLS
  • FMT-MC: MODEL CHECKING
  • Tree compression
  • μCRL
  • State collapsing
  • State space partitioning

Cite this

Blom, S., Lisser, B., van de Pol, J., & Weber, M. (2008). A Database Approach to Distributed State Space Generation. In I. Černá, & B. R. Haverkort (Eds.), Proceedings of the 6th International Workshop on Parallel and Distributed Methods in verifiCation: PDMC 2007, 8 July 2007, Berlin, Germany (pp. 17-32). (Electronic Notes in Theoretical Computer Science; Vol. 198, No. 1). Amsterdam: Elsevier. https://doi.org/10.1016/j.entcs.2007.10.018
Blom, Stefan ; Lisser, Bert ; van de Pol, Jaco ; Weber, Michael. / A Database Approach to Distributed State Space Generation. Proceedings of the 6th International Workshop on Parallel and Distributed Methods in verifiCation: PDMC 2007, 8 July 2007, Berlin, Germany. editor / I. Černá ; B.R. Haverkort. Amsterdam : Elsevier, 2008. pp. 17-32 (Electronic Notes in Theoretical Computer Science; 1).
@inproceedings{a08448a1a83944a49c12e07c4657dc38,
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 datatypes. 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 μCRL toolset, where state values are implemented as maximally shared terms (ATerms). However, it is applicable to other models as well, e.g., PROMELA models via the NIPS virtual machine. Our experiments show the trade-offs between keeping the database global, replicated, or local, depending on the available network bandwidth and latency.",
keywords = "FMT-TOOLS, FMT-MC: MODEL CHECKING, Tree compression, μCRL, State collapsing, State space partitioning",
author = "Stefan Blom and Bert Lisser and {van de Pol}, Jaco and Michael Weber",
year = "2008",
month = "3",
day = "4",
doi = "10.1016/j.entcs.2007.10.018",
language = "English",
series = "Electronic Notes in Theoretical Computer Science",
publisher = "Elsevier",
number = "1",
pages = "17--32",
editor = "I. Čern{\'a} and B.R. Haverkort",
booktitle = "Proceedings of the 6th International Workshop on Parallel and Distributed Methods in verifiCation",

}

Blom, S, Lisser, B, van de Pol, J & Weber, M 2008, A Database Approach to Distributed State Space Generation. in I Černá & BR Haverkort (eds), Proceedings of the 6th International Workshop on Parallel and Distributed Methods in verifiCation: PDMC 2007, 8 July 2007, Berlin, Germany. Electronic Notes in Theoretical Computer Science, no. 1, vol. 198, Elsevier, Amsterdam, pp. 17-32, 6th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2007, Berlin, Germany, 8/07/07. https://doi.org/10.1016/j.entcs.2007.10.018

A Database Approach to Distributed State Space Generation. / Blom, Stefan; Lisser, Bert; van de Pol, Jaco; Weber, Michael.

Proceedings of the 6th International Workshop on Parallel and Distributed Methods in verifiCation: PDMC 2007, 8 July 2007, Berlin, Germany. ed. / I. Černá; B.R. Haverkort. Amsterdam : Elsevier, 2008. p. 17-32 (Electronic Notes in Theoretical Computer Science; Vol. 198, No. 1).

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

TY - GEN

T1 - A Database Approach to Distributed State Space Generation

AU - Blom, Stefan

AU - Lisser, Bert

AU - van de Pol, Jaco

AU - Weber, Michael

PY - 2008/3/4

Y1 - 2008/3/4

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 datatypes. 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 μCRL toolset, where state values are implemented as maximally shared terms (ATerms). However, it is applicable to other models as well, e.g., PROMELA models via the NIPS virtual machine. 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 datatypes. 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 μCRL toolset, where state values are implemented as maximally shared terms (ATerms). However, it is applicable to other models as well, e.g., PROMELA models via the NIPS virtual machine. Our experiments show the trade-offs between keeping the database global, replicated, or local, depending on the available network bandwidth and latency.

KW - FMT-TOOLS

KW - FMT-MC: MODEL CHECKING

KW - Tree compression

KW - μCRL

KW - State collapsing

KW - State space partitioning

U2 - 10.1016/j.entcs.2007.10.018

DO - 10.1016/j.entcs.2007.10.018

M3 - Conference contribution

T3 - Electronic Notes in Theoretical Computer Science

SP - 17

EP - 32

BT - Proceedings of the 6th International Workshop on Parallel and Distributed Methods in verifiCation

A2 - Černá, I.

A2 - Haverkort, B.R.

PB - Elsevier

CY - Amsterdam

ER -

Blom S, Lisser B, van de Pol J, Weber M. A Database Approach to Distributed State Space Generation. In Černá I, Haverkort BR, editors, Proceedings of the 6th International Workshop on Parallel and Distributed Methods in verifiCation: PDMC 2007, 8 July 2007, Berlin, Germany. Amsterdam: Elsevier. 2008. p. 17-32. (Electronic Notes in Theoretical Computer Science; 1). https://doi.org/10.1016/j.entcs.2007.10.018