Experimenting with the Static Slicing of Petri Nets

Abstract

Petri net is a highly useful tool for modeling, simulation, and performance analysis of discrete event systems. However, the state spaces of the Petri net models of real-life discrete-event systems are enormous. Thus, model checking of these systems takes too much time, if it is possible at all. Therefore, static slicing of Petri nets is proposed in the literature to reduce a Petri net into a smaller size on which model checking becomes possible. However, this paper finds some fundamental problems in the idea of static slicing of Petri nets: 1) Most of the algorithms given in the literature for slicing do not work for real-life discrete-event systems. 2) The idea that the smaller the Petri net (obtained by slicing), the better for model checking is fundamentally wrong. As this paper shows, removal of places can be harmful as it can cause larger state spaces than the original ones. This paper proposes four hypotheses for devising newer slicing algorithms that can work on Petri net models of real-life systems too.