Efficient Unfolding and Approximation of Colored Petri Nets with Inhibitor Arcs
Author
Klostergaard, Andreas Hairing
Term
4. term
Education
Publication year
2018
Pages
44
Abstract
Petri-net er et matematisk værktøj til at beskrive og analysere systemer med samtidige processer. I farvede Petri-net kan tokens bære data (farver), og inhibitor-buer forhindrer en overgang i at ske, hvis der findes en token i en bestemt plads. I denne afhandling definerer vi en klasse af farvede Petri-net, der understøtter inhibitor-buer. Vi præsenterer en udfoldningsmetode, der oversætter disse net til (ikke-farvede) Petri-net med inhibitor-buer, så eksisterende analysemetoder kan bruges. Derudover introducerer vi en over-approksimationsalgoritme, som kan besvare et udvalg af verifikationsspørgsmål direkte på det farvede net uden at udfolde det. Denne tilgang er hurtigere for de spørgsmål, den kan håndtere, men kan ikke besvare alle typer spørgsmål. På et krævende net som BARTCOL fra MCC’2017-konkurrencen, som ingen værktøjer i konkurrencen tidligere har kunnet besvare, kan vores algoritme besvare 62 ud af 128 spørgsmål. Begge metoder er implementeret i værktøjet verifypn. Med nettene fra MCC’2017 som testsæt sammenligner vi vores udfoldning med implementeringen i værktøjet MCC: Vi er i gennemsnit 30% langsommere til selve udfoldningen, men har kortere samlet køretid på alle net undtagen ét.
Petri nets are a mathematical model for describing and analyzing systems with concurrent processes. In colored Petri nets, tokens carry data (colors), and inhibitor arcs prevent a transition from firing when a token is present in a given place. This thesis defines a class of colored Petri nets that supports inhibitor arcs. We present an unfolding method that converts these nets into (uncolored) Petri nets with inhibitor arcs, enabling the use of existing analysis techniques. We also introduce an over-approximation algorithm that can answer a subset of verification queries directly on the colored net without unfolding. This approach is faster for the queries it can handle, although it cannot answer all query types. On a challenging benchmark such as BARTCOL from the MCC’2017 competition—which previously received no answers from any tool in the contest—our algorithm answers 62 out of 128 queries. We implement both the over-approximation and the unfolding in the verifypn tool. Using the MCC’2017 nets as a test set, we compare our unfolding to the implementation in the MCC tool: on average we are 30% slower at unfolding, but achieve a shorter total run time on every net except one.
[This abstract was generated with the help of AI]
Keywords
Documents