Structural Reductions of Colored Petri Nets and P/T Nets with Inhibitor Arcs

Studenteropgave: Kandidatspeciale og HD afgangsprojekt

  • Jesper Adriaan van Diepen
  • Nicolaj Østerby Jensen
  • Mathias Mehl Sørensen
4. semester, Datalogi, Kandidat (Kandidatuddannelse)
Structural reductions of Petri nets allow for more efficient model checking by mitigating the state space explosion problem.
For a colored Petri net (CPN) there is an additional potential explosion in the size of the net during unfolding, and therefore structural reduction of CPNs is an effective technique to improve model checking performance.

We present novel structural reduction rules for both P/T nets and CPNs as well as generalizations of existing reduction rules.
These include removal of parallel structures, removal of redundant structures, and agglomerations.
We prove the correctness of all presented rules and extensions, and implement the rules in verifypn, the verification engine of TAPAAL.
To test the implementation and performance of our rules we apply the rules on models from MCC2021.
We measure multiple metrics during testing and compare these metrics against a baseline without our presented rules.
We find that our Rule S, an atomic free agglomeration, provide 393 additional answers across all categories on the P/T nets.
Our best rules on CPN models, Rule I, U, and C, provide an additional 162 answers across all categories.
We conclude that many of our colored rules are generalizations of rules on P/T nets, and does the same reduction, but on a higher abstraction level.
However, there is next to no overhead in applying the colored rules on CPNs, and we gain time during unfolding and reducing.
Udgivelsesdato10 jun. 2022
Antal sider85
ID: 472550110