Abstract
| Original language | Undefined |
|---|---|
| Article number | 10.1093/logcom/exp004 |
| Pages (from-to) | 45-62 |
| Number of pages | 18 |
| Journal | Journal of logic and computation |
| Volume | Advance Ac |
| Issue number | 1 |
| DOIs | |
| Publication status | Published - 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
}
A Database Approach to Distributed State-Space Generation. / Blom, Stefan; Cerna, I. (Editor); Haverkort, Boudewijn R.H.M. (Editor); Lisser, Bert; van de Pol, Jan Cornelis; Weber, M.
In: Journal of logic and computation, Vol. Advance Ac, No. 1, 10.1093/logcom/exp004, 05.03.2009, p. 45-62.Research output: Contribution to journal › Article › Academic › peer-review
TY - JOUR
T1 - A Database Approach to Distributed State-Space Generation
AU - Blom, Stefan
AU - Lisser, Bert
AU - van de Pol, Jan Cornelis
AU - Weber, M.
A2 - Cerna, I.
A2 - Haverkort, Boudewijn R.H.M.
N1 - Advance Access since February 2009
PY - 2009/3/5
Y1 - 2009/3/5
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 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.
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 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.
KW - parallel algorithms
KW - latency hiding
KW - EC Grant Agreement nr.: FP6/043235
KW - EWI-15980
KW - Distributed model checking
KW - FMT-MC: MODEL CHECKING
KW - METIS-263982
KW - IR-67856
KW - CR-I.1.2
U2 - 10.1093/logcom/exp004
DO - 10.1093/logcom/exp004
M3 - Article
VL - Advance Ac
SP - 45
EP - 62
JO - Journal of logic and computation
JF - Journal of logic and computation
SN - 0955-792X
IS - 1
M1 - 10.1093/logcom/exp004
ER -