1: \begin{abstract}

2: Colored Petri nets offer a compact and user friendly representation

3: of the traditional Place/Transition (P/T) nets and colored nets with finite color ranges

4: can be unfolded into the underlying P/T nets, however, at the expense

5: of an exponential explosion in size.

6: We present two novel techniques based on static analysis

7: in order to reduce the size of unfolded colored nets. The first method

8: identifies colors that behave equivalently and groups them into equivalence

9: classes, potentially reducing the number of used colors. The second method

10: overapproximates the sets of colors that can appear in places and excludes

11: colors that can never be present in a given place.

12: Both methods are complementary and the combined approach allows us to

13: significantly reduce the size of multiple colored Petri nets from the

14: Model Checking Contest benchmark. We compare the performance of our unfolder

15: with state-of-the-art techniques implemented in the tools

16: MCC, Spike and ITS-Tools, and while our approach is

17: competitive w.r.t.

18: unfolding time, it also outperforms the existing approaches both

19: in the size of unfolded nets as well as in the number of answered model

20: checking queries from the 2021 Model Checking Contest.

21: \end{abstract}

22: