A Database Approach to Distributed State-Space Generation
| Autor: | Blom, Stefan, Cerna, I., Haverkort, Boudewijn R.H.M., Lisser, Bert, van de Pol, Jan Cornelis, Weber, M. |
|---|---|
| Rok vydání: | 2009 |
| Předmět: |
latency hiding
Theoretical computer science Workstation Logic Computer science Hash function EWI-15980 Parallel algorithm 0102 computer and information sciences 02 engineering and technology computer.software_genre 01 natural sciences Data type Theoretical Computer Science law.invention Arts and Humanities (miscellaneous) law 0202 electrical engineering electronic engineering information engineering Latency (engineering) computer.programming_language IR-67856 Database parallel algorithms Distributed model checking 020207 software engineering METIS-263982 FMT-MC: MODEL CHECKING Numbering Promela 010201 computation theory & mathematics Hardware and Architecture EC Grant Agreement nr.: FP6/043235 CR-I.1.2 State space generation computer Software |
| Zdroj: | Journal of logic and computation, Advance Ac(1):10.1093/logcom/exp004, 45-62. Oxford University Press |
| ISSN: | 0955-792X |
| DOI: | 10.1093/logcom/exp004 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|