Structural Reductions of Colored Petri Nets and P/T Nets with Inhibitor Arcs
Authors
van Diepen, Jesper Adriaan ; Jensen, Nicolaj Østerby ; Sørensen, Mathias Mehl
Term
4. term
Education
Publication year
2022
Submitted on
2022-06-10
Pages
85
Abstract
Modeltjek med Petrinetter rammes ofte af tilstandsrums-eksplosion, hvor antallet af mulige tilstande vokser meget hurtigt. For farvede Petrinetter (CPN'er) kan selve udfoldningen også få nettet til at vokse kraftigt. Strukturel reduktion forenkler net uden at ændre den adfærd, der er relevant for verifikation, og kan derfor gøre modeltjek hurtigere. Vi præsenterer nye strukturelle reduktionsregler for både P/T-net og CPN'er samt generaliseringer af eksisterende regler. Reglerne omfatter fjernelse af parallelle strukturer, fjernelse af redundante strukturer og agglomerationer (sammenlægninger). Vi beviser korrektheden af alle regler og udvidelser og implementerer dem i verifypn, TAPAALs verifikationsmotor. For at evaluere effekten anvender vi reglerne på modeller fra MCC2021 og sammenligner flere mål mod en baseline uden vores regler. Vi finder, at vores Regel S, en 'atomic free' agglomeration, giver 393 ekstra svar på tværs af alle kategorier på P/T-net. På CPN-modeller giver vores bedste regler, I, U og C, yderligere 162 svar. Mange af de farvede regler er generaliseringer af P/T-regler og opnår samme reduktion på et højere abstraktionsniveau. Der er stort set ingen overhead ved at anvende de farvede regler på CPN'er, og vi sparer tid under udfoldning og reduktion.
Model checking with Petri nets often suffers from state space explosion, where the number of possible states grows very quickly. For colored Petri nets (CPNs), the unfolding step can also cause the net to grow dramatically. Structural reduction simplifies nets without changing the behavior relevant for verification, and can therefore make model checking faster. We introduce new structural reduction rules for both P/T nets and CPNs and generalize existing rules. The rules include removing parallel structures, removing redundant structures, and agglomerations (merging parts of the net). We prove all rules and extensions correct and implement them in verifypn, the verification engine of TAPAAL. To evaluate the impact, we apply the rules to models from MCC2021 and compare multiple metrics against a baseline without our rules. We find that our Rule S, an atomic free agglomeration, provides 393 additional answers across all categories on P/T nets. On CPN models, our best rules—Rules I, U, and C—provide an additional 162 answers across all categories. We conclude that many colored rules generalize P/T rules, achieving the same reductions at a higher level of abstraction. Applying colored rules adds virtually no overhead on CPNs, and we gain time during unfolding and reduction.
[This summary has been rewritten with the help of AI based on the project's original abstract]
Keywords
Documents