论文标题
有效展开有色培养皿网的方法
Methods for Efficient Unfolding of Colored Petri Nets
论文作者
论文摘要
彩色培养皿提供了传统的P/T网的紧凑而用户友好的表示，并可以将带有有限颜色范围的彩色网络展开到基础的P/T网中，而以大小的指数爆炸为代价。我们基于静态分析提出了两种新型技术，以减少展开的彩色网的大小。第一种方法标识了表现等效的颜色，并将它们分为等效类，从而有可能减少所用颜色的数量。第二种方法过度应用可以在某个地方出现的颜色集，并排除在给定位置中永远无法存在的颜色。两种方法都是互补的，合并的方法使我们能够从模型检查比赛基准中显着减少多种彩色培养皿网的大小。我们将进展者的性能与工具MCC，Spike和ITSools实施的最新技术进行了比较，而我们的方法是竞争性的W.R.T.展开的时间，它还胜过现有的方法，既在展开的网中，又在2021型模型检查比赛中响应的型号检查查询的数量中。
Colored Petri nets offer a compact and user friendly representation of the traditional P/T nets and colored nets with finite color ranges can be unfolded into the underlying P/T nets, however, at the expense of an exponential explosion in size. We present two novel techniques based on static analysis in order to reduce the size of unfolded colored nets. The first method identifies colors that behave equivalently and groups them into equivalence classes, potentially reducing the number of used colors. The second method overapproximates the sets of colors that can appear in places and excludes colors that can never be present in a given place. Both methods are complementary and the combined approach allows us to significantly reduce the size of multiple colored Petri nets from the Model Checking Contest benchmark. We compare the performance of our unfolder with state-of-the-art techniques implemented in the tools MCC, Spike and ITS-Tools, and while our approach is competitive w.r.t. unfolding time, it also outperforms the existing approaches both in the size of unfolded nets as well as in the number of answered model checking queries from the 2021 Model Checking Contest.
