• Andreas Hairing Klostergaard
4. term, Computer Science, Master (Master Programme)
We define colored Petri nets with inhibitor arcs, and present an
unfolding method, which allows us to unfold these to Petri nets with
inhibitor arcs. We also present an overapproximation algorithm, which
can answer a subset of queries performed on colored Petri nets, without
unfolding the net. This algorithm offers faster verification of colored
Petri nets, for the queries we are able to answer. In nets like BART-
COL from the MCC'2017 competition, which has never received any
answers by any tools in the competition, we are able to answer 62 out
of 128 queries, using this algorithm. We implement both the overap-
proximation algorithm and the unfolding method in the verifypn tool.
Using the nets from the MCC'2017 competition as test set, we com-
pare the unfolding implementation to the one in the tool MCC , where
we are on average 30% slower at unfolding, but are faster in total run
time in every net except one.
Publication date2018
Number of pages44
ID: 280594448