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.
翻译:背景:Petri网切片是一种缩减Petri网规模的技术,旨在简化原始Petri网的分析或理解过程。目标:提出两种新的Petri网切片算法,用于分离给定切片准则中可能向一个或多个库所贡献令牌的库所和变迁(即切片)。方法:对提出的两种算法进行了形式化描述。从理论上证明了第一种算法的最大性和第二种算法的最小性。这两种算法与其他三种现有算法均被实现并集成到统一工具中,从而能够进行公平的实证评估。结果:除两种新的Petri网切片算法外,还报告了五种算法的公开、免费且开源实现,并给出了新算法及其生成切片的实证评估结果。结论:第一种算法收集所有可能(在任何计算中)向切片准则贡献令牌的库所和变迁,而第二种算法仅收集触发最短变迁序列所需的库所和变迁——该序列能向切片准则中的某个库所贡献令牌。因此,第一种算法所计算的子网可重现任何向目标库所贡献令牌的计算过程;相比之下,第二种算法虽丧失此能力,但通常生成规模更小的子网(仍能重现某些向目标库所贡献令牌的计算)。理论证明第一种算法具有最大性,第二种算法具有最小性。