Parallel State Space Construction for Model-Checking

Hubert Garavel, Radu Mateescu, and Irina Smarandache

Proceedings of the 8th International SPIN Workshop on Model Checking of Software SPIN'2001 (Toronto, Canada), May 2001

Revised version available as INRIA Research Report RR-4341 (December 2001), which supersedes an earlier version formerly available as INRIA Research Report RR-4145 (March 2001).


The verification of concurrent finite-state systems by model-checking often requires to generate (a large part of) the state space of the system under analysis. Because of the state explosion problem, this may be a resource-consuming operation, both in terms of memory and CPU time. In this report, we aim at improving the performances of state space construction by using parallelization techniques. We present parallel algorithms for constructing state spaces (or Labeled Transition Systems) on a network or a cluster of workstations. Each node in the network builds a part of the state space, all parts being merged to form the whole state space upon termination of the parallel computation. These algorithms have been implemented within the CADP verification tool set and experimented on various concurrent applications specified in LOTOS. The results obtained show linear speedups and a good load balancing between network nodes.

20 pages


Slides of H. Garavel's lecture at SPIN'01

See also a more recent publication about the DISTRIBUTOR and BCG_MERGE tools.

ERRATA [May 14, 2003]