Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Methods for Efficient Unfolding of Colored Petri Nets

Alexander Bilgram, Peter G. Jensen, Thomas Pedersen, Jiri Srba, Peter H. Taankvist

TL;DR

This paper tackles the challenge of exponential growth when unfolding colored Petri nets (CPNs) into traditional P/T nets. It introduces two static analysis methods—color quotienting, which groups bisimilarly behaving colors into equivalence classes, and color approximation, which overapproximates possible colors in each place via a monotone expansion to preserve behavioral reachability—both aiming to shrink unfolded nets without altering their reachable semantics. The methods are implemented in the TAPAAL verification suite and evaluated against state-of-the-art unfoldings (MCCUnfolder, ITS-Tools, Spike), showing substantial reductions in unfolded net size and often faster or comparable unfolding times, as well as improved query-answering coverage on Model Checking Contest benchmarks. The work provides formal guarantees via bisimulation and stable partitions, demonstrates how quotienting and approximation can be combined for practical scalability, and outlines directions for integrating with other structural reductions for colored nets. Overall, the approaches advance scalable model checking for CPNs and enhance practical verification workflows in large benchmarks.

Abstract

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.

Methods for Efficient Unfolding of Colored Petri Nets

TL;DR

This paper tackles the challenge of exponential growth when unfolding colored Petri nets (CPNs) into traditional P/T nets. It introduces two static analysis methods—color quotienting, which groups bisimilarly behaving colors into equivalence classes, and color approximation, which overapproximates possible colors in each place via a monotone expansion to preserve behavioral reachability—both aiming to shrink unfolded nets without altering their reachable semantics. The methods are implemented in the TAPAAL verification suite and evaluated against state-of-the-art unfoldings (MCCUnfolder, ITS-Tools, Spike), showing substantial reductions in unfolded net size and often faster or comparable unfolding times, as well as improved query-answering coverage on Model Checking Contest benchmarks. The work provides formal guarantees via bisimulation and stable partitions, demonstrates how quotienting and approximation can be combined for practical scalability, and outlines directions for integrating with other structural reductions for colored nets. Overall, the approaches advance scalable model checking for CPNs and enhance practical verification workflows in large benchmarks.

Abstract

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.
Paper Structure (17 sections, 9 theorems, 7 equations, 4 figures, 4 tables, 1 algorithm)

This paper contains 17 sections, 9 theorems, 7 equations, 4 figures, 4 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Related work.
  3. Preliminaries
  4. Colored Petri nets
  5. P/T nets
  6. Integer colored Petri nets
  7. Unfolding of CPNs
  8. Color quotienting
  9. Computing stable partitions
  10. Stable partition Algorithm for integer CPNs
  11. Color approximation
  12. Computing color approximation on integer CPNs
  13. Experiments
  14. Unfolding experiments
  15. Query verification experiments
  16. ...and 2 more sections

Key Result

Theorem 2.6

Given a colored Petri net $\mathcal{N} = (P^{}, T^{},\mathbb{C}^{},\mathbb{B}^{}, C^{}, G^{}, W^{}, W_I^{}, M_0^{})$ and the unfolded P/T net $\mathcal{N}^u = (P^{u}, T^{u},\mathbb{C}^{u},\mathbb{B}^{u}, C^{u}, G^{u}, W^{u}, W_I^{u}, M_0^{u})$, it holds that $M_0 \sim M_0^u$ with the labeling functi

Figures (4)

  • Figure 1: A CPN and its Unfolding to a P/T net
  • Figure 2: Quotienting example
  • Figure 3: Example CPN
  • Figure 4: Unfolding size and unfolding time comparison

Theorems & Definitions (19)

  • Definition 2.1
  • Remark 2.2
  • Example 2.3
  • Example 2.4
  • Definition 2.5: Unfolding
  • Theorem 2.6: KlostergaardThesisLattePaper
  • Definition 3.1
  • Definition 3.2
  • Definition 3.3
  • Theorem 3.4
  • ...and 9 more