Proceedings of ISP RAS


Translation of Nested Petri Nets into Classical Petri Nets for Unfoldings Verification

V.O. Ermakova (HSE, Moscow, Russia)
I.A. Lomazova (HSE, Moscow, Russia)

Abstract

Nested Petri nets (NP-nets) have proved to be one of the convenient formalisms for distributed multi-agent systems modeling and analysis. It allows representing multi-agent systems structure in a natural way, since tokens in the system net are Petri nets themselves, and have their own behavior. Multi-agent systems are highly concurrent. Verification of such systems with model checking method causes serious difficulties arising from the huge growth of the number of system intermediate states (state-space explosion problem). To solve this problem an approach based on unfolding system behavior was proposed in the literature. Earlier in [4] the applicability of unfolding for nested Petri nets verification was studied, and the method for constructing unfolding for safe conservative nested Petri nets was proposed. In this work we propose another method for constructing safe conservative nested Petri nets unfoldings, which is based on translation of such nets into classical Petri nets and applying standard method for unfolding construction to them. We discuss also the comparative merits of the two approaches.

Keywords

multi-agent systems; verification; Petri nets; nested Petri nets; unfoldings

Edition

Proceedings of the Institute for System Programming, vol. 28, issue 4, 2016, pp. 115-136.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2016-28(4)-7

Full text of the paper in pdf (in Russian) Back to the contents of the volume