A Survey of Petri Nets Slicing <s> APNSlicing. <s> Reverse engineering involves a great deal of effort in comprehension of the current implementation of a software system and the ways in which it differs from the original design. Automated support tools are critical to the success of such efforts. It is shown how program slicing techniques can be employed to assist in the comprehension of large software systems, through traditional slicing techniques at the statement level, and through a new technique, interface slicing, at the module level. > <s> BIB001 </s> A Survey of Petri Nets Slicing <s> APNSlicing. <s> AlPiNA is a symbolic model checker for High Level Petri nets. It is comprised of two independent modules: a GUI plugin for Eclipse and an underlying model checking engine. AlPiNA’s objective is to perform efficient and user-friendly, easy to use model checking of large software systems. This is achieved by separating the model and its properties from the model checking-related concerns: the users can describe and perform checks on a high-level model without having to master low-level techniques. This article describes the features that AlPiNA provides to the user for specifying models and properties to validate, followed by the techniques that it implements for tuning validation performance. <s> BIB002 </s> A Survey of Petri Nets Slicing <s> APNSlicing. <s> High-level Petri nets make models more concise and readable as compared to low-level Petri nets. However, usual verification techniques such as state space analysis remain an open challenge for both because of state space explosion. The contribution of this paper is to propose an approach for property based reduction of the state space of Algebraic Petri nets (a variant of high-level Petri nets). To achieve the objective, we propose a slicing algorithm for Algebraic Petri nets (APNSlicing). The proposed algorithm can alleviate state space even for certain strongly connected nets. By construction, it is guaranteed that the state space of sliced net is at most as big as the original net. We exemplify our technique through the running case study of car crash management system. <s> BIB003
The first slicing algorithm introduced to improve the model checking of Algebraic Petri nets (a variant of high-level Petri nets) was presented by Khan et al. BIB003 . The construction methodology of the slicing algorithms proposed by Khan et al. is fairly similar to the construction methodology proposed by Astrid Rakow. One limitation of the slicing algorithms proposed by Astrid Rakow is that they cannot be applied directly to Algebraic Petri nets or any other variant of high-level Petri nets. However, the basic slicing algorithm can be directly applied to Algebraic Petri nets, but the sliced net would not be optimal. As has already been discussed, Astrid Rakow introduced the notion of reading and non-reading transitions to generate reduced sliced net. In Algebraic Petri nets, reading transitions cannot be determined straightforwardly (see Figure 8 ). The process-flow diagram shown in Figure 9 gives an overview of the proposed approach by Khan et al. The first step is to unfold the Algebraic Petri net model to know the ground substitutions of the variables such that reading and non-reading transitions could be identified. BIB001 They used a particular unfolding technique developed by the Software Modelling and Verification (SMV) group at the University of Geneva, i.e., a partial unfolding BIB002 . However, any unfolding technique can be used to identify reading transitions. The slicing algorithm starts by taking an unfolded Algebraic Petri net model and a set of the criterion places. Initially, T (representing the transitions set of the slice) contains the set of all pre and post transitions of the given criterion place, which correspond to non-reading transitions only. P (representing the places set of the slice) contains all the preset places of the transitions in T . The algorithm then iteratively adds other preset transitions together with their preset places in T and P .