Petri net-based parallel model checking with a splitting procedure

Model checking is very important to analyse the behavior of consumer electronic products. However, if a product has large-scale behavior, we cannot use model checking because of state space explosion. In this paper, we propose a Petri net-based framework of parallel model checking and a Petri net splitting procedure. The proposed framework is useful to reduce the size of the net, thereby increases the applicability of model checking. This parallel model checking allows us to analyse the property of each splitted nets simultaneously. We illustrate the proposed framework with a product called as i-Refrigerator as an application example.