PAIS Lab seminar: Verification on nested Petri nets by means of unfoldings // Vera Ermakova

At the session of our seminar,  Vera Ermakova (Master's student at the HSE CS Faculty) delivered a report "Verification on nested Petri nets by means of unfoldings".

Abstract. Nested Petri nets (NP-nets) proved to be one of the best formalisms for distributed systems analysis and modeling. They naturally represent multi-agent systems structure, because tokens in the main system net are Petri nets (P/T-nets) themselves, and can have their own behavior. 
To check nested Petri net model properties one of the most popular verification method, model checking, could be used. However, there is a crucial problem for verification of highly concurrent systems using model checking approach - a large number of interleavings of concurrent processes. This leads to the so-called state-space explosion problem. 
To tackle this problem unfolding theory was introduced. In a paper of D. Frumin and I. Lomazova applicability of unfoldings for NP-nets was studied and the method for constructing unfoldings for safe conservative NP-nets was proposed. However, as safe conservative NP-nets are bounded, for such net it is possible to construct a P/T net with equivalent behavior, for which the standard unfolding techniques can be applied. Then the question is whether direct unfolding is really better than constructing unfoldings via translation of NP-nets into safe P/T nets is better in terms of time complexity. 
Here we study this question. For that we developed an algorithm for translating a safe conservative NP-net into a behaviorally equivalent P/T net. We proved that the reachability graphs of a source NP-net and the obtained P/T net are isomorphic, and hence both unfolding methods give the same (up to isomorphism) result. From general considerations translating an NP-net into a P/T net and then constructing unfoldings will be more time consuming, than constructing unfoldings directly. To check whether this time gap reveals itself in practice, we implemented all the algorithms and compare both methods experimentally. We have shown that each conservative safe NP-net can be converted into a behaviorally equivalent classical P/T net.