A Survey of Petri Nets Slicing <s> Chang et al. Slicing <s> Program slices are useful in debugging, testing, maintenance, and understanding of programs. The conventional notion of a program slice, the static slice , is the set of all statements that might affect the value of a given variable occurrence. In this paper, we investigate the concept of the dynamic slice consisting of all statements that actually affect the value of a variable occurrence for a given program input. The sensitivity of dynamic slicing to particular program inputs makes it more useful in program debugging and testing than static slicing. Several approaches for computing dynamic slices are examined. The notion of a Dynamic Dependence Graph and its use in computing dynamic slices is discussed. The Dynamic Dependence Graph may be unbounded in length; therefore, we introduce the economical concept of a Reduced Dynamic Dependence Graph, which is proportional in size to the number of dynamic slices arising during the program execution. <s> BIB001 </s> A Survey of Petri Nets Slicing <s> Chang et al. Slicing <s> Our growing dependence on increasingly complex computer and software systems necessitates the development of formalisms, techniques, and tools for assessing functional properties of these systems. One such technique that has emerged in the last twenty years is model checking, which systematically (and automatically) checks whether a model of a given system satisfies a desired property such as deadlock freedom, invariants, and request-response properties. This automated technique for verification and debugging has developed into a mature and widely used approach with many applications. Principles of Model Checking offers a comprehensive introduction to model checking that is not only a text suitable for classroom use but also a valuable reference for researchers and practitioners in the field. The book begins with the basic principles for modeling concurrent and communicating systems, introduces different classes of properties (including safety and liveness), presents the notion of fairness, and provides automata-based algorithms for these properties. It introduces the temporal logics LTL and CTL, compares them, and covers algorithms for verifying these logics, discussing real-time systems as well as systems subject to random phenomena. Separate chapters treat such efficiency-improving techniques as abstraction and symbolic manipulation. The book includes an extensive set of examples (most of which run through several chapters) and a complete set of basic results accompanied by detailed proofs. Each chapter concludes with a summary, bibliographic notes, and an extensive list of exercises of both practical and theoretical nature. <s> BIB002
Chang et al. presented the first slicing algorithm for Petri nets in the context of testing  . The presented algorithm slices out all the concurrency set of a Petri net model. The concurrency set is defined as a set of paths in different processes that could be executed concurrently. Based on the information about which parts of the system would be executed, test input data can be generated. The algorithm takes as input the set of concurrent Petri net models, which is ProcessPN [1] , . . . , ProcessPN [N ], and produces an output of the concurrency set, which is S BIB001 , S BIB002 , . . . , S[I ]. The important sets required to extract the concurrency set are defined as follows: The algorithm first finds a base path that covers at least one communication transition (denoted by CS) and adds it into the concurrency set (denoted by S[I ]). To select a path that covers all the marked transitions, each process is scanned. The path may generate new communication transitions that have relations with the previous process (i.e., which has been scanned) or the succeeding process that has not been scanned yet. If this path does not involve any new communication transitions having relations with the previous processes or these transitions are already in the concurrency set, then this path is added into the concurrency set and the transitions having relations with the succeeding processes are marked. Otherwise, if this path involves new communication transitions having relations with a previous process, say x, a new path needs to be found to cover both the marked and temporarily marked transitions. If there is such a path, then replace the one already in the concurrency set with this new path and mark again the transitions in the other process. Otherwise, erase temporary marks and try to find a new path other than the old one that was already in the concurrency set. Afterward, restart the scanning process from x till all the processes have been scanned and a concurrency set has been found. The procedure is repeated until all the communication transitions are included in the certain concurrency set. The procedure named ProcedureScanninд (ProcessPN [1] , . . . A simple Petri net model (shown in Figure 16 ) is taken to apply to it the slicing algorithm proposed by Chang et al. (refer to Algorithm 6). The path shown with the red dotted line is put into the concurrency set. a smaller sliced net. The basic idea is to generate backward and forward slices, respectively, for the criterion places and then a resultant sliced net is obtained by their intersection (as shown in the Figure 17 ). It is important to note that in the forward slicing algorithm, initial markings are taken into consideration such that only those paths that contribute tokens to the criterion places are added to the sliced net. Whereas, in the backward slicing, initial markings are not utilized. For the clarity of concept, their slicing proposal is divided into three steps. In the first step, the basic algorithm given below computes a backward slice by taking as input a Petri net model and a set of criterion places.