A Database Approach to Distributed State Space Generation
Blom, Stefan and Lisser, Bert and Pol, Jaco van de 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 (pp. pp. 17-32).
|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|
Electrical Engineering, Mathematics and Computer Science (EEMCS)
|Link to this item:||http://purl.utwente.nl/publications/64523|
|Export this item as:||BibTeX|
Daily downloads in the past month
Monthly downloads in the past 12 months
Repository Staff Only: item control page
Metis ID: 247086