Efficient Unfolding and Approximation of Colored Petri Nets with Inhibitor Arcs
Term
4. term
Education
Publication year
2018
Submitted on
2018-06-08
Pages
44
Abstract
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.
Keywords
Documents