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)
    8 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

    Fingerprint

    Hash functions
    Bandwidth
    Experiments
    Virtual machine

    Keywords

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

    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
    Blom, Stefan ; Lisser, Bert ; van de Pol, Jaco ; Weber, Michael. / A Database Approach to Distributed State Space Generation. Proceedings of the 6th International Workshop on Parallel and Distributed Methods in verifiCation: PDMC 2007, 8 July 2007, Berlin, Germany. editor / I. Černá ; B.R. Haverkort. Amsterdam : Elsevier, 2008. pp. 17-32 (Electronic Notes in Theoretical Computer Science; 1).
    @inproceedings{a08448a1a83944a49c12e07c4657dc38,
    title = "A Database Approach to Distributed State Space Generation",
    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.",
    keywords = "FMT-TOOLS, FMT-MC: MODEL CHECKING, Tree compression, μCRL, State collapsing, State space partitioning",
    author = "Stefan Blom and Bert Lisser and {van de Pol}, Jaco and Michael Weber",
    year = "2008",
    month = "3",
    day = "4",
    doi = "10.1016/j.entcs.2007.10.018",
    language = "English",
    series = "Electronic Notes in Theoretical Computer Science",
    publisher = "Elsevier",
    number = "1",
    pages = "17--32",
    editor = "I. Čern{\'a} and B.R. Haverkort",
    booktitle = "Proceedings of the 6th International Workshop on Parallel and Distributed Methods in verifiCation",

    }

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

    A Database Approach to Distributed State Space Generation. / Blom, Stefan; Lisser, Bert; van de Pol, Jaco; Weber, Michael.

    Proceedings of the 6th International Workshop on Parallel and Distributed Methods in verifiCation: PDMC 2007, 8 July 2007, Berlin, Germany. ed. / I. Černá; B.R. Haverkort. Amsterdam : Elsevier, 2008. p. 17-32 (Electronic Notes in Theoretical Computer Science; Vol. 198, No. 1).

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

    TY - GEN

    T1 - A Database Approach to Distributed State Space Generation

    AU - Blom, Stefan

    AU - Lisser, Bert

    AU - van de Pol, Jaco

    AU - Weber, Michael

    PY - 2008/3/4

    Y1 - 2008/3/4

    N2 - 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.

    AB - 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.

    KW - FMT-TOOLS

    KW - FMT-MC: MODEL CHECKING

    KW - Tree compression

    KW - μCRL

    KW - State collapsing

    KW - State space partitioning

    U2 - 10.1016/j.entcs.2007.10.018

    DO - 10.1016/j.entcs.2007.10.018

    M3 - Conference contribution

    T3 - Electronic Notes in Theoretical Computer Science

    SP - 17

    EP - 32

    BT - Proceedings of the 6th International Workshop on Parallel and Distributed Methods in verifiCation

    A2 - Černá, I.

    A2 - Haverkort, B.R.

    PB - Elsevier

    CY - Amsterdam

    ER -

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