Local Verification Using a Distributed State Space

This paper deals with the modular analysis of distributed concurrent systems modelled by Petri nets. The main analysis techniques of such systems suffer from the well-known problem of the combinatory explosion of state space. In order to cope with this problem, we use a modular representation of the state space instead of the ordinary one. The modular representation, namely modular state space, is much smaller than the ordinary state space. We propose to distribute the modular state space on every machine associated with one module. We enhance the modularity of the verification of some local properties of any module by limiting it to the exploration of local and some global information. Once the construction of the distributed state space is performed, there is no communication between modules during the verification.