A Survey of Petri Nets Slicing <s> INTRODUCTION <s> We describe a method for using abstraction to reduce the complexity of temporal-logic model checking. Using techniques similar to those involved in abstract interpretation, we construct an abstract model of a program without ever examining the corresponding unabstracted model. We show how this abstract model can be used to verify properties of the original program. We have implemented a system based on these techniques, and we demonstrate their practicality using a number of examples, including a program representing a pipelined ALU circuit with over 10 1300 states. <s> BIB001 </s> A Survey of Petri Nets Slicing <s> INTRODUCTION <s> The majority of the work carried out in the formal methods community throughout the last three decades has (for good reasons) been devoted to special languages designed to make it easier to experiment with mechanized formal methods such as theorem provers and model checkers. In this paper, we give arguments for why we believe it is time for the formal methods community to shift some of its attention towards the analysis of programs written in modern programming languages. In keeping with this philosophy, we have developed a verification and testing environment for Java, called Java PathFinder (JPF), which integrates model checking, program analysis and testing. Part of this work has consisted of building a new Java Virtual Machine that interprets Java bytecode. JPF uses state compression to handle large states, and partial order reduction, slicing, abstraction and run-time analysis techniques to reduce the state space. JPF has been applied to a real-time avionics operating system developed at Honeywell, illustrating an intricate error, and to a model of a spacecraft controller, illustrating the combination of abstraction, run-time analysis and slicing with model checking. <s> BIB002 </s> A Survey of Petri Nets Slicing <s> INTRODUCTION <s> Software engineering comprehends several disciplines devoted to prevent and remedy malfunctions and to warrant adequate behaviour. Testing, the subject of this paper, is a widespread validation approach in industry, but it is still largely ad hoc, expensive, and unpredictably effective. Indeed, software testing is a broad term encompassing a variety of activities along the development cycle and beyond, aimed at different goals. Hence, software testing research faces a collection of challenges. A consistent roadmap of the most relevant challenges to be addressed is here proposed. In it, the starting point is constituted by some important past achievements, while the destination consists of four identified goals to which research ultimately tends, but which remain as unreachable as dreams. The routes from the achievements to the dreams are paved by the outstanding research challenges, which are discussed in the paper along with interesting ongoing work. <s> BIB003 </s> A Survey of Petri Nets Slicing <s> INTRODUCTION <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> BIB004
Petri nets have been extensively used to model and analyze concurrent and distributed systems since their birth. Among several dedicated analysis techniques for Petri nets, model checking and testing are more widely and commonly used. A typical challenge in model checking is the limitations imposed by the state space explosion problem, which signifies that as systems get moderately complex, the complete enumeration of their states demands a growing amount of resources. Therefore, in some cases model checking is impractical in terms of time and memory consumption BIB004 BIB001  BIB002 . Similarly, testing suffers from problems such as a large input amount 109:2 Y. I. Khan et al. of test data, test case selection, and so on  BIB003 . As a result, an intense field of research is targeting to optimize these verification techniques, either by reducing the state space or by improving the test input data. A technique called Petri net slicing falls into the first category. Petri net slicing (PN slicing) is a syntactic technique that is used to reduce a Petri net model (PN model) based on a given criterion. The given criterion refers to the point of interest, e.g., a PN place or code line number, for which the PN model is analyzed. The sliced part constitutes only that part of a PN model that may affect the given criterion. Existing PN slicing techniques that can be found in the present literature are being reviewed in this article [9, 17, 22, 24-26, 28-30, 35] . The classification of Petri nets slicing algorithms is proposed based on their construction methodology and objective (meaning whether they are designed to improve state space analysis or testing). Further to that, a discussion about qualitative and quantitative contributions of each slicing construction and a comparison describing the major differences between them are given. A distinct practice is adopted to study the proposed slicing techniques, i.e., at first, the objective of slicing algorithm is given and then the different steps required to generate the slice are presented with the help of a process-flow diagram. Moreover, by taking a simple example of a Petri net model and a property, the algorithm is explained and evaluated in terms of state space reduction. A syntactic unification of slicing algorithms either designed to improve state space analysis or testing is also presented for easy and clear understanding. Additionally, a discussion about the application of slicing in general and with respect to other state space reduction techniques is given. Finally, some recent improvements to existing slicing algorithms are presented, which can certainly be helpful for the reduction of slice size, even for strongly connected nets. The remaining part of the article is structured as follows: in Section 2, an overview and background of slicing is discussed in the context of programming and Petri nets. A classification of Petri nets slicing is presented in Section 3. Section 4 consists of formal definitions necessary for the understanding of studied slicing algorithms. In Sections 5 and 6, a review of existing Petri nets slicing techniques is presented to provide details about the underlying theory and techniques for each slicing construction. A comparative analysis is given for all the studied algorithms in Section 7. In Section 8, the application of slicing is described in general and with respect to other state space reduction techniques. Finally, in Section 9, conclusions are drawn with respect to the review of the algorithms and the future work related to the Petri nets slicing is presented.