cl-banner

A Database Approach to Distributed State Space Generation

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

Proceedings of the 6th International Workshop on Parallel and Distributed Methods in Verification (PDMC 2007), Electronic Notes in Theoretical Computer Science 198(1), pp. 17 – 32, 2008.

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 experi-ments show the trade-offs between keeping the database global, replicated, or local, depending on the available network bandwidth and latency.

 

  PDF |    doi:10.1016/j.entcs.2007.10.018  |  © 2008 Elsevier B.V.

BibTeX 

@inproceedings{BLPW-PDMC07,
author = "Stefan Blom and Bert Lisser and Jaco van de Pol and Michael Weber",
title = "A Database Approach to Distributed State Space Generation",
booktitle = "Proceedings of the 6th International Workshop on Parallel
and Distributed Methods in Verification",
series = "Electronic Notes in Theoretical Computer Science",
volume = 198,
pages = "17--32",
year = 2007
}
Nach oben scrollen