A Database Approach to Distributed State-Space Generation

Stefan Blom, I. Cerna (Editor), Boudewijn R.H.M. Haverkort (Editor), Bert Lisser, Jan Cornelis van de Pol, M. Weber

    Research output: Contribution to journalArticleAcademicpeer-review

    8 Citations (Scopus)
    209 Downloads (Pure)

    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.
    Original languageUndefined
    Article number10.1093/logcom/exp004
    Pages (from-to)45-62
    Number of pages18
    JournalJournal of logic and computation
    VolumeAdvance Ac
    Issue number1
    DOIs
    Publication statusPublished - 5 Mar 2009

    Keywords

    • parallel algorithms
    • latency hiding
    • EC Grant Agreement nr.: FP6/043235
    • EWI-15980
    • Distributed model checking
    • FMT-MC: MODEL CHECKING
    • METIS-263982
    • IR-67856
    • CR-I.1.2

    Cite this