A Database Approach to Distributed State Space Generation

Stefan Blom, Bert Lisser, Jaco van de Pol, Michael Weber

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    9 Citations (Scopus)
    17 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 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.
    Original languageEnglish
    Title of host publicationProceedings of the 6th International Workshop on Parallel and Distributed Methods in verifiCation
    Subtitle of host publicationPDMC 2007, 8 July 2007, Berlin, Germany
    EditorsI. Černá, B.R. Haverkort
    Place of PublicationAmsterdam
    PublisherElsevier
    Pages17-32
    Number of pages16
    DOIs
    Publication statusPublished - 4 Mar 2008
    Event6th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2007 - Berlin, Germany
    Duration: 8 Jul 20078 Jul 2007
    Conference number: 6
    http://anna.fi.muni.cz/PDMC/PDMC07/

    Publication series

    NameElectronic Notes in Theoretical Computer Science
    PublisherElsevier
    Number1
    Volume198
    ISSN (Print)1571-0661
    ISSN (Electronic)1571-0661

    Workshop

    Workshop6th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2007
    Abbreviated titlePDMC
    CountryGermany
    CityBerlin
    Period8/07/078/07/07
    Internet address

    Keywords

    • FMT-TOOLS
    • FMT-MC: MODEL CHECKING
    • Tree compression
    • μCRL
    • State collapsing
    • State space partitioning

    Fingerprint Dive into the research topics of 'A Database Approach to Distributed State Space Generation'. Together they form a unique fingerprint.

  • Cite this

    Blom, S., Lisser, B., van de Pol, J., & Weber, M. (2008). A Database Approach to Distributed State Space Generation. In I. Černá, & B. R. Haverkort (Eds.), Proceedings of the 6th International Workshop on Parallel and Distributed Methods in verifiCation: PDMC 2007, 8 July 2007, Berlin, Germany (pp. 17-32). (Electronic Notes in Theoretical Computer Science; Vol. 198, No. 1). Amsterdam: Elsevier. https://doi.org/10.1016/j.entcs.2007.10.018