• A
  • A
  • A
  • ABC
  • ABC
  • ABC
  • А
  • А
  • А
  • А
  • А
Regular version of the site

Verification of Nested Petri Nets Using Unfolding Approach

Student: Ermakova Vera

Supervisor: Irina A. Lomazova

Faculty: Faculty of Computer Science

Educational Programme: System and Software Engineering (Master)

Year of Graduation: 2016

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.

Student Theses at HSE must be completed in accordance with the University Rules and regulations specified by each educational programme.

Summaries of all theses must be published and made freely available on the HSE website.

The full text of a thesis can be published in open access on the HSE website only if the authoring student (copyright holder) agrees, or, if the thesis was written by a team of students, if all the co-authors (copyright holders) agree. After a thesis is published on the HSE website, it obtains the status of an online publication.

Student theses are objects of copyright and their use is subject to limitations in accordance with the Russian Federation’s law on intellectual property.

In the event that a thesis is quoted or otherwise used, reference to the author’s name and the source of quotation is required.

Search all student theses