Unfolding of Colored Petri Nets by Color Quotienting and Approximation

Student thesis: Master thesis (including HD thesis)

  • Thomas Pedersen
  • Alexander Bilgram Kristensen
  • Peter Haahr Taankvist
4. term, Computer Science, Master (Master Programme)
Colored Petri nets offer a compact and user friendly representation of traditional Petri nets also known as P/T nets. Colored Petri nets with finite color ranges can be unfolded into traditional P/T nets. However, this unfolding may produce exponentially larger P/T nets. We present two novel formal techniques based on static analyses for reducing the size of unfolded colored Petri nets. The first method identifies colors that behave equivalent in the colored Petri net and groups them into equivalence classes representing the colors, producing a smaller quotiented colored Petri net. The second method analyses which colors can ever exist in any place and excludes colors that can never be present in a given place. Both methods show great promise individually, but even more when combined. The combined method is able to reduce the size of multiple colored Petri nets from the Model Checking Contest compared to state of the art unfolders MCC, Spike and ITS-Tools, while still remaining competitive in terms of unfolding time. Lastly, we show the effect of the smaller unfolded nets by verifying queries from the 2020 Model Checking Contest using the unfolded nets from each tool.
LanguageEnglish
Publication date3 Jun 2021
Number of pages33
ID: 413695062