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网中可能为给定位置(即切片准则)贡献令牌的位置和变迁(即切片)。方法:对所提出的两种算法进行了形式化描述。第一种算法的最大性和第二种算法的最小性得到了严格证明。这两种算法与其他三种现有算法一起被实现并集成到同一工具中,从而能够进行公平的实证评估。结果:除两种新的Petri网切片算法外,还报告了五种算法的公开、免费且开源的实现。同时给出了新算法及其生成切片的实证评估结果。结论:第一种算法收集所有可能(在任何计算中)为切片准则贡献令牌的位置和变迁,而第二种算法则收集触发向切片准则中某位置贡献令牌的最短变迁序列所需的位置和变迁。因此,第一种算法计算得到的子网能够重现任何为感兴趣位置贡献令牌的计算。相比之下,第二种算法失去了这种可能性,但通常能生成规模更小的子网(该子网仍能重现部分为感兴趣位置贡献令牌的计算)。已证明第一种算法具有最大性,第二种算法具有最小性。