Unfolding of Colored Petri Nets by Color Quotienting and Approximation
Authors
Pedersen, Thomas ; Kristensen, Alexander Bilgram ; Taankvist, Peter Haahr
Term
4. term
Education
Publication year
2021
Submitted on
2021-06-03
Pages
33
Abstract
Petri nets are a mathematical model used to describe systems with concurrent events. In colored Petri nets, tokens carry data values (“colors”), which makes models more compact and easier to read. Colored nets with finite color ranges can be unfolded into ordinary place/transition (P/T) nets, but this unfolding can make the nets exponentially larger. We present two formal, static analysis techniques to reduce the size of the unfolded nets. The first identifies colors that always behave the same and merges them into equivalence classes, producing a smaller colored net before unfolding. The second determines, for each place, which colors can ever occur and removes colors that can never appear there. Each method is useful on its own, and even more so in combination. Together, they produce smaller unfolded nets than state-of-the-art unfolders (MCC, Spike, and ITS-Tools) on several colored Petri nets from the Model Checking Contest, while keeping unfolding time competitive. We also demonstrate the impact by verifying queries from the 2020 Model Checking Contest on the unfolded nets from each tool.
Petri-net er en matematisk model til at beskrive systemer med samtidige hændelser. I farvede Petri-net får tokens tilknyttet data (kaldet “farver”), hvilket gør modellerne mere kompakte og lettere at læse. Farvede net med endelige farvemængder kan udfoldes til almindelige P/T-net, men denne udfoldning kan få størrelsen til at vokse eksplosivt. Vi præsenterer to formelle, statiske analyser, der mindsker størrelsen af de udfoldede net. Den første finder farver, der opfører sig ens, og samler dem i ækvivalensklasser, så det farvede net bliver mindre, før det udfoldes. Den anden bestemmer for hvert sted, hvilke farver overhovedet kan forekomme, og udelukker farver, der aldrig kan være der. Hver metode hjælper for sig, og især i kombination. Den kombinerede tilgang giver mindre udfoldede net end state-of-the-art udfoldere (MCC, Spike og ITS-Tools) på flere farvede Petri-net fra Model Checking Contest, samtidig med at udfoldningstiden er konkurrencedygtig. Vi demonstrerer også effekten ved at verificere forespørgsler fra Model Checking Contest 2020 på de udfoldede net fra hvert værktøj.
[This apstract has been rewritten with the help of AI based on the project's original abstract]
Keywords