Unfolding of Colored Petri Nets by Color Quotienting and Approximation

Studenteropgave: Speciale (inkl. HD afgangsprojekt)

  • Thomas Pedersen
  • Alexander Bilgram Kristensen
  • Peter Haahr Taankvist
4. semester, Datalogi, Kandidat (Kandidatuddannelse)
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.
Udgivelsesdato3 jun. 2021
Antal sider33
ID: 413695062