A Database Approach to Distributed State-Space Generation

Blom, Stefan and Lisser, Bert and Pol van de, Jaco and Weber, Michael (2009) A Database Approach to Distributed State-Space Generation. Journal of Logic and Computation, 21 (1). pp. 45-62. ISSN 0955-792X

PDF (Publisher's version)
Restricted to UT campus only: Request a copy
271Kb

Preview

PDF (Author's version)
276Kb

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 data types. 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 muCRL toolset, where state values are implemented as maximally shared terms (ATerms). However, it is applicable to other models as well, e.g. PROMELA or LOTOS models. Our experiments show the trade-offs between keeping the database global, replicated or local, depending on the available network bandwidth and latency.
Item Type:	Article
Copyright:	© 2009 Oxford University Press
Faculty:	Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:	Formal Methods and Tools (FMT)
Link to this item:	http://purl.utwente.nl/publications/67856
Official URL:	http://dx.doi.org/10.1093/logcom/exp004
Export this item as:	BibTeX EndNote HTML Citation Reference Manager

Show download statistics for this publication

Repository Staff Only: item control page

Metis ID: 263982