Survey of Petri nets Slicing

Petri nets slicing is a technique that aims to improve the verification of systems modeled in Petri nets. Different Petri nets slicing constructions are studied along with algorithms to compute them. Petri nets slicing was first developed to facilitate debugging but then devel- oped for alleviating the state space explosion problem for model checking Petri nets. This article has twofold objectives, the first is to unify all the existing slicing algorithms syntactically by the definition of a standard abstract syntax and rewriting of the studied slicing algorithms using the proposed syntax. The second is to discuss the contribution of each slicing construction and comparing the major differences between them. One of the interesting exploitation of the survey is for the selection and im- provement of slicing techniques for approaches concerned by optimizing verification of state event models