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.

翻译：有色Petri网为传统P/T网提供了紧凑且用户友好的表示方式，有限色域的有色网可展开为底层P/T网，但代价是指数级的规模爆炸。我们提出两种基于静态分析的新技术以缩减展开后有色网的规模。第一种方法识别行为等效的颜色并将其归入等价类，从而可能减少使用的颜色数量。第二种方法对库所中可能出现的颜色集合进行过近似，并排除特定库所中绝不会出现的颜色。两种方法具有互补性，其组合方式使我们能够显著缩减模型检测竞赛基准中多个有色Petri网的规模。我们将展开器的性能与工具MCC、Spike及ITS-Tools中实现的最新先进技术进行对比，结果表明我们的方法不仅在展开时间上具有竞争力，在展开网规模以及2021年模型检测竞赛中能回答的模型检测查询数量方面均优于现有方法。