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.
翻译:背景:Petrie网切片是一种缩小Petri网大小的技术,以方便分析或理解原始Petri网。目标:提供两种新的Petri网切片算法,以孤立这些地方和Petri网(切片)的过渡,这些地方和过渡可能有助于给定一个或多个地方的象征物(切片标准)。方法:两种拟议算法是正规化的。第一个算法和第二个算法的最小性得到了正式证明。两种算法与其他三个最先进的算法一起,已经实施并整合到一个工具中,以便我们能够进行公平的实证评估。结果:除了两种新的Petri网切片(切片)可帮助给定一个或更多地方的象征物化算法(切片标准)之外,除了两种新的Petri网切片(切片)的切片(切片)的切片(切片标准)可能被正式证明。第一个算法收集了所有地方和最起码的代算法(在任何计算中)都有助于确定裁量标准的转换标准,而第二个算法通常用来进行公平的计算。在第一个地方的第二个算法中,一个地方的第二个算法可以使一个最接近一个象征性的运算法成为最起码的缩算法。一个地方的缩算法。在某个的缩算法,一个地方和任何最容易的缩算法可以降低的缩算法。在某个的缩算法可以降低一个地方的缩算法。