Maximal and minimal dynamic Petri net slicing
Marisa Llorens, Javier Oliver, Josep Silva, Salvador Tamarit
TL;DR
The paper addresses the problem of efficiently reducing Petri nets for analysis by introducing two dynamic slicing algorithms: a maximal contributing slice that preserves all paths that can contribute tokens to a slicing criterion, and a minimal contributing slice that preserves only the shortest contributing firing sequence. Both algorithms are formalized with proofs of maximality and minimality, respectively, and implemented in an open-source tool, pn_slicer, alongside existing approaches for comparative evaluation. The authors provide a thorough empirical study using Model Checking Contest nets, demonstrating trade-offs in slice size, runtime, and property preservation across multiple algorithms, and showing that the new methods offer robust options for debugging (maximal slice) and component reuse (minimal/smallest slice). The work advances practical Petri net slicing by offering rigorous definitions, formal guarantees, public tooling, and fair benchmarking to support debugging, comprehension, and specialization workflows. The results have immediate impact on model checking preprocessing, net understanding, and modular reuse of Petri net components, all facilitated by accessible, reproducible software and data. $$\langle M_0,Q \rangle$$ is central to the criterion, and the methods emphasize dynamic behavior by incorporating the initial marking into slice computation, enabling precise, state-aware reductions.
Abstract
Context: Petri net slicing is a technique to reduce the size of a Petri net to ease the analysis or understanding of the original Petri net. Objective: Presenting two new Petri net slicing algorithms to isolate those places and transitions of a Petri net (the slice) that may contribute tokens to one or more places given (the slicing criterion). Method: The two algorithms proposed are formalized. The maximality of the first algorithm and the minimality of the second algorithm are formally proven. Both algorithms, together with three other state-of-the-art algorithms, have been implemented and integrated into a single tool so that we have been able to carry out a fair empirical evaluation. Results: Besides the two new Petri net slicing algorithms, a public, free, and open-source implementation of five algorithms is reported. The results of an empirical evaluation of the new algorithms and the slices they produce are also presented. Conclusions: The first algorithm collects all places and transitions that may contribute tokens (in any computation) to the slicing criterion, while the second algorithm collects the places and transitions needed to fire the shortest transition sequence that contributes tokens to some place in the slicing criterion. Therefore, the net computed by the first algorithm can reproduce any computation that contributes tokens to any place of interest. In contrast, the second algorithm loses this possibility, but it often produces a much more reduced subnet (which still can reproduce some computations that contribute tokens to some places of interest). The first algorithm is proven maximal, and the second one is proven minimal.