pith. sign in

arxiv: 2204.07039 · v3 · submitted 2022-04-12 · 💻 cs.LO

Methods for Efficient Unfolding of Colored Petri Nets

Alexander Bilgram , Peter G. Jensen , Thomas Pedersen , Jiri Srba , Peter H. Taankvist This is my paper

Pith reviewed 2026-05-24 12:34 UTC · model grok-4.3

classification 💻 cs.LO
keywords colored Petri netsunfoldingstatic analysisequivalence classesmodel checkingP/T netsModel Checking Contest
0
0 comments X

The pith

Two static analysis methods reduce unfolded colored Petri net size by grouping equivalent colors and dropping unreachable ones.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper develops two static-analysis techniques that limit the exponential growth when colored Petri nets are unfolded into ordinary place/transition nets. The first technique finds colors whose behavior is identical and merges them into equivalence classes. The second over-approximates the colors that can ever reach each place and removes those that cannot appear. When the two are combined they produce markedly smaller unfolded nets on Model Checking Contest examples while remaining competitive in unfolding time and allowing more model-checking queries to finish.

Core claim

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-T

What carries the argument

Static analysis that computes equivalence classes of colors together with per-place over-approximations of reachable colors.

If this is right

  • Unfolded nets from the Model Checking Contest benchmarks become smaller.
  • Unfolding time stays competitive with existing tools.
  • More model-checking queries from the 2021 contest are answered within resource limits.
  • The two techniques work together without interfering with each other.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same static-analysis ideas could be applied to other high-level net formalisms that use typed tokens.
  • Tighter over-approximations might further shrink the unfolded nets if more precise reachability information is available.
  • The reduced net sizes could enable verification of systems that previously exceeded memory limits.

Load-bearing premise

The static analyses must correctly compute equivalence classes and reachable-color sets without ever excluding a color that can actually occur in some execution.

What would settle it

A concrete counter-example would be any colored net from the Model Checking Contest on which the combined method produces an unfolded net that either omits reachable behavior or fails to reduce size relative to the MCC, Spike or ITS-Tools unfolders.

Figures

Figures reproduced from arXiv: 2204.07039 by Alexander Bilgram, Jiri Srba, Peter G. Jensen, Peter H. Taankvist, Thomas Pedersen.

Figure 1
Figure 1. Figure 1: A CPN and its Unfolding to a P/T net Figure 1a shows an integer CPN where places (circles) are associated with ranges. The initial marking contains five tokens (two of color 0 and three of color 2) in p1 and two tokens of color 5 in place p2. There is a guard on transition t (rectangle) that compares x with the integer 1 and restricts the valid bindings. We can see that the arc from t to p3 creates a produ… view at source ↗
Figure 2
Figure 2. Figure 2: Quotienting example We thus introduce color partition on places where all colors with similar behaviour in a given place are grouped into an equivalence class, denoted by θ. For the rest of this section, let us assume a fixed CPN N = (P , T , C, B, C, G, W , WI , M0 ). A partition δ is a function δ : P −→ 2 2 C \ ∅ that for a place p returns the equivalence classes of C(p) such that ( S θ∈δ(p) θ) = C(p) an… view at source ↗
Figure 3
Figure 3. Figure 3: Example CPN [PITH_FULL_IMAGE:figures/full_fig_p017_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Unfolding size and unfolding time comparison [PITH_FULL_IMAGE:figures/full_fig_p021_4.png] view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 0 minor

Summary. The paper claims to present two novel static analysis techniques for reducing the size of unfolded colored Petri nets: (1) identifying and grouping behaviorally equivalent colors and (2) overapproximating reachable colors per place to exclude unreachable ones. The combined approach is evaluated on multiple colored nets from the Model Checking Contest benchmark and is claimed to produce smaller unfolded nets while answering more model checking queries than the MCC, Spike, and ITS-Tools unfolders.

Significance. If the analyses are sound, the techniques address a practical bottleneck in colored Petri net verification by producing smaller P/T nets without altering reachable behaviors, potentially improving scalability on standard benchmarks. The work is credited for its direct comparison against state-of-the-art tools on the 2021 MCC queries and for reporting both size and query-answering metrics.

major comments (1)
  1. [Abstract] Abstract (description of the two methods): the central claim that model-checking answers on the unfolded nets remain valid for the original colored nets rests on the unstated assumption that the equivalence classes preserve all transition guards and arc expressions and that the color-exclusion overapproximation introduces no false negatives. No formal statement, invariant, or proof of these properties is referenced, making the soundness of the static analyses load-bearing for the reported query results.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the constructive review and for highlighting the importance of clearly establishing soundness in the abstract. We address the single major comment below.

read point-by-point responses

  1. Referee: [Abstract] Abstract (description of the two methods): the central claim that model-checking answers on the unfolded nets remain valid for the original colored nets rests on the unstated assumption that the equivalence classes preserve all transition guards and arc expressions and that the color-exclusion overapproximation introduces no false negatives. No formal statement, invariant, or proof of these properties is referenced, making the soundness of the static analyses load-bearing for the reported query results.

    Authors: We agree that the abstract should explicitly reference the soundness properties. In the revised version we will add a sentence stating that the equivalence relation on colors is defined so that it preserves all transition guards and arc expressions, and that the color overapproximation is a sound over-approximation (reachable colors are never excluded). Formal definitions of the equivalence, the over-approximation operator, the associated invariants, and the proofs that the unfolded net preserves the reachable behaviors of the original colored net appear in Sections 3.2 and 4.2. The abstract will cite these sections. revision: yes

Circularity Check

0 steps flagged

No circularity; claims rest on external benchmark evaluation

full rationale

The paper presents two static-analysis algorithms for colored Petri net unfolding and reports empirical size and model-checking improvements on the 2021 Model Checking Contest benchmark suite. No equations, fitted parameters, self-citations, or uniqueness theorems appear in the abstract or described content; the central claims are performance comparisons against external tools (MCC, Spike, ITS-Tools) rather than any derivation that reduces to its own inputs by construction. The soundness assumptions noted by the reader are standard verification obligations for the algorithms and do not constitute circular reasoning within the paper.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claims rest on the domain assumption that colored nets with finite colors unfold to P/T nets and that static analysis can be performed correctly; no free parameters or invented entities are mentioned.

axioms (1)
  • domain assumption Colored nets with finite color ranges can be unfolded into underlying P/T nets
    Stated as background fact in the first sentence of the abstract.

pith-pipeline@v0.9.0 · 5728 in / 1148 out tokens · 28230 ms · 2026-05-24T12:34:32.899002+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

29 extracted references · 29 canonical work pages

  1. [1]

    Kommunikation mit Automaten

    Petri C. Kommunikation mit Automaten. Ph.D. thesis, Institut für instrumentelle Mathematik, Bonn, 1962

    work page 1962

  2. [2]

    Petri nets: Properties, analysis and applications

    Murata T. Petri nets: Properties, analysis and applications. Proceedings of the IEEE, 1989. 77(4):541–580. doi:10.1109/5.24143

    work page doi:10.1109/5.24143 1989

  3. [3]

    Coloured Petri Nets and the Invariant-Method

    Jensen K. Coloured Petri Nets and the Invariant-Method. Theoretical Computer Science, 1981. 14:317–

    work page 1981

  4. [4]

    doi:10.1016/0304-3975(81)90049-9

    work page doi:10.1016/0304-3975(81)90049-9

  5. [5]

    MCC: A Tool for Unfolding Colored Petri Nets in PNML Format

    Dal Zilio S. MCC: A Tool for Unfolding Colored Petri Nets in PNML Format. In: Application and Theory of Petri Nets and Concurrency. Springer International Publishing, Cham, 2020 pp. 426–435. doi: 10.1007/978-3-030-51831-8_23

    work page doi:10.1007/978-3-030-51831-8_23 2020

  6. [6]

    An efficient method for unfolding colored Petri nets

    Liu F, Heiner M, Yang M. An efficient method for unfolding colored Petri nets. In: Proceedings of the 2012 Winter Simulation Conference (WSC). ISBN 978-1-4673-4779-2, 2012 pp. 1–12. doi:10.1109/ WSC.2012.6465203

    work page arXiv 2012

  7. [7]

    Efficient Unfolding of Coloured Petri Nets Using Interval Decision Diagrams, pp

    Schwarick M, Rohr C, Liu F, Assaf G, Chodak J, Heiner M. Efficient Unfolding of Coloured Petri Nets Using Interval Decision Diagrams, pp. 324–344. Application and Theory of Petri Nets and Concurrency. ISBN 978-3-030-51830-1, 2020. doi:10.1007/978-3-030-51831-8_16

    work page doi:10.1007/978-3-030-51831-8_16 2020

  8. [8]

    Family Reunion

    Hillah L. Family Reunion. https://mcc.lip6.fr/pdf/FamilyReunion-form.pdf, 2021

    work page 2021

  9. [9]

    Law Modeling with Ontological Support and BPMN: a Case Study

    Ciaghi A, Weldemariam K, Villafiorita A, Kessler F. Law Modeling with Ontological Support and BPMN: a Case Study. In CYBERLAWS 2011, The Second International Conference on Technical and Legal Aspects of the e-Society, 2011. pp. 29–34. A. Bilgram et. al. / Methods for Efficient Unfolding of Colored Petri Nets 319

    work page 2011

  10. [10]

    A hot drink vending machine

    Hillah L. A hot drink vending machine. https://mcc.lip6.fr/pdf/DrinkVendingMachine-form.pdf, 2021

    work page 2021

  11. [11]

    Modular Modelling of Software Product Lines with Feature Nets

    Muschevici R, Proença J, Clarke D. Modular Modelling of Software Product Lines with Feature Nets. In: Software Engineering and Formal Methods. Springer Berlin Heidelberg, Berlin, Heidelberg, 2011 pp. 318–333. doi:10.1007/978-3-642-24690-6_22

    work page doi:10.1007/978-3-642-24690-6_22 2011

  12. [12]

    Complete Results for the 2021 Edition of the Model Checking Contest

    Kordon F, Bouvier P, Garavel H, Hillah LM, Hulin-Hubard F, Amat N, Amparore E, Berthomieu B, Biswal S, Donatelli D, Galla F, , Dal Zilio S, Jensen P, He C, Le Botlan D, Li S, , Srba J, Thierry- Mieg, Walner A, Wolf K. Complete Results for the 2021 Edition of the Model Checking Contest. http://mcc.lip6.fr/2021/results.php, 2021

    work page 2021

  13. [13]

    TAPAAL 2.0: Integrated Development Environment for Timed-Arc Petri Nets

    David A, Jacobsen L, Jacobsen M, Jørgensen K, Møller M, Srba J. TAPAAL 2.0: Integrated Development Environment for Timed-Arc Petri Nets. In: Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’12), volume 7214 ofLNCS. Springer- Verlag, 2012 pp. 492–497. doi:10.1007/978-3-642-28756-5_36

    work page doi:10.1007/978-3-642-28756-5_36 2012

  14. [14]

    TAPAAL and Reachability Analysis of P/T Nets

    Jensen J, Nielsen T, Oestergaard L, Srba J. TAPAAL and Reachability Analysis of P/T Nets. LNCS Transactions on Petri Nets and Other Models of Concurrency (ToPNoC) , 2016. 9930:307–318. doi: 10.1007/978-3-662-53401-4_16

    work page doi:10.1007/978-3-662-53401-4_16 2016

  15. [15]

    Snoopy – A Unifying Petri Net Tool

    Heiner M, Herajy M, Liu F, Rohr C, Schwarick M. Snoopy – A Unifying Petri Net Tool. In: Application and Theory of Petri Nets. Springer Berlin Heidelberg, Berlin, Heidelberg. ISBN 978-3-642-31131-4, 2012 pp. 398–407. doi:10.1007/978-3-642-31131-4_22

    work page doi:10.1007/978-3-642-31131-4_22 2012

  16. [16]

    MARCIE - Model Checking and Reachability Analysis Done Efficiently

    Heiner M, Rohr C, Schwarick M. MARCIE - Model Checking and Reachability Analysis Done Efficiently. In: Application and Theory of Petri Nets and Concurrency. Springer Berlin Heidelberg, Berlin, Heidelberg, 2013 pp. 389–399. doi:10.1007/978-3-642-38697-8_21

    work page doi:10.1007/978-3-642-38697-8_21 2013

  17. [17]

    Spike - Reproducible Simulation Experiments with Configuration File Branching

    Chodak J, Heiner M. Spike - Reproducible Simulation Experiments with Configuration File Branching. In: Computational Methods in Systems Biology. Springer International Publishing, Cham. ISBN 978-3- 030-31304-3, 2019 pp. 315–321. doi:10.1007/978-3-030-31304-3_19

    work page doi:10.1007/978-3-030-31304-3_19 2019

  18. [18]

    The tool TINA — construction of abstract state spaces for Petri nets and time Petri nets

    Berthomieu B, Ribet PO, Vernadat F. The tool TINA — construction of abstract state spaces for Petri nets and time Petri nets. International Journal of Production Research , 2004. 42:2741–2756. doi:10.1080/ 00207540412331312688

    work page 2004

  19. [19]

    Petri Net Model Checking with LoLA 2

    Wolf K. Petri Net Model Checking with LoLA 2. In: Application and Theory of Petri Nets and Con- currency. Springer International Publishing, Cham. ISBN 978-3-319-91268-4, 2018 pp. 351–362. doi: 10.1007/978-3-319-91268-4_18

    work page doi:10.1007/978-3-319-91268-4_18 2018

  20. [20]

    30 Years of GreatSPN

    Amparore EG, Balbo G, Beccuti M, Donatelli S, Franceschinis G. 30 Years of GreatSPN. In: Fiondella L, Puliafito A (eds.), Principles of Performance and Reliability Modeling and Evaluation: Essays in Honor of Kishor Trivedi on his 70th Birthday. Springer International Publishing, Cham. ISBN 978-3-319-30599-8, 2016 pp. 227–254. doi:10.1007/978-3-319-30599-8_9

    work page doi:10.1007/978-3-319-30599-8_9 2016

  21. [21]

    Symbolic Model-Checking Using ITS-Tools

    Thierry-Mieg Y . Symbolic Model-Checking Using ITS-Tools. In: Tools and Algorithms for the Construc- tion and Analysis of Systems. Springer Berlin Heidelberg, Berlin, Heidelberg. ISBN 978-3-662-46681-0, 2015 pp. 231–237. doi:10.1007/978-3-662-46681-0_20

    work page doi:10.1007/978-3-662-46681-0_20 2015

  22. [22]

    Personal Correspondence with Y

    Thierry-Mieg Y . Personal Correspondence with Y . Thierry-Mieg, 2021

    work page 2021

  23. [23]

    Automatic Symmetry Detection in Well-Formed Nets

    Thierry-Mieg Y , Dutheillet C, Mounier I. Automatic Symmetry Detection in Well-Formed Nets. In: van der Aalst W, Best E (eds.), Applications and Theory of Petri Nets 2003. Springer Berlin Heidelberg, Berlin, Heidelberg. ISBN 978-3-540-44919-5, 2003 pp. 82–101. 320 A. Bilgram et. al. / Methods for Efficient Unfolding of Colored Petri Nets

    work page 2003

  24. [24]

    Efficient Unfolding and Approximation of Colored Petri Nets with Inhibitor Arcs

    Klostergaard A. Efficient Unfolding and Approximation of Colored Petri Nets with Inhibitor Arcs. Mas- ter’s thesis, Department of Computer Science, Aalborg University, 2018. URL https://projekter. aau.dk/projekter/files/281079031/main.pdf

    work page arXiv 2018

  25. [25]

    Improvements in Unfolding of Colored Petri Nets

    Bilgram A, Jensen P, Pedersen T, Srba J, Taankvist P. Improvements in Unfolding of Colored Petri Nets. In: Proceedings of the 15th International Conference on Reachability Problems (RP’21), volume 13035 of LNCS. Springer-Verlag, 2021 pp. 69–84. doi:10.1007/978-3-030-89716-1_5

    work page doi:10.1007/978-3-030-89716-1_5 2021

  26. [26]

    Coloured Petri Nets, Modelling and Validation of Concurrent Systems

    Jensen K, Kristensen LM. Coloured Petri Nets, Modelling and Validation of Concurrent Systems. Springer-Verlag Berlin Heidelberg, 1 edition, 2009. doi:10.1007/b95112

    work page doi:10.1007/b95112 2009

  27. [27]

    Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use

    Jensen K. Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use. V olume 1, volume 1. Springer-Verlag Berlin Heidelberg, 2 edition, 1996. doi:10.1007/978-3-662-03241-1

    work page doi:10.1007/978-3-662-03241-1 1996

  28. [28]

    Latte: Improving the Latency of Transiently Consistent Network Update Schedules

    Christensen N, Glavind M, Schmid S, Srba J. Latte: Improving the Latency of Transiently Consistent Network Update Schedules. SIGMETRICS Perform. Eval. Rev., 2021. 48(3):14–26. doi:10.1145/3453953. 3453957

    work page doi:10.1145/3453953 2021

  29. [29]

    Repeatability package for: Methods for Efficient Unfolding of Colored Petri Nets, 2022

    Bilgram A, Peter G J, Pedersen T, Srba J, Taankvist PH. Repeatability package for: Methods for Efficient Unfolding of Colored Petri Nets, 2022. URL https://doi.org/10.5281/zenodo.6417272

    work page doi:10.5281/zenodo.6417272 2022