Enhancing the parallel state space generation for real-time systems

In this paper we deal with the combinatorial state space explosion problem which can occur in the generation of the state space in explicit model checking. The generation phase will determine the performances of the rest model checking, which justify the need of efficient methods to enhance the generated state space and obtain good solutions. We define the parallel generation of the state space as an optimization problem, and we propose an Ant-based clustering algorithm to optimize the parallel generation in terms of balancing the workload and minimizing the communications overhead. Earlier experimental measures performed on cluster of machines have shown very promising results.