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

Nested Petri nets verification based on net unfoldings.

Student: Frumin Daniil

Supervisor: Irina A. Lomazova

Faculty: School of Software Engineering

Educational Programme: Bachelor

Final Grade: 10

Year of Graduation: 2014

<p>45 pages, 20 illustrations, 35 references. Keywords: verification,<br />Petri nets, nested Petri nets, concurrency, model checking, unfoldings<br />multiagent systems.<br /><br />The topic of this study is the net unfoldings in application to the<br />verification of nested Petri nets. Nested Petri nets formalism is used<br />for modeling multiagency systems &ndash; systems consisting of autonomous<br />agents with their own autonomous behavior, communicating with each<br />other via the means of synchronization. Due to the independent<br />behavior of agents, multiagent systems are highly concurrent by their<br />nature.<br /><br /><br />One particular problem that is associated with the verification of<br />highly concurrent and distributed systems is the state space explosion<br />problem, when the number of reachable states of the system grows<br />exponentially with the addition of new parallel components. One of the<br />reasons for this is the immense amount of intermediate system states<br />arising due to consideration of all the sequential executions in the<br />system &ndash; interleavings. One of the solutions for this problem utilizes<br />the construction of (finite prefixes of) unfoldings.<br /><br /><br />Nets unfoldings are used for describing the behavior of the system in<br />the true concurrency semantics. In the case of highly concurrent<br />systems, the unfolding (or their finite prefixes, to be precise) is<br />smaller than the reachability graph, which allows to solve the problem<br />of the exponential blowup of the space of possible system states.<br /><br />The main result of this work is the constructive definitions of the<br />branching processes and unfoldings for conservative nested Petri nets,<br />modeling systems with a fixed number of agents. Those definitions is<br />used for constructing an unfolding-based algorithm for verification of<br />important behavioural properties of conservative nested Petri nets.<br /><br />The results of the research will be presented at the Verification and<br />Program Transformation workshop, co-located with the Computer Aided<br />Verification 2014 conference, which will be taking place in Viena in<br />July this year.<br />&nbsp;</p>

Full text (added May 28, 2014) (473.10 Kb)

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