A Survey of Petri Nets Slicing <s> Comparison of Static Slicing Algorithms <s> Temporal logic model checking is an automatic technique for verifying finite-state concurrent systems. Specifications are expressed in a propositional temporal logic, and the concurrent system is modeled as a state-transition graph. An efficient search procedure is used to determine whether or not the state-transition graph satisfies the specification. When the technique was first developed ten years ago, it was only possible to handle concurrent systems with a few thousand states. In the last few years, however, the size of the concurrent systems that can be handled has increased dramatically. By representing transition relations and sets of states implicitly using binary decision diagrams, it is now possible to check concurrent systems with more than 10120 states. In this paper we describe in detail how the new implementation works and give realistic examples to illustrate its power. We also discuss a number of directions for future research. The necessary background information on binary decision diagrams, temporal logic, and model checking has been included in order to make the exposition as self-contained as possible. <s> BIB001 </s> A Survey of Petri Nets Slicing <s> Comparison of Static Slicing Algorithms <s> The CASAS architecture facilitates the development and implementation of future smart home technologies by offering an easy-to-install lightweight design that provides smart home capabilities out of the box with no customization or training. <s> BIB002 </s> A Survey of Petri Nets Slicing <s> Comparison of Static Slicing Algorithms <s> This study evaluates the ability of users to self-install a smart home in a box (SHiB) intended for use by a senior population. SHiB is a ubiquitous system, developed by the Washington State University Center for Advanced Studies in Adaptive Systems (CASAS). Participants involved in this study are from the greater Palouse region of Washington State, and there are 13 participants in the study with an average age of 69.23. The SHiB package, which included several different types of components to collect and transmit sensor data, was given to participants to self-install. After installation of the SHiB, the participants were visited by researchers for a check of the installation. The researchers evaluated how well the sensors were installed and asked the resident questions about the installation process to help improve the SHiB design. The results indicate strengths and weaknesses of the SHiB design. Indoor motion tracking sensors are installed with high success rate, low installation success rate was found for door sensors and setting up the Internet server. <s> BIB003
It is worth noting that the comparison presented in this section considers only the static slicing algorithms, as the dynamic ones do not contribute to the alleviation of the generated state space of  Petri nets, but mostly to the testing process. Furthermore, although the Lee et al. slicing algorithm is a static slicing algorithm, it is not included in the comparison as it does not reduce the state space of the examined nets.  Consequently, the static slicing algorithms that will be compared against the state space of the unsliced Petri net models are the APN, CTL* −X , Abstract and Safety algorithms. To compare these algorithms, two real-world case studies are used as examples, the Washington State University-Center for Advanced Studies in Adaptive Systems (WSU-CASAS) smart home project BIB002 BIB003 and the insurance claim system  . These case studies are actually used to investigate the "performance" on the slicing of strongly and non-strongly connected Petri nets, respectively. Thus, it is examined how the application of the different slicing algorithms on these two types of nets affects the total number of states, edges, places, and transitions required for the model checking and construction of the analyzed model. Specifically, the efficiency of those algorithms is compared with respect to the reduction of the state space against which the examined system properties will be verified in each case. The properties used are actually liveness and safety properties expressed in Computation Tree Logic (CTL) BIB001 .