A Database Approach to Distributed State Space Generation

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

doi:10.1016/j.entcs.2007.10.018

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 proceeding › Conference contribution › Academic › peer-review

12 Citations (Scopus)

77 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 language	English
Title of host publication	Proceedings of the 6th International Workshop on Parallel and Distributed Methods in verifiCation
Subtitle of host publication	PDMC 2007, 8 July 2007, Berlin, Germany
Editors	I. Černá, B.R. Haverkort
Place of Publication	Amsterdam
Publisher	Elsevier
Pages	17-32
Number of pages	16
DOIs	https://doi.org/10.1016/j.entcs.2007.10.018
Publication status	Published - 4 Mar 2008
Event	6th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2007 - Berlin, Germany Duration: 8 Jul 2007 → 8 Jul 2007 Conference number: 6 http://anna.fi.muni.cz/PDMC/PDMC07/

Publication series

Name	Electronic Notes in Theoretical Computer Science
Publisher	Elsevier
Number	1
Volume	198
ISSN (Print)	1571-0661
ISSN (Electronic)	1571-0661

Workshop

Workshop	6th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2007
Abbreviated title	PDMC
Country/Territory	Germany
City	Berlin
Period	8/07/07 → 8/07/07
Internet address	http://anna.fi.muni.cz/PDMC/PDMC07/

Keywords

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

Access to Document

10.1016/j.entcs.2007.10.018

databaseAccepted author version, 263 KB

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). Elsevier. https://doi.org/10.1016/j.entcs.2007.10.018

Blom, Stefan ; Lisser, Bert ; van de Pol, Jaco et al. / 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 = mar,

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. {\v C}ern{\'a} and B.R. Haverkort",

booktitle = "Proceedings of the 6th International Workshop on Parallel and Distributed Methods in verifiCation",

note = "6th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2007, PDMC ; Conference date: 08-07-2007 Through 08-07-2007",

url = "http://anna.fi.muni.cz/PDMC/PDMC07/",

}

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 et al.
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 proceeding › Conference contribution › Academic › peer-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

N1 - Conference code: 6

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

T2 - 6th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2007

Y2 - 8 July 2007 through 8 July 2007

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). doi: 10.1016/j.entcs.2007.10.018

A Database Approach to Distributed State Space Generation

Abstract

Publication series

Workshop

Keywords

Access to Document

Fingerprint

Cite this