Cover Picture Story: Experiments with Modular State Spaces

The main analysis techniques for critical systems use state space exploration. However, one is often quickly limited by the so-called state space explosion problem, even if the systems models are relatively small. Several methods have been proposed to tackle this problem in order to get a manageable state space. One of these takes advantage of the modular structure of the model in order to build a modular state space, which is basically a set of local state spaces plus a synchronisation graph indicating the global behaviour. In this paper, we present a few case studies and compare the state space sizes with those of the full state space. The results are discussed, pointing out the criteria the model should satisfy for the technique to be efficient