a

Conventional methods for state space exploration are limited to the analysis of small systems because they suer from excessive memory and computational re-quirements. We have developed a new dynamic probabilistic state exploration al-gorithm which addresses this problem for general, structurally unrestricted state spaces. Our method has a low state omission probability and low memory usage that is independent of the length of the state vector. In addition, the algorithm can be easily parallelised. This combination of probability and parallelism 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 its bene ts in terms of distributed run-time, speedup and eÆciency. We implement our technique on a distributed-memory parallel computer and demonstrate results which compare favourably with the performance model. Finally, we discuss suitable choices for the three hash functions upon which our algorithm is based