A probabilistic dynamic technique for the distributed generation of very large state spaces

Conventional methods for state space exploration are limited to the analysi s of small systems because they suffer from excessive memory and computatio nal requirements. We have developed a new dynamic probabilistic state explo ration algorithm which addresses this problem for general, structurally unr estricted state spaces. Our method has a low state omission probability and low memory usage that i s independent of the length of the state vector. In addition, the algorithm can be easily parallelised. This combination of probability and parallelis m enables us to rapidly explore state spaces that are an order of magnitude larger than those obtainable using conventional exhaustive techniques. We derive a performance model of this new algorithm in order to quantify it s benefits in terms of distributed run-time, speedup and efficiency. We imp lement our technique on a distributed-memory parallel computer acid demonst rate results which compare favourably with the performance model. Finally, we discuss suitable choices for the three hash functions upon which our alg orithm is based. (C)2000 Elsevier Science B.V. All rights reserved.