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.

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
}