A Database Approach to Distributed State Space Generation

Share/Save/Bookmark

Blom, Stefan and Lisser, Bert and Pol van de, Jaco and Weber, Michael (2007) A Database Approach to Distributed State Space Generation. In: Sixth International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2007, 8 July 2007, Berlin, Germany.

[img]
Preview
PDF
263Kb
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 mCRL 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.

Item Type:Conference or Workshop Item
Faculty:
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/64523
Official URL:http://www.foldr.org/~michaelw/papers/pdmc-2007-mcrl-db.pdf
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page

Metis ID: 245851